symbol_factoryt Class Reference

#include <c_nondet_symbol_factory.h>

Collaboration diagram for symbol_factoryt:

Public Types
typedef std::set< irep_idt >	recursion_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_baset &	symbol_table
const source_locationt &	loc
namespacet	ns
const c_object_factory_parameterst &	object_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

typedef std::set<irep_idt> symbol_factoryt::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

assignments	The code block to add code to
expr	An expression of array type
depth	The struct recursion depth
recursion_set	The 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

assignments	The code block to add code to
expr	The expression which we are generating a non-determinate value for
depth	number of pointers followed so far during initialisation
recursion_set	names of structs seen so far on current pointer chain
assign_const	Indicates 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:

• /home/runner/work/cbmc/cbmc/src/ansi-c/c_nondet_symbol_factory.h
• /home/runner/work/cbmc/cbmc/src/ansi-c/c_nondet_symbol_factory.cpp