cprover
|
C Nondet Symbol Factory. More...
#include "c_nondet_symbol_factory.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/string_constant.h>
#include <goto-programs/goto_functions.h>
Go to the source code of this file.
Classes | |
class | symbol_factoryt |
Functions | |
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. More... | |
static exprt | c_get_nondet_bool (const typet &type) |
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. More... | |
C Nondet Symbol Factory.
Definition in file c_nondet_symbol_factory.cpp.
type | Desired type (C_bool or plain bool) |
Definition at line 47 of file c_nondet_symbol_factory.cpp.
Referenced by symbol_factoryt::gen_nondet_init().
|
static |
Create a new temporary static symbol.
symbol_table | The symbol table to create the symbol in |
loc | The location to assign to the symbol |
type | The type of symbol to create |
static_lifetime | Whether the symbol should have a static lifetime |
prefix | The prefix to use for the symbol's basename |
Definition at line 31 of file c_nondet_symbol_factory.cpp.
References get_fresh_aux_symbol(), id2string(), symbolt::is_static_lifetime, and loc.
Referenced by symbol_factoryt::allocate_object().
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 210 of file c_nondet_symbol_factory.cpp.
References exprt::add_source_location(), code_blockt::append(), symbolt::base_name, CHECK_RETURN, goto_functionst::entry_point(), from_integer(), symbol_factoryt::gen_nondet_init(), id2string(), index_type(), symbolt::is_static_lifetime, loc, symbolt::location, symbolt::mode, symbol_tablet::move(), code_blockt::move(), symbolt::name, exprt::op0(), exprt::op1(), exprt::operands(), symbolt::symbol_expr(), and symbolt::type.
Referenced by build_function_environment().