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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
typet
The type of an expression, extends irept.
Definition: type.h:28
symbol_factoryt::object_factory_params
const c_object_factory_parameterst & object_factory_params
Definition: c_nondet_symbol_factory.h:27
allocate_objectst::add_created_symbol
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
Definition: allocate_objects.cpp:218
exprt
Base class for all expressions.
Definition: expr.h:54
symbol_factoryt::gen_nondet_array_init
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.
Definition: c_nondet_symbol_factory.cpp:164
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
symbol_factoryt::symbol_factoryt
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)
Definition: c_nondet_symbol_factory.h:36
c_nondet_symbol_factory
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.
Definition: c_nondet_symbol_factory.cpp:198
symbol_factoryt::ns
namespacet ns
Definition: c_nondet_symbol_factory.h:26
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
symbol_factoryt::add_created_symbol
void add_created_symbol(const symbolt *symbol_ptr)
Definition: c_nondet_symbol_factory.h:58
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:18
source_locationt
Definition: source_location.h:19
symbol_factoryt::gen_nondet_init
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 ...
Definition: c_nondet_symbol_factory.cpp:35
symbol_factoryt::loc
const source_locationt & loc
Definition: c_nondet_symbol_factory.h:25
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_factoryt::allocate_objects
allocate_objectst allocate_objects
Definition: c_nondet_symbol_factory.h:29
symbol_factoryt::lifetime
const lifetimet lifetime
Definition: c_nondet_symbol_factory.h:31
symbol_factoryt::symbol_table
symbol_tablet & symbol_table
Definition: c_nondet_symbol_factory.h:24
allocate_objectst
Definition: allocate_objects.h:28
allocate_objectst::mark_created_symbols_as_input
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
Definition: allocate_objects.cpp:244
symbol_factoryt
Definition: c_nondet_symbol_factory.h:23
symbol_factoryt::recursion_sett
std::set< irep_idt > recursion_sett
Definition: c_nondet_symbol_factory.h:34
symbol_table.h
Author: Diffblue Ltd.
symbol_factoryt::mark_created_symbols_as_input
void mark_created_symbols_as_input(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:68
allocate_objects.h
symbol_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:63