@@ -63,7 +63,6 @@ class java_object_factoryt:public messaget
63
63
bool is_sub,
64
64
irep_idt class_identifier,
65
65
const source_locationt &loc,
66
- bool skip_classid,
67
66
bool create_dynamic_objects,
68
67
bool override =false ,
69
68
const typet &override_type=empty_typet());
@@ -158,7 +157,6 @@ Function: java_object_factoryt::gen_nondet_init
158
157
is_sub -
159
158
class_identifier -
160
159
loc -
161
- skip_classid -
162
160
create_dynamic_objects -
163
161
override - Ignore the LHS' real type. Used at the moment for
164
162
reference arrays, which are implemented as void*
@@ -177,7 +175,6 @@ void java_object_factoryt::gen_nondet_init(
177
175
bool is_sub,
178
176
irep_idt class_identifier,
179
177
const source_locationt &loc,
180
- bool skip_classid,
181
178
bool create_dynamic_objects,
182
179
bool override ,
183
180
const typet &override_type)
@@ -263,7 +260,6 @@ void java_object_factoryt::gen_nondet_init(
263
260
false ,
264
261
" " ,
265
262
loc,
266
- false ,
267
263
create_dynamic_objects);
268
264
}
269
265
@@ -298,9 +294,6 @@ void java_object_factoryt::gen_nondet_init(
298
294
299
295
if (name==" @class_identifier" )
300
296
{
301
- if (skip_classid)
302
- continue ;
303
-
304
297
irep_idt qualified_clsid=" java::" +as_string (class_identifier);
305
298
constant_exprt ci (qualified_clsid, string_typet ());
306
299
code_assignt code (me, ci);
@@ -328,7 +321,6 @@ void java_object_factoryt::gen_nondet_init(
328
321
_is_sub,
329
322
class_identifier,
330
323
loc,
331
- false ,
332
324
create_dynamic_objects);
333
325
}
334
326
}
@@ -380,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init(
380
372
const auto &length_sym_expr=length_sym.symbol_expr ();
381
373
382
374
// Initialize array with some undetermined length:
383
- gen_nondet_init (length_sym_expr, false , irep_idt (), loc, false , false );
375
+ gen_nondet_init (length_sym_expr, false , irep_idt (), loc, false );
384
376
385
377
// Insert assumptions to bound its length:
386
378
binary_relation_exprt
@@ -465,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init(
465
457
false ,
466
458
irep_idt (),
467
459
loc,
468
- false ,
469
460
true ,
470
461
true ,
471
462
element_type);
@@ -495,7 +486,6 @@ void gen_nondet_init(
495
486
code_blockt &init_code,
496
487
symbol_tablet &symbol_table,
497
488
const source_locationt &loc,
498
- bool skip_classid,
499
489
bool create_dyn_objs,
500
490
bool assume_non_null,
501
491
message_handlert &message_handler,
@@ -512,7 +502,6 @@ void gen_nondet_init(
512
502
false ,
513
503
" " ,
514
504
loc,
515
- skip_classid,
516
505
create_dyn_objs);
517
506
}
518
507
@@ -599,7 +588,6 @@ exprt object_factory(
599
588
symbol_table,
600
589
loc,
601
590
false ,
602
- false ,
603
591
!allow_null,
604
592
message_handler,
605
593
max_nondet_array_length);
0 commit comments