cprover
c_nondet_symbol_factory.cpp File Reference

C Nondet Symbol Factory. More...

Include dependency graph for c_nondet_symbol_factory.cpp:

Go to the source code of this file.

Classes

class  symbol_factoryt
 

Functions

static const symboltc_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, const source_locationt &loc)
 
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...
 

Detailed Description

C Nondet Symbol Factory.

Definition in file c_nondet_symbol_factory.cpp.

Function Documentation

◆ c_get_nondet_bool()

static exprt c_get_nondet_bool ( const typet type,
const source_locationt loc 
)
static
Parameters
typeDesired type (C_bool or plain bool)
locsource location
Returns
nondet expr of that type

Definition at line 48 of file c_nondet_symbol_factory.cpp.

References loc.

Referenced by symbol_factoryt::gen_nondet_init().

◆ c_new_tmp_symbol()

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" 
)
static

Create a new temporary static symbol.

Parameters
symbol_tableThe symbol table to create the symbol in
locThe location to assign to the symbol
typeThe type of symbol to create
static_lifetimeWhether the symbol should have a static lifetime
prefixThe prefix to use for the symbol's basename
Returns
Returns a reference to the new symbol

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().

◆ c_nondet_symbol_factory()

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.

Parameters
init_codeThe code block to add generated code to
symbol_tableThe symbol table
base_nameThe name to use for the symbol created
typeThe type for the symbol created
locThe location to assign to generated code
allow_nullWhether to allow a null value when type is a pointer
Returns
Returns the symbol_exprt for the symbol created

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().