cprover
symbol_factoryt Class Reference
+ Collaboration diagram for symbol_factoryt:

Public Member Functions

 symbol_factoryt (std::vector< const symbolt * > &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const c_object_factory_parameterst &object_factory_params)
 
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, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett())
 Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer. More...
 

Private Types

typedef std::set< irep_idtrecursion_sett
 

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

std::vector< const symbolt * > & symbols_created
 
symbol_tabletsymbol_table
 
const source_locationtloc
 
namespacet ns
 
const c_object_factory_parameterstobject_factory_params
 

Detailed Description

Definition at line 27 of file c_nondet_symbol_factory.cpp.

Member Typedef Documentation

◆ recursion_sett

typedef std::set<irep_idt> symbol_factoryt::recursion_sett
private

Definition at line 35 of file c_nondet_symbol_factory.cpp.

Constructor & Destructor Documentation

◆ symbol_factoryt()

symbol_factoryt::symbol_factoryt ( std::vector< const symbolt * > &  _symbols_created,
symbol_tablet _symbol_table,
const source_locationt loc,
const c_object_factory_parameterst object_factory_params 
)
inline

Definition at line 38 of file c_nondet_symbol_factory.cpp.

Member Function Documentation

◆ allocate_object()

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.

Parameters
assignmentsThe code block to add code to
target_exprThe expression which we are allocating a symbol for
allocate_typeThe type to use for the symbol. If this doesn't match target_expr then a cast will be used for the assignment
static_lifetimeWhether the symbol created should have static lifetime
Returns
Returns the address of the allocated symbol

Definition at line 84 of file c_nondet_symbol_factory.cpp.

◆ gen_nondet_array_init()

void symbol_factoryt::gen_nondet_array_init ( code_blockt assignments,
const exprt expr,
std::size_t  depth,
const recursion_sett recursion_set 
)
private

Generate initialisation code for each array element.

Parameters
assignmentsThe code block to add code to
exprAn expression of array type
depthThe struct recursion depth
recursion_setThe struct recursion set
See also
gen_nondet_init For the meaning of the last 2 parameters

Definition at line 236 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() 
)

Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer.

Parameters
assignmentsThe code block to add code to
exprThe expression which we are generating a non-determinate value for
depthnumber of pointers followed so far during initialisation
recursion_setnames of structs seen so far on current pointer chain

Definition at line 126 of file c_nondet_symbol_factory.cpp.

Member Data Documentation

◆ loc

const source_locationt& symbol_factoryt::loc
private

Definition at line 31 of file c_nondet_symbol_factory.cpp.

◆ ns

namespacet symbol_factoryt::ns
private

Definition at line 32 of file c_nondet_symbol_factory.cpp.

◆ object_factory_params

const c_object_factory_parameterst& symbol_factoryt::object_factory_params
private

Definition at line 33 of file c_nondet_symbol_factory.cpp.

◆ symbol_table

symbol_tablet& symbol_factoryt::symbol_table
private

Definition at line 30 of file c_nondet_symbol_factory.cpp.

◆ symbols_created

std::vector<const symbolt *>& symbol_factoryt::symbols_created
private

Definition at line 29 of file c_nondet_symbol_factory.cpp.


The documentation for this class was generated from the following file: