44 const bool static_lifetime,
45 const std::string &prefix=
"tmp")
72 std::vector<symbolt const *> &_symbols_created,
75 const bool _assume_non_null):
85 const exprt &target_expr,
86 const typet &allocate_type,
87 const bool static_lifetime);
102 const exprt &target_expr,
103 const typet &allocate_type,
104 const bool static_lifetime)
114 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
116 bool cast_needed=allocate_type_resolved!=target_type;
128 assignments.
add(assign);
144 if(type.
id()==ID_pointer)
155 if(allocated.
id()==ID_address_of)
157 init_expr=allocated.
op0();
169 assignments.
append(non_null_inst);
182 set_null_inst.add_source_location()=
loc;
189 assignments.
add(null_check);
199 exprt rhs=type.
id()==ID_c_bool?
205 assignments.
add(assign);
231 main_symbol.
mode=ID_C;
233 main_symbol.
name=identifier;
235 main_symbol.
type=type;
238 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
239 assert(!moving_symbol_failed);
241 std::vector<symbolt const *> symbols_created;
242 symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
243 symbols_created.push_back(main_symbol_ptr);
255 for(
symbolt const *symbol_ptr : symbols_created)
262 init_code.
append(assignments);
266 for(
symbolt const *symbol_ptr : symbols_created)
268 codet input_code(ID_input);
274 input_code.
op1()=symbol_ptr->symbol_expr();
276 init_code.
add(input_code);
279 return main_symbol_expr;
The type of an expression.
irep_idt name
The unique identifier.
const codet & then_case() const
const typet & follow(const typet &src) 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.
Linking: Zero Initialization.
symbol_factoryt(std::vector< symbolt const *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null)
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
irep_idt mode
Language mode.
const exprt & cond() const
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...
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
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A declaration of a local variable.
Operator to dereference a pointer.
static irep_idt entry_point()
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.
bitvector_typet index_type()
Operator to return the address of an object.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
const bool assume_non_null
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
typet type
Type of symbol.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
std::vector< symbolt const * > & symbols_created
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)
A statement in a programming language.
const typet & subtype() const
const codet & else_case() const