Skip to content

Commit 26ef690

Browse files
Goto program should not use java_method_typet
1 parent 5109733 commit 26ef690

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@
77
88
\*******************************************************************/
99

10-
#include <java_bytecode/java_types.h>
11-
1210
#include <testing-utils/catch.hpp>
1311
#include <java-testing-utils/load_java_class.h>
1412

@@ -135,8 +133,9 @@ SCENARIO(
135133
call.function() = callee;
136134
// Specific argument doesn't matter, so just pass an appropriately typed
137135
// null pointer:
138-
call.arguments().push_back(null_pointer_exprt(to_pointer_type(
139-
to_java_method_type(callee.type()).parameters()[0].type())));
136+
call.arguments().push_back(
137+
null_pointer_exprt(
138+
to_pointer_type(to_code_type(callee.type()).parameters()[0].type())));
140139
virtual_call_inst->code = call;
141140

142141
test_program.add_instruction(END_FUNCTION);

0 commit comments

Comments
 (0)