Skip to content

Commit 4fd14b2

Browse files
Adapt cproverNondetInitialize call for static case
1 parent 6d2d6c4 commit 4fd14b2

File tree

1 file changed

+5
-8
lines changed

1 file changed

+5
-8
lines changed

src/java_bytecode/java_object_factory.cpp

+5-8
Original file line numberDiff line numberDiff line change
@@ -1043,15 +1043,12 @@ void java_object_factoryt::gen_nondet_struct_init(
10431043
if(const auto func = symbol_table.lookup(validate_method_name))
10441044
{
10451045
const code_typet &type = to_code_type(func->type);
1046-
if(type.has_this() && type.parameters().size() == 1)
1047-
{
1048-
code_function_callt fun_call;
1049-
fun_call.function() = func->symbol_expr();
1046+
code_function_callt fun_call;
1047+
fun_call.function() = func->symbol_expr();
1048+
if(type.has_this())
10501049
fun_call.arguments().push_back(address_of_exprt(expr));
1051-
assignments.add(fun_call);
1052-
}
1053-
else
1054-
throw "cproverNondetInitialize should be a non-static function";
1050+
1051+
assignments.add(fun_call);
10551052
}
10561053
}
10571054

0 commit comments

Comments
 (0)