CBMC
c_nondet_symbol_factory.cpp File Reference

C Nondet Symbol Factory. More...

+ Include dependency graph for c_nondet_symbol_factory.cpp:

Go to the source code of this file.

Functions

symbol_exprt c_nondet_symbol_factory (code_blockt &init_code, symbol_table_baset &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
 Creates a symbol and generates code so that it can vary over all possible values for its type. More...
 

Detailed Description

C Nondet Symbol Factory.

Definition in file c_nondet_symbol_factory.cpp.

Function Documentation

◆ c_nondet_symbol_factory()

symbol_exprt c_nondet_symbol_factory ( code_blockt init_code,
symbol_table_baset symbol_table,
const irep_idt  base_name,
const typet type,
const source_locationt loc,
const c_object_factory_parameterst object_factory_parameters,
const lifetimet  lifetime 
)

Creates a symbol and generates code so that it can vary over all possible values for its type.

For pointers this involves allocating symbols which it can point to.

Parameters
init_codeThe code block to add generated code to
symbol_tableThe symbol table
base_nameThe name to use for the symbol created
typeThe type for the symbol created
locThe location to assign to generated code
object_factory_parametersconfiguration parameters for the object factory
lifetimeLifetime of the allocated object (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
Returns
Returns the symbol_exprt for the symbol created

Definition at line 203 of file c_nondet_symbol_factory.cpp.