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 "goto_instruction_code.h"
13 
14 #include <util/namespace.h>
15 #include <util/source_location.h>
16 #include <util/std_code.h>
17 
19 enum class lifetimet
20 {
26  DYNAMIC
27 };
28 
30 {
31 public:
33  const irep_idt &symbol_mode,
35  const irep_idt &name_prefix,
42  {
43  }
44 
46  code_blockt &assignments,
47  const exprt &target_expr,
48  const typet &allocate_type,
49  const lifetimet lifetime,
50  const irep_idt &basename_prefix = "tmp");
51 
53  code_blockt &assignments,
54  const exprt &target_expr,
55  const typet &allocate_type,
56  const irep_idt &basename_prefix = "tmp");
57 
59  code_blockt &assignments,
60  const exprt &target_expr,
61  const typet &allocate_type,
62  const irep_idt &basename_prefix = "tmp");
63 
80  code_blockt &output_code,
81  const exprt &target_expr,
82  const typet &allocate_type);
83 
88  code_blockt &output_code,
89  const exprt &target_expr,
90  const typet &allocate_type);
91 
93  const typet &allocate_type,
94  const irep_idt &basename_prefix = "tmp");
95 
96  void add_created_symbol(const symbolt &symbol);
97 
98  void declare_created_symbols(code_blockt &init_code);
99 
101 
102 private:
106 
108  const namespacet ns;
109 
110  std::vector<irep_idt> symbols_created;
111 
113  code_blockt &assignments,
114  const exprt &target_expr,
115  const typet &allocate_type,
116  const bool static_lifetime,
117  const irep_idt &basename_prefix);
118 };
119 
125 make_allocate_code(const symbol_exprt &lhs, const exprt &size);
126 
127 #endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H
code_frontend_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
lifetimet
Selects the kind of objects allocated.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
void add_created_symbol(const symbolt &symbol)
Add a pointer to a symbol to the list of pointers to symbols created so far.
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)
allocate_objectst(const irep_idt &symbol_mode, const source_locationt &source_location, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
const namespacet ns
const irep_idt symbol_mode
std::vector< irep_idt > symbols_created
const irep_idt name_prefix
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,...
symbol_table_baset & symbol_table
const source_locationt source_location
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a 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...
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.
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
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.
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
A codet representing an assignment in the program.
Definition: std_code.h:24
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
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29