CBMC
Loading...
Searching...
No Matches
java_object_factory.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
84
86 const typet &type,
87 const irep_idt base_name,
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,
100 symbol_table_baset &symbol_table,
101 const java_object_factory_parameterst &object_factory_parameters,
102 lifetimet lifetime,
103 const source_locationt &location,
105
112
113void gen_nondet_init(
114 const exprt &expr,
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,
124
125void gen_nondet_init(
126 const exprt &expr,
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,
135
136using array_element_generatort = std::function<
137 code_blockt(const exprt &element_at_counter, const typet &element_type)>;
138
162 const exprt &expr,
164 const source_locationt &location,
167 const symbol_table_baset &symbol_table,
169
170#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
lifetimet
Selects the kind of objects allocated.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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...
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:2449
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition nondet.h:18
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.