cprover
|
C Nondet Symbol Factory. More...
Go to the source code of this file.
Functions | |
exprt | c_nondet_symbol_factory (code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &, bool allow_null) |
Creates a symbol and generates code so that it can vary over all possible values for its type. More... | |
C Nondet Symbol Factory.
Definition in file c_nondet_symbol_factory.h.
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.
For pointers this involves allocating symbols which it can point to.
init_code | The code block to add generated code to |
symbol_table | The symbol table |
base_name | The name to use for the symbol created |
type | The type for the symbol created |
loc | The location to assign to generated code |
allow_null | Whether to allow a null value when type is a pointer |
Definition at line 219 of file c_nondet_symbol_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), code_blockt::append(), symbolt::base_name, goto_functions_templatet< goto_programt >::entry_point(), from_integer(), symbol_factoryt::gen_nondet_init(), id2string(), index_type(), symbolt::is_static_lifetime, loc, symbolt::mode, symbol_tablet::move(), symbolt::name, exprt::op0(), exprt::op1(), exprt::operands(), and symbolt::type.
Referenced by build_function_environment().