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
lifetimet
Selects the kind of objects allocated.
A codet representing sequential composition of program statements.
Definition: std_code.h:170
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
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:20
The type of an expression, extends irept.
Definition: type.h:28
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort
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...
update_in_placet
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.
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...
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:19
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
Author: Diffblue Ltd.