cprover
java_object_factory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
70 
71 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
72 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
73 
74 #include "java_bytecode_language.h"
75 #include "select_pointer_type.h"
76 
77 #include <util/message.h>
78 #include <util/std_code.h>
79 #include <util/symbol_table.h>
80 
82 enum class allocation_typet
83 {
85  GLOBAL,
87  LOCAL,
89  DYNAMIC
90 };
91 
93  const typet &type,
94  const irep_idt base_name,
95  code_blockt &init_code,
96  symbol_table_baset &symbol_table,
98  allocation_typet alloc_type,
99  const source_locationt &location,
100  const select_pointer_typet &pointer_type_selector);
101 
103  const typet &type,
104  const irep_idt base_name,
105  code_blockt &init_code,
106  symbol_tablet &symbol_table,
107  const java_object_factory_parameterst &object_factory_parameters,
108  allocation_typet alloc_type,
109  const source_locationt &location);
110 
112 {
116 };
117 
118 void gen_nondet_init(
119  const exprt &expr,
120  code_blockt &init_code,
121  symbol_table_baset &symbol_table,
122  const source_locationt &loc,
123  bool skip_classid,
124  allocation_typet alloc_type,
125  const java_object_factory_parameterst &object_factory_parameters,
126  const select_pointer_typet &pointer_type_selector,
127  update_in_placet update_in_place);
128 
129 void gen_nondet_init(
130  const exprt &expr,
131  code_blockt &init_code,
132  symbol_table_baset &symbol_table,
133  const source_locationt &loc,
134  bool skip_classid,
135  allocation_typet alloc_type,
136  const java_object_factory_parameterst &object_factory_parameters,
137  update_in_placet update_in_place);
138 
140  const exprt &target_expr,
141  const typet &allocate_type,
142  symbol_table_baset &symbol_table,
143  const source_locationt &loc,
144  const irep_idt &function_id,
145  code_blockt &output_code,
146  std::vector<const symbolt *> &symbols_created,
147  bool cast_needed = false);
148 
150  const exprt &target_expr,
151  symbol_table_baset &symbol_table,
152  const source_locationt &loc,
153  const irep_idt &function_id,
154  code_blockt &output_code);
155 
156 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
object_factory
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, allocation_typet alloc_type, const source_locationt &location, const select_pointer_typet &pointer_type_selector)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
Definition: java_object_factory.cpp:1590
java_bytecode_language.h
allocate_dynamic_object_with_decl
exprt allocate_dynamic_object_with_decl(const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
Generates code for allocating a dynamic object.
Definition: java_object_factory.cpp:251
select_pointer_type.h
allocation_typet::GLOBAL
Allocate global objects.
update_in_placet::MAY_UPDATE_IN_PLACE
typet
The type of an expression, extends irept.
Definition: type.h:27
allocation_typet::LOCAL
Allocate local stacked objects.
exprt
Base class for all expressions.
Definition: expr.h:54
update_in_placet
update_in_placet
Definition: java_object_factory.h:111
update_in_placet::MUST_UPDATE_IN_PLACE
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
select_pointer_typet
Definition: select_pointer_type.h:28
std_code.h
source_locationt
Definition: source_location.h:20
gen_nondet_init
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
Definition: java_object_factory.cpp:1681
allocate_dynamic_object
exprt allocate_dynamic_object(const exprt &target_expr, const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code, std::vector< const symbolt * > &symbols_created, bool cast_needed=false)
Generates code for allocating a dynamic object.
Definition: java_object_factory.cpp:187
update_in_placet::NO_UPDATE_IN_PLACE
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4256
allocation_typet
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
Definition: java_object_factory.h:82
symbol_table.h
Author: Diffblue Ltd.
message.h
allocation_typet::DYNAMIC
Allocate dynamic objects (using MALLOC)
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:14