cprover
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_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
allow_nullWhether to allow a null value when type is a pointer
Returns
Returns the symbol_exprt for the symbol created

Definition at line 210 of file c_nondet_symbol_factory.cpp.

References exprt::add_source_location(), code_blockt::append(), symbolt::base_name, CHECK_RETURN, goto_functionst::entry_point(), from_integer(), symbol_factoryt::gen_nondet_init(), id2string(), index_type(), symbolt::is_static_lifetime, loc, symbolt::location, symbolt::mode, symbol_tablet::move(), code_blockt::move(), symbolt::name, exprt::op0(), exprt::op1(), exprt::operands(), symbolt::symbol_expr(), and symbolt::type.

Referenced by build_function_environment().