cprover
c_nondet_symbol_factory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Nondet Symbol Factory
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
13 #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
14 
16 
17 #include <util/std_code.h>
18 #include <util/symbol_table.h>
19 
21  code_blockt &init_code,
22  symbol_tablet &symbol_table,
23  const irep_idt base_name,
24  const typet &type,
25  const source_locationt &,
26  const c_object_factory_parameterst &object_factory_parameters);
27 
28 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
The type of an expression, extends irept.
Definition: type.h:27
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 &, const c_object_factory_parameterst &object_factory_parameters)
Creates a symbol and generates code so that it can vary over all possible values for its type...
The symbol table.
Definition: symbol_table.h:19
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
A codet representing sequential composition of program statements.
Definition: std_code.h:150
Expression to hold a symbol (variable)
Definition: std_expr.h:143