cprover
allocate_objects.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
10 #define CPROVER_UTIL_ALLOCATE_OBJECTS_H
11 
12 #include "expr.h"
13 #include "namespace.h"
14 #include "source_location.h"
15 #include "std_code.h"
16 #include "symbol_table.h"
17 #include "type.h"
18 
20 enum class lifetimet
21 {
27  DYNAMIC
28 };
29 
31 {
32 public:
34  const irep_idt &symbol_mode,
36  const irep_idt &name_prefix,
43  {
44  }
45 
47  code_blockt &assignments,
48  const exprt &target_expr,
49  const typet &allocate_type,
50  const lifetimet lifetime,
51  const irep_idt &basename_prefix = "tmp");
52 
54  code_blockt &assignments,
55  const exprt &target_expr,
56  const typet &allocate_type,
57  const irep_idt &basename_prefix = "tmp");
58 
60  code_blockt &assignments,
61  const exprt &target_expr,
62  const typet &allocate_type,
63  const irep_idt &basename_prefix = "tmp");
64 
81  code_blockt &output_code,
82  const exprt &target_expr,
83  const typet &allocate_type);
84 
89  code_blockt &output_code,
90  const exprt &target_expr,
91  const typet &allocate_type);
92 
94  const typet &allocate_type,
95  const irep_idt &basename_prefix = "tmp");
96 
97  void add_created_symbol(const symbolt *symbol_ptr);
98 
99  void declare_created_symbols(code_blockt &init_code);
100 
102 
103 private:
107 
109  const namespacet ns;
110 
111  std::vector<const symbolt *> symbols_created;
112 
114  code_blockt &assignments,
115  const exprt &target_expr,
116  const typet &allocate_type,
117  const bool static_lifetime,
118  const irep_idt &basename_prefix);
119 };
120 
125 code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size);
126 
127 #endif // CPROVER_UTIL_ALLOCATE_OBJECTS_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
lifetimet::AUTOMATIC_LOCAL
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
typet
The type of an expression, extends irept.
Definition: type.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
allocate_objectst::symbol_table
symbol_table_baset & symbol_table
Definition: allocate_objects.h:108
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
expr.h
allocate_objectst::symbol_mode
const irep_idt symbol_mode
Definition: allocate_objects.h:104
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
allocate_objectst::ns
const namespacet ns
Definition: allocate_objects.h:109
allocate_objectst::symbols_created
std::vector< const symbolt * > symbols_created
Definition: allocate_objects.h:111
allocate_objectst::allocate_dynamic_object_symbol
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
Definition: allocate_objects.cpp:124
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
allocate_objectst::allocate_static_global_object
exprt allocate_static_global_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a global variable with static lifetime.
Definition: allocate_objects.cpp:91
allocate_objectst::allocate_object
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
Definition: allocate_objects.cpp:32
source_location.h
make_allocate_code
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
Definition: allocate_objects.cpp:255
allocate_objectst::allocate_objectst
allocate_objectst(const irep_idt &symbol_mode, const source_locationt &source_location, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
Definition: allocate_objects.h:33
allocate_objectst::name_prefix
const irep_idt name_prefix
Definition: allocate_objects.h:106
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
allocate_objectst::source_location
const source_locationt source_location
Definition: allocate_objects.h:105
allocate_objectst::allocate_non_dynamic_object
exprt allocate_non_dynamic_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime, const irep_idt &basename_prefix)
Definition: allocate_objects.cpp:180
symbolt
Symbol table entry.
Definition: symbol.h:28
lifetimet::STATIC_GLOBAL
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
allocate_objectst
Definition: allocate_objects.h:31
allocate_objectst::allocate_dynamic_object
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
Definition: allocate_objects.cpp:171
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
allocate_objectst::allocate_automatic_local_object
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
Definition: allocate_objects.cpp:70
symbol_table.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295