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/allocate_objects.h>
78 #include <util/message.h>
79 #include <util/nondet.h>
80 #include <util/std_code.h>
81 #include <util/symbol_table.h>
82 
84  const typet &type,
85  const irep_idt base_name,
86  code_blockt &init_code,
87  symbol_table_baset &symbol_table,
89  lifetimet lifetime,
90  const source_locationt &location,
91  const select_pointer_typet &pointer_type_selector,
92  message_handlert &log);
93 
95  const typet &type,
96  const irep_idt base_name,
97  code_blockt &init_code,
98  symbol_tablet &symbol_table,
99  const java_object_factory_parameterst &object_factory_parameters,
100  lifetimet lifetime,
101  const source_locationt &location,
102  message_handlert &log);
103 
105 {
109 };
110 
111 void gen_nondet_init(
112  const exprt &expr,
113  code_blockt &init_code,
114  symbol_table_baset &symbol_table,
115  const source_locationt &loc,
116  bool skip_classid,
117  lifetimet lifetime,
118  const java_object_factory_parameterst &object_factory_parameters,
119  const select_pointer_typet &pointer_type_selector,
120  update_in_placet update_in_place,
121  message_handlert &log);
122 
123 void gen_nondet_init(
124  const exprt &expr,
125  code_blockt &init_code,
126  symbol_table_baset &symbol_table,
127  const source_locationt &loc,
128  bool skip_classid,
129  lifetimet lifetime,
130  const java_object_factory_parameterst &object_factory_parameters,
131  update_in_placet update_in_place,
132  message_handlert &log);
133 
134 using array_element_generatort = std::function<
135  code_blockt(const exprt &element_at_counter, const typet &element_type)>;
136 
160  const exprt &expr,
161  update_in_placet update_in_place,
162  const source_locationt &location,
163  const array_element_generatort &element_generator,
164  const allocate_local_symbolt &allocate_local_symbol,
165  const symbol_tablet &symbol_table,
166  size_t max_nondet_array_length);
167 
168 #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: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
java_bytecode_language.h
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
update_in_placet::MAY_UPDATE_IN_PLACE
@ MAY_UPDATE_IN_PLACE
typet
The type of an expression, extends irept.
Definition: type.h:29
exprt
Base class for all expressions.
Definition: expr.h:53
update_in_placet
update_in_placet
Definition: java_object_factory.h:105
update_in_placet::MUST_UPDATE_IN_PLACE
@ MUST_UPDATE_IN_PLACE
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, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
Definition: java_object_factory.cpp:1624
gen_nondet_array_init
code_blockt gen_nondet_array_init(const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table, size_t max_nondet_array_length)
Synthesize GOTO for generating a array of nondet length to be stored in the expr.
Definition: java_object_factory.cpp:1367
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, lifetimet lifetime, const source_locationt &location, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
Definition: java_object_factory.cpp:1537
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
select_pointer_typet
Definition: select_pointer_type.h:26
message_handlert
Definition: message.h:28
std_code.h
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:21
source_locationt
Definition: source_location.h:20
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:19
nondet.h
update_in_placet::NO_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
symbol_table.h
Author: Diffblue Ltd.
message.h
array_element_generatort
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort
Definition: java_object_factory.h:135
allocate_objects.h
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16