cprover
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  )

◆ dummy_open()

int dummy_open ( struct inode ,
struct file  
)

◆ dummy_read()

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

◆ dummy_release()

int dummy_release ( struct inode ,
struct file  
)

◆ init_module()

int init_module ( void  )

◆ nondet_int()

int nondet_int ( )

◆ nondet_uchar()

unsigned char nondet_uchar ( )

◆ nondet_uint()

unsigned int nondet_uint ( )