c_nondet_symbol_factory.h File Reference

C Nondet Symbol Factory. More...

#include <set>
#include <goto-programs/allocate_objects.h>

Include dependency graph for c_nondet_symbol_factory.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	symbol_factoryt

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 &, 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.h.

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_code	The code block to add generated code to
symbol_table	The symbol table
base_name	The name to use for the symbol created
type	The type for the symbol created
loc	The location to assign to generated code
object_factory_parameters	configuration parameters for the object factory
lifetime	Lifetime 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.