cprover
Loading...
Searching...
No Matches
c_nondet_symbol_factory.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C Nondet Symbol Factory
4
5Author: 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
34public:
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
74private:
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
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Author: Diffblue Ltd.