35 const bool static_lifetime,
36 const std::string &prefix=
"tmp")
63 std::vector<const symbolt *> &_symbols_created,
66 const bool _assume_non_null):
76 const exprt &target_expr,
77 const typet &allocate_type,
78 const bool static_lifetime);
93 const exprt &target_expr,
94 const typet &allocate_type,
95 const bool static_lifetime)
105 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
107 bool cast_needed=allocate_type_resolved!=target_type;
119 assignments.
move(assign);
135 if(type.
id()==ID_pointer)
146 if(allocated.
id()==ID_address_of)
148 init_expr=allocated.
op0();
160 assignments.
append(non_null_inst);
173 set_null_inst.add_source_location()=
loc;
180 assignments.
move(null_check);
190 exprt rhs=type.
id()==ID_c_bool?
196 assignments.
move(assign);
222 main_symbol.
mode=ID_C;
224 main_symbol.
name=identifier;
226 main_symbol.
type=type;
232 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
235 std::vector<const symbolt *> symbols_created;
236 symbols_created.push_back(main_symbol_ptr);
248 for(
const symbolt *
const symbol_ptr : symbols_created)
252 init_code.
move(decl);
255 init_code.
append(assignments);
259 for(
symbolt const *symbol_ptr : symbols_created)
261 codet input_code(ID_input);
267 input_code.
op1()=symbol_ptr->symbol_expr();
269 init_code.
move(input_code);
272 return main_symbol_expr;
The type of an expression.
irep_idt name
The unique identifier.
const codet & then_case() const
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.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt mode
Language mode.
const exprt & cond() const
std::vector< const symbolt * > & symbols_created
Goto Programs with Functions.
Fresh auxiliary symbol creation.
The null pointer constant.
const source_locationt & loc
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define CHECK_RETURN(CONDITION)
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, bool allow_null)
Creates a symbol and generates code so that it can vary over all possible values for its type...
const irep_idt & id() const
symbol_tablet & symbol_table
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A declaration of a local variable.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Operator to dereference a pointer.
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
A side effect that returns a non-deterministically chosen value.
const typet & follow(const typet &) const
bitvector_typet index_type()
Operator to return the address of an object.
symbol_factoryt(std::vector< const symbolt *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null)
const bool assume_non_null
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
static irep_idt entry_point()
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.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
static const symbolt & c_new_tmp_symbol(symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const bool static_lifetime, const std::string &prefix="tmp")
Create a new temporary static symbol.
source_locationt & add_source_location()
void gen_nondet_init(code_blockt &assignments, const exprt &expr)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
static exprt c_get_nondet_bool(const typet &type)
Expression to hold a symbol (variable)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
A statement in a programming language.
const typet & subtype() const
const codet & else_case() const