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 
67 
68 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
69 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
70 
71 #include "java_bytecode_language.h"
72 #include "select_pointer_type.h"
73 
74 #include <util/message.h>
75 #include <util/std_code.h>
76 #include <util/symbol_table.h>
77 
79 enum class allocation_typet
80 {
82  GLOBAL,
84  LOCAL,
86  DYNAMIC
87 };
88 
90  const typet &type,
91  const irep_idt base_name,
92  code_blockt &init_code,
93  symbol_table_baset &symbol_table,
94  object_factory_parameterst parameters,
95  allocation_typet alloc_type,
96  const source_locationt &location,
97  const select_pointer_typet &pointer_type_selector);
98 
100  const typet &type,
101  const irep_idt base_name,
102  code_blockt &init_code,
103  symbol_tablet &symbol_table,
104  const object_factory_parameterst &object_factory_parameters,
105  allocation_typet alloc_type,
106  const source_locationt &location);
107 
109 {
113 };
114 
115 void gen_nondet_init(
116  const exprt &expr,
117  code_blockt &init_code,
118  symbol_table_baset &symbol_table,
119  const source_locationt &loc,
120  bool skip_classid,
121  allocation_typet alloc_type,
122  const object_factory_parameterst &object_factory_parameters,
123  const select_pointer_typet &pointer_type_selector,
124  update_in_placet update_in_place);
125 
126 void gen_nondet_init(
127  const exprt &expr,
128  code_blockt &init_code,
129  symbol_table_baset &symbol_table,
130  const source_locationt &loc,
131  bool skip_classid,
132  allocation_typet alloc_type,
133  const object_factory_parameterst &object_factory_parameters,
134  update_in_placet update_in_place);
135 
137  const exprt &target_expr,
138  const typet &allocate_type,
139  symbol_table_baset &symbol_table,
140  const source_locationt &loc,
141  const irep_idt &function_id,
142  code_blockt &output_code,
143  std::vector<const symbolt *> &symbols_created,
144  bool cast_needed = false);
145 
147  const exprt &target_expr,
148  symbol_table_baset &symbol_table,
149  const source_locationt &loc,
150  const irep_idt &function_id,
151  code_blockt &output_code);
152 
154  const exprt &obj,
155  const std::size_t &max_nondet_string_length,
156  const source_locationt &loc,
157  const irep_idt &function_id,
158  symbol_table_baset &symbol_table,
159  bool printable);
160 
161 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
#define loc()
The type of an expression.
Definition: type.h:22
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
codet initialize_nondet_string_struct(const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialize a nondeterministic String structure.
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.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, 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...
Allocate local stacked objects.
Allocate global objects.
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 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...
The symbol table.
Definition: symbol_table.h:19
Author: Diffblue Ltd.
update_in_placet
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.
Allocate dynamic objects (using MALLOC)
Base class for all expressions.
Definition: expr.h:42
The symbol table base class interface.
Sequential composition.
Definition: std_code.h:88
A statement in a programming language.
Definition: std_code.h:21
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...