CBMC
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 <util/std_code.h>
75 
77 
78 #include "nondet.h"
79 
80 class message_handlert;
82 class symbol_table_baset;
84 
86  const typet &type,
87  const irep_idt base_name,
88  code_blockt &init_code,
89  symbol_table_baset &symbol_table,
91  lifetimet lifetime,
92  const source_locationt &location,
93  const select_pointer_typet &pointer_type_selector,
95 
97  const typet &type,
98  const irep_idt base_name,
99  code_blockt &init_code,
100  symbol_table_baset &symbol_table,
101  const java_object_factory_parameterst &object_factory_parameters,
102  lifetimet lifetime,
103  const source_locationt &location,
105 
107 {
111 };
112 
113 void gen_nondet_init(
114  const exprt &expr,
115  code_blockt &init_code,
116  symbol_table_baset &symbol_table,
117  const source_locationt &loc,
118  bool skip_classid,
119  lifetimet lifetime,
120  const java_object_factory_parameterst &object_factory_parameters,
121  const select_pointer_typet &pointer_type_selector,
122  update_in_placet update_in_place,
124 
125 void gen_nondet_init(
126  const exprt &expr,
127  code_blockt &init_code,
128  symbol_table_baset &symbol_table,
129  const source_locationt &loc,
130  bool skip_classid,
131  lifetimet lifetime,
132  const java_object_factory_parameterst &object_factory_parameters,
133  update_in_placet update_in_place,
135 
136 using array_element_generatort = std::function<
137  code_blockt(const exprt &element_at_counter, const typet &element_type)>;
138 
162  const exprt &expr,
163  update_in_placet update_in_place,
164  const source_locationt &location,
165  const array_element_generatort &element_generator,
166  const allocate_local_symbolt &allocate_local_symbol,
167  const symbol_table_baset &symbol_table,
168  size_t max_nondet_array_length);
169 
170 #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:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
The symbol table base class interface.
The type of an expression, extends irept.
Definition: type.h:29
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_table_baset &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...
double log(double x)
Definition: math.c:2776
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18