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 
15 #include <set>
16 
18 
19 #include <util/symbol_table.h>
20 
22 
24 {
29 
31 
33 
34 public:
35  typedef std::set<irep_idt> recursion_sett;
36 
38  symbol_tablet &_symbol_table,
39  const source_locationt &loc,
40  const irep_idt &name_prefix,
42  const lifetimet lifetime)
43  : symbol_table(_symbol_table),
44  loc(loc),
45  ns(_symbol_table),
47  allocate_objects(ID_C, loc, name_prefix, symbol_table),
49  {
50  }
51 
52  void gen_nondet_init(
53  code_blockt &assignments,
54  const exprt &expr,
55  const std::size_t depth = 0,
56  recursion_sett recursion_set = recursion_sett(),
57  const bool assign_const = true);
58 
59  void add_created_symbol(const symbolt &symbol)
60  {
62  }
63 
65  {
67  }
68 
70  {
72  }
73 
74 private:
82  code_blockt &assignments,
83  const exprt &expr,
84  std::size_t depth,
85  const recursion_sett &recursion_set);
86 };
87 
89  code_blockt &init_code,
90  symbol_tablet &symbol_table,
91  const irep_idt base_name,
92  const typet &type,
93  const source_locationt &,
94  const c_object_factory_parameterst &object_factory_parameters,
95  const lifetimet lifetime);
96 
97 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
lifetimet
Selects the kind of objects allocated.
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, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
void add_created_symbol(const symbolt &symbol)
Add a pointer to a symbol to the list of pointers to symbols created so far.
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, std::size_t depth, const recursion_sett &recursion_set)
Generate initialisation code for each array element.
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
allocate_objectst allocate_objects
void add_created_symbol(const symbolt &symbol)
symbol_tablet & symbol_table
symbol_factoryt(symbol_tablet &_symbol_table, const source_locationt &loc, const irep_idt &name_prefix, const c_object_factory_parameterst &object_factory_params, const lifetimet lifetime)
std::set< irep_idt > recursion_sett
void mark_created_symbols_as_input(code_blockt &init_code)
const c_object_factory_parameterst & object_factory_params
void declare_created_symbols(code_blockt &init_code)
const source_locationt & loc
const lifetimet lifetime
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
Author: Diffblue Ltd.