c_nondet_symbol_factory.cpp File Reference

#include "c_nondet_symbol_factory.h"
#include <ansi-c/c_object_factory_parameters.h>
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/namespace.h>
#include <util/nondet_bool.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <goto-programs/allocate_objects.h>
#include <goto-programs/goto_functions.h>

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_tablet &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_tablet &	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 202 of file c_nondet_symbol_factory.cpp.