cprover
symbol_factoryt Class Reference
Collaboration diagram for symbol_factoryt:
[legend]

Public Member Functions

 symbol_factoryt (std::vector< const symbolt *> &_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< const symbolt * > & symbols_created
 
symbol_tabletsymbol_table
 
const source_locationtloc
 
const bool assume_non_null
 
namespacet ns
 

Detailed Description

Definition at line 54 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 bool  _assume_non_null 
)
inline

Definition at line 63 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 92 of file c_nondet_symbol_factory.cpp.

References exprt::add_source_location(), c_new_tmp_symbol(), namespace_baset::follow(), loc, code_blockt::move(), ns, typet::subtype(), symbolt::symbol_expr(), symbol_table, symbols_created, and exprt::type().

Referenced by gen_nondet_init().

◆ 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.

Parameters
assignmentsThe code block to add code to
exprThe expression which we are generating a non-determinate value for

Definition at line 130 of file c_nondet_symbol_factory.cpp.

References 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, code_blockt::move(), ns, exprt::op0(), pointer_type(), typet::subtype(), code_ifthenelset::then_case(), to_pointer_type(), and exprt::type().

Referenced by c_nondet_symbol_factory().

Member Data Documentation

◆ assume_non_null

const bool symbol_factoryt::assume_non_null
private

Definition at line 59 of file c_nondet_symbol_factory.cpp.

Referenced by gen_nondet_init().

◆ loc

const source_locationt& symbol_factoryt::loc
private

Definition at line 58 of file c_nondet_symbol_factory.cpp.

Referenced by allocate_object(), and gen_nondet_init().

◆ ns

namespacet symbol_factoryt::ns
private

Definition at line 60 of file c_nondet_symbol_factory.cpp.

Referenced by allocate_object(), and gen_nondet_init().

◆ symbol_table

symbol_tablet& symbol_factoryt::symbol_table
private

Definition at line 57 of file c_nondet_symbol_factory.cpp.

Referenced by allocate_object().

◆ symbols_created

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

Definition at line 56 of file c_nondet_symbol_factory.cpp.

Referenced by allocate_object().


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