Go to the documentation of this file.
18 const exprt &min_value_expr,
19 const exprt &max_value_expr,
20 const std::string &basename_prefix,
29 type, basename_prefix);
36 allocate_local_symbol,
41 const exprt &min_value_expr,
42 const exprt &max_value_expr,
43 const std::string &basename_prefix,
49 const typet &int_type = min_value_expr.
type();
53 alocate_local_symbol(int_type, basename_prefix);
77 const std::string &basename_prefix,
78 const typet &int_type,
96 const typet &int_type,
103 if(switch_cases.size() == 1)
109 mode, source_location, name_prefix, symbol_table};
113 switch_cases.size() - 1,
121 size_t case_number = 0;
122 for(
const auto &switch_case : switch_cases)
125 this_block.
add(switch_case);
129 switch_block.
add(std::move(this_case));
134 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.
Fresh auxiliary symbol creation.
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.