Go to the documentation of this file.
40 const std::size_t depth,
42 const bool assign_const)
51 if(type.
id()==ID_pointer)
57 if(subtype.
id() == ID_code)
67 if(subtype.
id() == ID_struct_tag)
72 recursion_set.find(struct_tag) != recursion_set.end() &&
84 typet object_type = subtype;
85 if(object_type.
id() == ID_empty)
89 non_null_inst, expr, object_type,
lifetime);
91 gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set,
true);
97 assignments.
append(non_null_inst);
114 std::move(set_null_inst),
115 std::move(non_null_inst));
117 assignments.
add(std::move(null_check));
120 else if(type.
id() == ID_struct_tag)
124 const irep_idt struct_tag = struct_tag_type.get_identifier();
126 recursion_set.insert(struct_tag);
130 for(
const auto &
component : struct_type.components())
134 if(!assign_const && component_type.
get_bool(ID_C_constant))
147 else if(type.
id() == ID_array)
162 assignments.
add(std::move(assign));
173 const auto &size = array_type.size();
176 DATA_INVARIANT(array_size > 0,
"Arrays should have positive size");
177 for(
size_t index = 0; index < array_size; ++index)
213 main_symbol.
mode=ID_C;
215 main_symbol.
name=identifier;
217 main_symbol.
type=type;
223 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
230 object_factory_parameters,
239 init_code.
append(assignments);
243 return main_symbol_expr;
const irep_idt & get_identifier() const
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.
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
typet type
Type of symbol.
const c_object_factory_parameterst & object_factory_params
symbol_exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, std::size_t depth, const recursion_sett &recursion_set)
Generate initialisation code for each array element.
Expression to hold a symbol (variable)
codet representation of an if-then-else statement.
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
irep_idt mode
Language mode.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
The null pointer constant.
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void add_created_symbol(const symbolt *symbol_ptr)
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void add(const codet &code)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
lifetimet
Selects the kind of objects allocated.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
bitvector_typet char_type()
A side_effect_exprt that returns a non-deterministically chosen value.
Extract member of struct or union.
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
const source_locationt & loc
source_locationt location
Source code location of definition of symbol.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
allocate_objectst allocate_objects
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Goto Programs with Functions.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
std::set< irep_idt > recursion_sett
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
source_locationt & add_source_location()
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
unsignedbv_typet size_type()
A codet representing an assignment in the program.
void mark_created_symbols_as_input(code_blockt &init_code)
API to expression classes.
irep_idt name
The unique identifier.
Nondeterministic boolean helper.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void declare_created_symbols(code_blockt &init_code)