cprover
|
Public Member Functions | |
symbol_factoryt (std::vector< symbolt const *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null) | |
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) |
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer. More... | |
Private Attributes | |
std::vector< symbolt const * > & | symbols_created |
symbol_tablet & | symbol_table |
const source_locationt & | loc |
const bool | assume_non_null |
namespacet | ns |
Definition at line 62 of file c_nondet_symbol_factory.cpp.
|
inline |
Definition at line 71 of file c_nondet_symbol_factory.cpp.
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.
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 |
Definition at line 100 of file c_nondet_symbol_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), c_new_tmp_symbol(), namespace_baset::follow(), loc, ns, typet::subtype(), symbolt::symbol_expr(), symbol_table, symbols_created, and exprt::type().
Referenced by gen_nondet_init().
void symbol_factoryt::gen_nondet_init | ( | code_blockt & | assignments, |
const exprt & | expr | ||
) |
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer.
assignments | The code block to add code to |
expr | The expression which we are generating a non-determinate value for |
Definition at line 138 of file c_nondet_symbol_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), allocate_object(), code_blockt::append(), assume_non_null, c_get_nondet_bool(), code_ifthenelset::cond(), code_ifthenelset::else_case(), namespace_baset::follow(), irept::id(), loc, ns, exprt::op0(), pointer_type(), typet::subtype(), code_ifthenelset::then_case(), to_pointer_type(), and exprt::type().
Referenced by c_nondet_symbol_factory().
|
private |
Definition at line 67 of file c_nondet_symbol_factory.cpp.
Referenced by gen_nondet_init().
|
private |
Definition at line 66 of file c_nondet_symbol_factory.cpp.
Referenced by allocate_object(), and gen_nondet_init().
|
private |
Definition at line 68 of file c_nondet_symbol_factory.cpp.
Referenced by allocate_object(), and gen_nondet_init().
|
private |
Definition at line 65 of file c_nondet_symbol_factory.cpp.
Referenced by allocate_object().
|
private |
Definition at line 64 of file c_nondet_symbol_factory.cpp.
Referenced by allocate_object().