|
25 | 25 | #include "java_types.h"
|
26 | 26 | #include "java_utils.h"
|
27 | 27 |
|
28 |
| -/*******************************************************************\ |
29 |
| -
|
30 |
| -Function: gen_nondet_init |
31 |
| -
|
32 |
| - Inputs: |
33 |
| -
|
34 |
| - Outputs: |
35 |
| -
|
36 |
| - Purpose: |
37 |
| -
|
38 |
| -\*******************************************************************/ |
39 |
| - |
40 | 28 | class java_object_factoryt:public messaget
|
41 | 29 | {
|
42 | 30 | code_blockt &init_code;
|
@@ -81,19 +69,15 @@ class java_object_factoryt:public messaget
|
81 | 69 | const typet &override_type=empty_typet());
|
82 | 70 | };
|
83 | 71 |
|
84 |
| - |
85 | 72 | /*******************************************************************\
|
86 | 73 |
|
87 |
| -Function: gen_nondet_array_init |
| 74 | +Function: java_object_factoryt::allocate_object |
88 | 75 |
|
89 |
| - Inputs: the target expression, desired object type, source location |
90 |
| - and Boolean whether to create a dynamic object |
| 76 | + Inputs: |
91 | 77 |
|
92 |
| - Outputs: the allocated object |
| 78 | + Outputs: |
93 | 79 |
|
94 |
| - Purpose: Returns false if we can't figure out the size of allocate_type. |
95 |
| - allocate_type may differ from target_expr, e.g. for target_expr |
96 |
| - having type int* and allocate_type being an int[10]. |
| 80 | + Purpose: |
97 | 81 |
|
98 | 82 | \*******************************************************************/
|
99 | 83 |
|
@@ -165,10 +149,29 @@ exprt java_object_factoryt::allocate_object(
|
165 | 149 | }
|
166 | 150 | }
|
167 | 151 |
|
168 |
| -// Override type says to ignore the LHS' real type, and init it with the given |
169 |
| -// type regardless. Used at the moment for reference arrays, which are |
170 |
| -// implemented as void* arrays but should be init'd as their true type with |
171 |
| -// appropriate casts. |
| 152 | +/*******************************************************************\ |
| 153 | +
|
| 154 | +Function: java_object_factoryt::gen_nondet_init |
| 155 | +
|
| 156 | + Inputs: |
| 157 | + expr - |
| 158 | + is_sub - |
| 159 | + class_identifier - |
| 160 | + loc - |
| 161 | + skip_classid - |
| 162 | + create_dynamic_objects - |
| 163 | + override - Ignore the LHS' real type. Used at the moment for |
| 164 | + reference arrays, which are implemented as void* |
| 165 | + arrays but should be init'd as their true type with |
| 166 | + appropriate casts. |
| 167 | + override_type - Type to use if ignoring the LHS' real type |
| 168 | +
|
| 169 | + Outputs: |
| 170 | +
|
| 171 | + Purpose: |
| 172 | +
|
| 173 | +\*******************************************************************/ |
| 174 | + |
172 | 175 | void java_object_factoryt::gen_nondet_init(
|
173 | 176 | const exprt &expr,
|
174 | 177 | bool is_sub,
|
@@ -343,7 +346,7 @@ void java_object_factoryt::gen_nondet_init(
|
343 | 346 |
|
344 | 347 | /*******************************************************************\
|
345 | 348 |
|
346 |
| -Function: gen_nondet_array_init |
| 349 | +Function: java_object_factoryt::gen_nondet_array_init |
347 | 350 |
|
348 | 351 | Inputs:
|
349 | 352 |
|
|
0 commit comments