cprover
Loading...
Searching...
No Matches
symbol_factoryt Class Reference

#include <c_nondet_symbol_factory.h>

+ Collaboration diagram for symbol_factoryt:

Public Types

typedef std::set< irep_idtrecursion_sett
 

Public Member Functions

 symbol_factoryt (symbol_table_baset &_symbol_table, const source_locationt &loc, const irep_idt &name_prefix, const c_object_factory_parameterst &object_factory_params, const lifetimet lifetime)
 
void gen_nondet_init (code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
 Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer.
 
void add_created_symbol (const symbolt &symbol)
 
void declare_created_symbols (code_blockt &init_code)
 
void mark_created_symbols_as_input (code_blockt &init_code)
 

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.
 

Private Attributes

symbol_table_basetsymbol_table
 
const source_locationtloc
 
namespacet ns
 
const c_object_factory_parameterstobject_factory_params
 
allocate_objectst allocate_objects
 
const lifetimet lifetime
 

Detailed Description

Definition at line 21 of file c_nondet_symbol_factory.h.

Member Typedef Documentation

◆ recursion_sett

Definition at line 33 of file c_nondet_symbol_factory.h.

Constructor & Destructor Documentation

◆ symbol_factoryt()

symbol_factoryt::symbol_factoryt ( symbol_table_baset & _symbol_table,
const source_locationt & loc,
const irep_idt & name_prefix,
const c_object_factory_parameterst & object_factory_params,
const lifetimet lifetime )
inline

Definition at line 35 of file c_nondet_symbol_factory.h.

Member Function Documentation

◆ add_created_symbol()

void symbol_factoryt::add_created_symbol ( const symbolt & symbol)
inline

Definition at line 57 of file c_nondet_symbol_factory.h.

◆ declare_created_symbols()

void symbol_factoryt::declare_created_symbols ( code_blockt & init_code)
inline

Definition at line 62 of file c_nondet_symbol_factory.h.

◆ 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 167 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(),
const bool assign_const = true )

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
assign_constIndicates whether const objects should be nondet initialized

Definition at line 37 of file c_nondet_symbol_factory.cpp.

◆ mark_created_symbols_as_input()

void symbol_factoryt::mark_created_symbols_as_input ( code_blockt & init_code)
inline

Definition at line 67 of file c_nondet_symbol_factory.h.

Member Data Documentation

◆ allocate_objects

allocate_objectst symbol_factoryt::allocate_objects
private

Definition at line 28 of file c_nondet_symbol_factory.h.

◆ lifetime

const lifetimet symbol_factoryt::lifetime
private

Definition at line 30 of file c_nondet_symbol_factory.h.

◆ loc

const source_locationt& symbol_factoryt::loc
private

Definition at line 24 of file c_nondet_symbol_factory.h.

◆ ns

namespacet symbol_factoryt::ns
private

Definition at line 25 of file c_nondet_symbol_factory.h.

◆ object_factory_params

const c_object_factory_parameterst& symbol_factoryt::object_factory_params
private

Definition at line 26 of file c_nondet_symbol_factory.h.

◆ symbol_table

symbol_table_baset& symbol_factoryt::symbol_table
private

Definition at line 23 of file c_nondet_symbol_factory.h.


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