Go to the documentation of this file.
15 const exprt &min_value_expr,
16 const exprt &max_value_expr,
17 const std::string &basename_prefix,
26 type, basename_prefix);
33 allocate_local_symbol,
38 const exprt &min_value_expr,
39 const exprt &max_value_expr,
40 const std::string &basename_prefix,
46 const typet &int_type = min_value_expr.
type();
50 alocate_local_symbol(int_type, basename_prefix);
74 const std::string &basename_prefix,
75 const typet &int_type,
93 const typet &int_type,
100 if(switch_cases.size() == 1)
106 mode, source_location, name_prefix, symbol_table};
110 switch_cases.size() - 1,
118 size_t case_number = 0;
119 for(
const auto &switch_case : switch_cases)
122 this_block.
add(switch_case);
126 switch_block.
add(std::move(this_case));
131 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.
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.
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,...
The type of an expression, extends irept.
A codet representing the declaration of a local variable.
Base class for all expressions.
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).
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
The symbol table base class interface.
An assumption, which must hold in subsequent code.
void add(const codet &code)
A side_effect_exprt that returns a non-deterministically chosen value.
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
codet representing a switch statement.
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
A codet representing an assignment in the program.