#include <c_nondet_symbol_factory.h>
Collaboration diagram for symbol_factoryt:Public Types | |
| typedef std::set< irep_idt > | recursion_sett |
Public Member Functions | |
| symbol_factoryt (symbol_table_baset &_symbol_table, const source_locationt &loc, const irep_idt &name_prefix, const c_object_factory_parameterst &object_factory_params, const lifetimet lifetime) | |
| 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 to if expr is a pointer. More... | |
| void | add_created_symbol (const symbolt &symbol) |
| void | declare_created_symbols (code_blockt &init_code) |
| void | mark_created_symbols_as_input (code_blockt &init_code) |
Private Member Functions | |
| 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. More... | |
Private Attributes | |
| symbol_table_baset & | symbol_table |
| const source_locationt & | loc |
| namespacet | ns |
| const c_object_factory_parameterst & | object_factory_params |
| allocate_objectst | allocate_objects |
| const lifetimet | lifetime |
Detailed Description
Definition at line 21 of file c_nondet_symbol_factory.h.
Member Typedef Documentation
◆ recursion_sett
| typedef std::set<irep_idt> symbol_factoryt::recursion_sett |
Definition at line 33 of file c_nondet_symbol_factory.h.
Constructor & Destructor Documentation
◆ symbol_factoryt()
|
inline |
Definition at line 35 of file c_nondet_symbol_factory.h.
Member Function Documentation
◆ add_created_symbol()
|
inline |
Definition at line 57 of file c_nondet_symbol_factory.h.
◆ declare_created_symbols()
|
inline |
Definition at line 62 of file c_nondet_symbol_factory.h.
◆ gen_nondet_array_init()
|
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 167 of file c_nondet_symbol_factory.cpp.
◆ gen_nondet_init()
| void symbol_factoryt::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 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 assign_const Indicates whether const objects should be nondet initialized
Definition at line 37 of file c_nondet_symbol_factory.cpp.
◆ mark_created_symbols_as_input()
|
inline |
Definition at line 67 of file c_nondet_symbol_factory.h.
Member Data Documentation
◆ allocate_objects
|
private |
Definition at line 28 of file c_nondet_symbol_factory.h.
◆ lifetime
|
private |
Definition at line 30 of file c_nondet_symbol_factory.h.
◆ loc
|
private |
Definition at line 24 of file c_nondet_symbol_factory.h.
◆ ns
|
private |
Definition at line 25 of file c_nondet_symbol_factory.h.
◆ object_factory_params
|
private |
Definition at line 26 of file c_nondet_symbol_factory.h.
◆ symbol_table
|
private |
Definition at line 23 of file c_nondet_symbol_factory.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/ansi-c/c_nondet_symbol_factory.h
- /home/runner/work/cbmc/cbmc/src/ansi-c/c_nondet_symbol_factory.cpp
