Go to the documentation of this file.
9 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H
10 #define CPROVER_JAVA_BYTECODE_NONDET_H
32 const exprt &min_value_expr,
33 const exprt &max_value_expr,
34 const std::string &basename_prefix,
40 const exprt &min_value_expr,
41 const exprt &max_value_expr,
42 const std::string &basename_prefix,
68 const std::string &basename_prefix,
69 const typet &int_type,
89 const typet &int_type,
94 #endif // CPROVER_JAVA_BYTECODE_NONDET_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
The type of an expression, extends irept.
Base class for all expressions.
symbol_exprt generate_nondet_int(const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value,...
Expression to hold a symbol (variable)
std::vector< codet > alternate_casest
The symbol table base class interface.
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
API to expression classes.