@@ -106,7 +106,6 @@ class java_object_factoryt
106
106
code_blockt &assignments,
107
107
const exprt &expr,
108
108
bool is_sub,
109
- irep_idt class_identifier,
110
109
bool skip_classid,
111
110
lifetimet lifetime,
112
111
const optionalt<typet> &override_type,
@@ -132,7 +131,6 @@ class java_object_factoryt
132
131
code_blockt &assignments,
133
132
const exprt &expr,
134
133
bool is_sub,
135
- irep_idt class_identifier,
136
134
bool skip_classid,
137
135
lifetimet lifetime,
138
136
const struct_typet &struct_type,
@@ -262,7 +260,6 @@ void java_object_factoryt::gen_pointer_target_init(
262
260
assignments,
263
261
init_expr,
264
262
false , // is_sub
265
- " " , // class_identifier
266
263
false , // skip_classid
267
264
lifetime,
268
265
{}, // no override type
@@ -706,7 +703,6 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
706
703
assignments,
707
704
new_symbol_expr,
708
705
false , // is_sub
709
- " " , // class_identifier
710
706
false , // skip_classid
711
707
lifetime,
712
708
{}, // no override_type
@@ -754,8 +750,6 @@ alternate_casest get_string_input_values_code(
754
750
// / \param expr: Struct-typed lvalue expression to initialize
755
751
// / \param is_sub: If true, `expr` is a substructure of a larger object, which
756
752
// / in Java necessarily means a base class
757
- // / \param class_identifier: Name of the parent class. Used to initialize the
758
- // / `@class_identifier` among others
759
753
// / \param skip_classid: If true, skip initializing `@class_identifier`
760
754
// / \param lifetime: Lifetime of the allocated objects (AUTOMATIC_LOCAL,
761
755
// / STATIC_GLOBAL, or DYNAMIC)
@@ -771,7 +765,6 @@ void java_object_factoryt::gen_nondet_struct_init(
771
765
code_blockt &assignments,
772
766
const exprt &expr,
773
767
bool is_sub,
774
- irep_idt class_identifier,
775
768
bool skip_classid,
776
769
lifetimet lifetime,
777
770
const struct_typet &struct_type,
@@ -833,8 +826,7 @@ void java_object_factoryt::gen_nondet_struct_init(
833
826
// This code mirrors the `remove_java_new` pass:
834
827
auto initial_object = zero_initializer (expr.type (), source_locationt (), ns);
835
828
CHECK_RETURN (initial_object.has_value ());
836
- class_identifier = struct_tag;
837
- const irep_idt qualified_clsid = " java::" + id2string (class_identifier);
829
+ const irep_idt qualified_clsid = " java::" + id2string (struct_tag);
838
830
set_class_identifier (
839
831
to_struct_expr (*initial_object), ns, struct_tag_typet (qualified_clsid));
840
832
@@ -903,7 +895,6 @@ void java_object_factoryt::gen_nondet_struct_init(
903
895
assignments,
904
896
me,
905
897
_is_sub,
906
- class_identifier,
907
898
false , // skip_classid
908
899
lifetime,
909
900
{}, // no override_type
@@ -938,9 +929,6 @@ void java_object_factoryt::gen_nondet_struct_init(
938
929
// / \param is_sub:
939
930
// / If true, `expr` is a substructure of a larger object, which in Java
940
931
// / necessarily means a base class.
941
- // / \param class_identifier:
942
- // / Name of the parent class. Used to initialize the `@class_identifier` among
943
- // / others.
944
932
// / \param skip_classid:
945
933
// / If true, skip initializing `@class_identifier`.
946
934
// / \param lifetime:
@@ -965,7 +953,6 @@ void java_object_factoryt::gen_nondet_init(
965
953
code_blockt &assignments,
966
954
const exprt &expr,
967
955
bool is_sub,
968
- irep_idt class_identifier,
969
956
bool skip_classid,
970
957
lifetimet lifetime,
971
958
const optionalt<typet> &override_type,
@@ -1022,7 +1009,6 @@ void java_object_factoryt::gen_nondet_init(
1022
1009
assignments,
1023
1010
expr,
1024
1011
is_sub,
1025
- class_identifier,
1026
1012
skip_classid,
1027
1013
lifetime,
1028
1014
struct_type,
@@ -1245,7 +1231,6 @@ void java_object_factoryt::array_loop_init_code(
1245
1231
assignments,
1246
1232
arraycellref,
1247
1233
false , // is_sub
1248
- irep_idt (), // class_identifier
1249
1234
false , // skip_classid
1250
1235
// These are variable in number, so use dynamic allocator:
1251
1236
lifetimet::DYNAMIC,
@@ -1464,7 +1449,6 @@ exprt object_factory(
1464
1449
assignments,
1465
1450
object,
1466
1451
false , // is_sub
1467
- " " , // class_identifier
1468
1452
false , // skip_classid
1469
1453
lifetime,
1470
1454
{}, // no override_type
@@ -1535,7 +1519,6 @@ void gen_nondet_init(
1535
1519
assignments,
1536
1520
expr,
1537
1521
false , // is_sub
1538
- " " , // class_identifier
1539
1522
skip_classid,
1540
1523
lifetime,
1541
1524
{}, // no override_type
0 commit comments