|
| symbol_factoryt (std::vector< const symbolt * > &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const c_object_factory_parameterst &object_factory_params) |
|
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. More...
|
|
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 to if expr is a pointer. More...
|
|
Definition at line 27 of file c_nondet_symbol_factory.cpp.
◆ recursion_sett
◆ symbol_factoryt()
◆ allocate_object()
exprt symbol_factoryt::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.
- Parameters
-
assignments | The code block to add code to |
target_expr | The expression which we are allocating a symbol for |
allocate_type | The type to use for the symbol. If this doesn't match target_expr then a cast will be used for the assignment |
static_lifetime | Whether the symbol created should have static lifetime |
- Returns
- Returns the address of the allocated symbol
Definition at line 84 of file c_nondet_symbol_factory.cpp.
◆ gen_nondet_array_init()
void symbol_factoryt::gen_nondet_array_init |
( |
code_blockt & |
assignments, |
|
|
const exprt & |
expr, |
|
|
std::size_t |
depth, |
|
|
const recursion_sett & |
recursion_set |
|
) |
| |
|
private |
Generate initialisation code for each array element.
- Parameters
-
assignments | The code block to add code to |
expr | An expression of array type |
depth | The struct recursion depth |
recursion_set | The struct recursion set |
- See also
- gen_nondet_init For the meaning of the last 2 parameters
Definition at line 236 of file c_nondet_symbol_factory.cpp.
◆ gen_nondet_init()
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer.
- Parameters
-
assignments | The code block to add code to |
expr | The expression which we are generating a non-determinate value for |
depth | number of pointers followed so far during initialisation |
recursion_set | names of structs seen so far on current pointer chain |
Definition at line 126 of file c_nondet_symbol_factory.cpp.
◆ loc
◆ ns
◆ object_factory_params
◆ symbol_table
◆ symbols_created
std::vector<const symbolt *>& symbol_factoryt::symbols_created |
|
private |
The documentation for this class was generated from the following file: