Adapt cproverNondetInitialize call for static case

smowton · Nov 20, 2017 · 4fd14b2 · 4fd14b2
1 parent 6d2d6c4
commit 4fd14b2
Showing 1 changed file with 5 additions and 8 deletions.
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
@@ -1043,15 +1043,12 @@ void java_object_factoryt::gen_nondet_struct_init(
   if(const auto func = symbol_table.lookup(validate_method_name))
   {
     const code_typet &type = to_code_type(func->type);
-    if(type.has_this() && type.parameters().size() == 1)
-    {
-      code_function_callt fun_call;
-      fun_call.function() = func->symbol_expr();
+    code_function_callt fun_call;
+    fun_call.function() = func->symbol_expr();
+    if(type.has_this())
       fun_call.arguments().push_back(address_of_exprt(expr));
-      assignments.add(fun_call);
-    }
-    else
-      throw "cproverNondetInitialize should be a non-static function";
+
+    assignments.add(fun_call);
   }
 }