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

Public Member Functions

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

Detailed Description

Definition at line 62 of file c_nondet_symbol_factory.cpp.

Constructor & Destructor Documentation

§ symbol_factoryt()

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

Definition at line 71 of file c_nondet_symbol_factory.cpp.

References allocate_object(), and gen_nondet_init().

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 100 of file c_nondet_symbol_factory.cpp.

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

Referenced by gen_nondet_init(), and symbol_factoryt().

§ 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 138 of file c_nondet_symbol_factory.cpp.

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

Referenced by c_nondet_symbol_factory(), and symbol_factoryt().

Member Data Documentation

§ assume_non_null

const bool symbol_factoryt::assume_non_null
private

Definition at line 67 of file c_nondet_symbol_factory.cpp.

Referenced by gen_nondet_init().

§ loc

const source_locationt& symbol_factoryt::loc
private

§ ns

namespacet symbol_factoryt::ns
private

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

Referenced by allocate_object().

§ symbols_created

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

Definition at line 64 of file c_nondet_symbol_factory.cpp.

Referenced by allocate_object(), and c_nondet_symbol_factory().


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