CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Private Member Functions | Private Attributes | List of all members
symbol_factoryt Class Reference

#include <c_nondet_symbol_factory.h>

+ Collaboration diagram for symbol_factoryt:
[フレーム]
[legend]

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:

AltStyle によって変換されたページ (->オリジナル) /