Go to the documentation of this file.
39 const std::string &name_prefix,
40 const typet &int_type,
51 int_type, name_prefix,
"nondet_int", source_location, mode, symbol_table)
65 nondet_symbol, ID_ge,
from_integer(min_value, int_type))));
90 const typet &int_type,
97 if(switch_cases.size() == 1)
104 switch_cases.size() - 1,
113 size_t case_number = 0;
114 for(
const auto &switch_case : switch_cases)
117 this_block.
add(switch_case);
121 switch_block.add(std::move(this_case));
126 result_block.
add(std::move(result_switch));
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.
#define PRECONDITION(CONDITION)
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'.
codet representation of a switch-case, i.e. a case statement within a switch.
The type of an expression, extends irept.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
A codet representing the declaration of a local variable.
Expression to hold a symbol (variable)
typet & type()
Return the type of the expression.
std::vector< codet > alternate_casest
codet representation of a break statement (within a for or while loop).
const std::string & id2string(const irep_idt &d)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
The symbol table base class interface.
An assumption, which must hold in subsequent code.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void add(const codet &code)
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).
A side_effect_exprt that returns a non-deterministically chosen value.
codet representing a switch statement.
A codet representing an assignment in the program.