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 <set>
18 #include <vector>
19 
20 #include <util/allocate_objects.h>
21 #include <util/std_code.h>
22 #include <util/symbol_table.h>
23 
25 {
30 
32 
34 
35 public:
36  typedef std::set<irep_idt> recursion_sett;
37 
39  symbol_tablet &_symbol_table,
40  const source_locationt &loc,
41  const irep_idt &name_prefix,
43  const lifetimet lifetime)
44  : symbol_table(_symbol_table),
45  loc(loc),
46  ns(_symbol_table),
48  allocate_objects(ID_C, loc, name_prefix, symbol_table),
50  {
51  }
52 
53  void gen_nondet_init(
54  code_blockt &assignments,
55  const exprt &expr,
56  const std::size_t depth = 0,
57  recursion_sett recursion_set = recursion_sett(),
58  const bool assign_const = true);
59 
60  void add_created_symbol(const symbolt *symbol_ptr)
61  {
63  }
64 
66  {
68  }
69 
71  {
73  }
74 
75 private:
83  code_blockt &assignments,
84  const exprt &expr,
85  std::size_t depth,
86  const recursion_sett &recursion_set);
87 };
88 
90  code_blockt &init_code,
91  symbol_tablet &symbol_table,
92  const irep_idt base_name,
93  const typet &type,
94  const source_locationt &,
95  const c_object_factory_parameterst &object_factory_parameters,
96  const lifetimet lifetime);
97 
98 #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:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
typet
The type of an expression, extends irept.
Definition: type.h:29
symbol_factoryt::object_factory_params
const c_object_factory_parameterst & object_factory_params
Definition: c_nondet_symbol_factory.h:29
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:53
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:166
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:38
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:200
symbol_factoryt::ns
namespacet ns
Definition: c_nondet_symbol_factory.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
c_object_factory_parameters.h
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:60
std_code.h
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:21
source_locationt
Definition: source_location.h:20
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:37
symbol_factoryt::loc
const source_locationt & loc
Definition: c_nondet_symbol_factory.h:27
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_factoryt::allocate_objects
allocate_objectst allocate_objects
Definition: c_nondet_symbol_factory.h:31
symbol_factoryt::lifetime
const lifetimet lifetime
Definition: c_nondet_symbol_factory.h:33
symbol_factoryt::symbol_table
symbol_tablet & symbol_table
Definition: c_nondet_symbol_factory.h:26
allocate_objectst
Definition: allocate_objects.h:31
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:25
symbol_factoryt::recursion_sett
std::set< irep_idt > recursion_sett
Definition: c_nondet_symbol_factory.h:36
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:70
allocate_objects.h
symbol_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:65