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 
17 #include <util/allocate_objects.h>
18 #include <util/symbol_table.h>
19 
21 
23 {
28 
30 
32 
33 public:
34  typedef std::set<irep_idt> recursion_sett;
35 
37  symbol_tablet &_symbol_table,
38  const source_locationt &loc,
39  const irep_idt &name_prefix,
41  const lifetimet lifetime)
42  : symbol_table(_symbol_table),
43  loc(loc),
44  ns(_symbol_table),
46  allocate_objects(ID_C, loc, name_prefix, symbol_table),
48  {
49  }
50 
51  void gen_nondet_init(
52  code_blockt &assignments,
53  const exprt &expr,
54  const std::size_t depth = 0,
55  recursion_sett recursion_set = recursion_sett(),
56  const bool assign_const = true);
57 
58  void add_created_symbol(const symbolt *symbol_ptr)
59  {
61  }
62 
64  {
66  }
67 
69  {
71  }
72 
73 private:
81  code_blockt &assignments,
82  const exprt &expr,
83  std::size_t depth,
84  const recursion_sett &recursion_set);
85 };
86 
88  code_blockt &init_code,
89  symbol_tablet &symbol_table,
90  const irep_idt base_name,
91  const typet &type,
92  const source_locationt &,
93  const c_object_factory_parameterst &object_factory_parameters,
94  const lifetimet lifetime);
95 
96 #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_ptr)
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:168
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_ptr)
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:28
Author: Diffblue Ltd.