c_nondet_symbol_factory.h File Reference

C Nondet Symbol Factory. More...

#include <util/std_code.h>
#include <util/symbol_table.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.

Functions
exprt	c_nondet_symbol_factory (code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &, bool allow_null)
	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()

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,
		bool	allow_null
	)

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
allow_null	Whether to allow a null value when type is a pointer

Returns

Returns the symbol_exprt for the symbol created

Definition at line 219 of file c_nondet_symbol_factory.cpp.

References code_blockt::add(), exprt::add_source_location(), code_blockt::append(), symbolt::base_name, goto_functions_templatet< goto_programt >::entry_point(), from_integer(), symbol_factoryt::gen_nondet_init(), id2string(), index_type(), symbolt::is_static_lifetime, loc, symbolt::mode, symbol_tablet::move(), symbolt::name, exprt::op0(), exprt::op1(), exprt::operands(), and symbolt::type.

Referenced by build_function_environment().