39 std::vector<const symbolt *> &_symbols_created,
52 const exprt &target_expr,
53 const typet &allocate_type,
54 const bool static_lifetime);
59 const std::size_t depth = 0,
86 const exprt &target_expr,
87 const typet &allocate_type,
88 const bool static_lifetime)
100 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
102 bool cast_needed=allocate_type_resolved!=target_type;
114 assignments.
add(std::move(assign));
129 const std::size_t depth,
134 if(type.
id()==ID_pointer)
140 if(subtype.
id() == ID_struct)
146 recursion_set.find(struct_tag) != recursion_set.end() &&
150 assignments.
add(std::move(c));
161 if(allocated.
id()==ID_address_of)
163 init_expr=allocated.
op0();
175 assignments.
append(non_null_inst);
188 set_null_inst.add_source_location()=
loc;
192 std::move(set_null_inst),
193 std::move(non_null_inst));
195 assignments.
add(std::move(null_check));
198 else if(type.
id() == ID_struct)
204 recursion_set.insert(struct_tag);
217 else if(type.
id() == ID_array)
232 assignments.
add(std::move(assign));
243 auto const array_size = numeric_cast_v<size_t>(array_type.size());
244 DATA_INVARIANT(array_size > 0,
"Arrays should have positive size");
245 for(
size_t index = 0; index < array_size; ++index)
278 main_symbol.
mode=ID_C;
280 main_symbol.
name=identifier;
282 main_symbol.
type=type;
288 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
291 std::vector<const symbolt *> symbols_created;
292 symbols_created.push_back(main_symbol_ptr);
295 symbols_created, symbol_table,
loc, object_factory_parameters);
301 for(
const symbolt *
const symbol_ptr : symbols_created)
305 init_code.
add(std::move(decl));
308 init_code.
append(assignments);
312 for(
symbolt const *symbol_ptr : symbols_created)
314 codet input_code(ID_input);
320 input_code.
op1()=symbol_ptr->symbol_expr();
322 init_code.
add(std::move(input_code));
325 return main_symbol_expr;
The type of an expression, extends irept.
irep_idt name
The unique identifier.
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime)
Create a symbol for a pointer to point to.
Semantic type conversion.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt mode
Language mode.
const irep_idt & get_function() const
std::vector< const symbolt * > & symbols_created
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Goto Programs with Functions.
Fresh auxiliary symbol creation.
The null pointer constant.
const componentst & components() const
Nondeterministic boolean helper.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
const source_locationt & loc
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
Extract member of struct or union.
const irep_idt & id() const
symbol_tablet & symbol_table
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects...
std::set< irep_idt > recursion_sett
A codet representing the declaration of a local variable.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett())
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
Operator to dereference a pointer.
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)
Creates a symbol and generates code so that it can vary over all possible values for its type...
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
A side_effect_exprt that returns a non-deterministically chosen value.
symbol_factoryt(std::vector< const symbolt *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const c_object_factory_parameterst &object_factory_params)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
const c_object_factory_parameterst & object_factory_params
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
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.
irep_idt base_name
Base (non-scoped) name.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
codet representation of an if-then-else statement.
Expression to hold a symbol (variable)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Data structure for representing an arbitrary statement in a program.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
A codet representing an assignment in the program.