@@ -147,11 +147,6 @@ class java_object_factoryt
147
147
size_t depth,
148
148
const source_locationt &location);
149
149
150
- void gen_method_call_if_present (
151
- code_blockt &assignments,
152
- const exprt &instance_expr,
153
- const irep_idt &method_name);
154
-
155
150
void array_primitive_init_code (
156
151
code_blockt &assignments,
157
152
const exprt &init_array_expr,
@@ -582,7 +577,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
582
577
{
583
578
const irep_idt &class_name = class_type->get_name ();
584
579
const irep_idt class_clinit = clinit_wrapper_name (class_name);
585
- gen_method_call_if_present (assignments, expr, class_clinit);
580
+ if (const auto clinit_func = symbol_table.lookup (class_clinit))
581
+ assignments.add (code_function_callt{clinit_func->symbol_expr ()});
586
582
}
587
583
}
588
584
@@ -948,7 +944,9 @@ void java_object_factoryt::gen_nondet_struct_init(
948
944
949
945
const irep_idt init_method_name =
950
946
" java::" + id2string (struct_tag) + " .cproverNondetInitialize:()V" ;
951
- gen_method_call_if_present (assignments, expr, init_method_name);
947
+ if (const auto init_func = symbol_table.lookup (init_method_name))
948
+ assignments.add (
949
+ code_function_callt{init_func->symbol_expr (), {address_of_exprt{expr}}});
952
950
}
953
951
954
952
// / Initializes a primitive-typed or reference-typed object tree rooted at
@@ -1623,24 +1621,3 @@ void gen_nondet_init(
1623
1621
update_in_place,
1624
1622
log );
1625
1623
}
1626
-
1627
- // / Adds a call for the given method to the end of `assignments` if the method
1628
- // / exists in the symbol table. Does nothing if the method does not exist.
1629
- // / \param assignments: A code block that the method call will be appended to.
1630
- // / \param instance_expr: The instance to call the method on. This argument is
1631
- // / ignored if the method is static.
1632
- // / \param method_name: The name of the method to be called.
1633
- void java_object_factoryt::gen_method_call_if_present (
1634
- code_blockt &assignments,
1635
- const exprt &instance_expr,
1636
- const irep_idt &method_name)
1637
- {
1638
- if (const auto func = symbol_table.lookup (method_name))
1639
- {
1640
- const java_method_typet &type = to_java_method_type (func->type );
1641
- code_function_callt fun_call (func->symbol_expr ());
1642
- if (type.has_this ())
1643
- fun_call.arguments ().push_back (address_of_exprt (instance_expr));
1644
- assignments.add (fun_call);
1645
- }
1646
- }
0 commit comments