9 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H 10 #define CPROVER_JAVA_BYTECODE_NONDET_H 19 const std::string &name_prefix,
20 const typet &int_type,
31 const typet &int_type,
36 #endif // CPROVER_JAVA_BYTECODE_NONDET_H The type of an expression, extends irept.
symbol_exprt generate_nondet_int(const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions)
Gets a fresh nondet choice in range (min_value, max_value).
API to expression classes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The symbol table base class interface.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
A codet representing sequential composition of program statements.
Expression to hold a symbol (variable)
std::vector< codet > alternate_casest
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'.