cprover
Loading...
Searching...
No Matches
driver.h File Reference
#include "modules.h"
Include dependency graph for driver.h:

Go to the source code of this file.

Macros

#define MODULE
#define TRUE   1
#define FALSE   0
#define BUF_SIZE   255

Functions

int init_module (void)
void cleanup_module (void)
int dummy_open (struct inode *, struct file *)
unsigned int dummy_read (struct file *, char *, int)
int dummy_release (struct inode *, struct file *)
int nondet_int ()
unsigned int nondet_uint ()
unsigned char nondet_uchar ()

Macro Definition Documentation

◆ BUF_SIZE

#define BUF_SIZE   255

Definition at line 10 of file driver.h.

◆ FALSE

#define FALSE   0

Definition at line 8 of file driver.h.

◆ MODULE

#define MODULE

Definition at line 4 of file driver.h.

◆ TRUE

#define TRUE   1

Definition at line 7 of file driver.h.

Function Documentation

◆ cleanup_module()

void cleanup_module ( void )
extern

◆ dummy_open()

int dummy_open ( struct inode * ,
struct file *  )
extern

◆ dummy_read()

unsigned int dummy_read ( struct file * ,
char * ,
int  )
extern

◆ dummy_release()

int dummy_release ( struct inode * ,
struct file *  )
extern

◆ init_module()

int init_module ( void )
extern

◆ nondet_int()

int nondet_int ( )

◆ nondet_uchar()

unsigned char nondet_uchar ( )

◆ nondet_uint()

unsigned int nondet_uint ( )