esbmc Namespace Reference

Functions
int	nondet_int ()
float	nondet_float ()
bool	nondet_bool ()
str	nondet_str ()
list	nondet_list ()
dict	nondet_dict ()
None	assume (bool cond)

Detailed Description

ESBMC Python intrinsic stubs.

These functions are replaced with symbolic operations during ESBMC
verification. The ESBMC Python frontend intercepts them and
translates them into symbolic operations.

Function Documentation

assume()

None esbmc.assume

(

bool

cond

)

ESBMC intrinsic: path constraint

nondet_bool()

bool esbmc.nondet_bool

(

void

)

ESBMC intrinsic: returns symbolic bool

nondet_dict()

dict esbmc.nondet_dict

(

)

ESBMC intrinsic: returns symbolic dict

nondet_float()

float esbmc.nondet_float

(

)

ESBMC intrinsic: returns symbolic float

nondet_int()

int esbmc.nondet_int

(

void

)

ESBMC intrinsic: returns symbolic int

nondet_list()

list esbmc.nondet_list

(

)

ESBMC intrinsic: returns symbolic list

nondet_str()

str esbmc.nondet_str

(

)

ESBMC intrinsic: returns symbolic string