@@ -123,6 +123,7 @@ class java_object_factoryt
123123 const exprt &expr,
124124 bool is_sub,
125125 irep_idt class_identifier,
126+ bool skip_classid,
126127 bool create_dynamic_objects,
127128 bool override ,
128129 const typet &override_type,
@@ -309,6 +310,7 @@ void java_object_factoryt::gen_pointer_target_init(
309310 init_expr,
310311 false ,
311312 " " ,
313+ false ,
312314 create_dynamic_objects,
313315 false ,
314316 typet (),
@@ -355,6 +357,7 @@ void java_object_factoryt::gen_nondet_init(
355357 const exprt &expr,
356358 bool is_sub,
357359 irep_idt class_identifier,
360+ bool skip_classid,
358361 bool create_dynamic_objects,
359362 bool override ,
360363 const typet &override_type,
@@ -483,6 +486,9 @@ void java_object_factoryt::gen_nondet_init(
483486 if (update_in_place==MUST_UPDATE_IN_PLACE)
484487 continue ;
485488
489+ if (skip_classid)
490+ continue ;
491+
486492 irep_idt qualified_clsid=" java::" +as_string (class_identifier);
487493 constant_exprt ci (qualified_clsid, string_typet ());
488494 code_assignt code (me, ci);
@@ -519,6 +525,7 @@ void java_object_factoryt::gen_nondet_init(
519525 me,
520526 _is_sub,
521527 class_identifier,
528+ false ,
522529 create_dynamic_objects,
523530 false ,
524531 typet (),
@@ -578,6 +585,7 @@ void java_object_factoryt::allocate_nondet_length_array(
578585 irep_idt (),
579586 false ,
580587 false ,
588+ false ,
581589 typet (),
582590 NO_UPDATE_IN_PLACE);
583591
@@ -718,6 +726,7 @@ void java_object_factoryt::gen_nondet_array_init(
718726 arraycellref,
719727 false ,
720728 irep_idt (),
729+ false ,
721730 true ,
722731 true ,
723732 element_type,
@@ -799,6 +808,7 @@ exprt object_factory(
799808 " " ,
800809 false ,
801810 false ,
811+ false ,
802812 typet (),
803813 NO_UPDATE_IN_PLACE);
804814
@@ -853,6 +863,7 @@ void gen_nondet_init(
853863 code_blockt &init_code,
854864 symbol_tablet &symbol_table,
855865 const source_locationt &loc,
866+ bool skip_classid,
856867 bool create_dyn_objs,
857868 bool assume_non_null,
858869 size_t max_nondet_array_length,
@@ -872,6 +883,7 @@ void gen_nondet_init(
872883 expr,
873884 false ,
874885 " " ,
886+ skip_classid,
875887 create_dyn_objs,
876888 false ,
877889 typet (),
0 commit comments