Always load cprover-nondet-initialize

NathanJPhillips · Jun 4, 2018 · 971a34b · 971a34b
1 parent 8de6a33
commit 971a34b
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp
@@ -248,6 +248,17 @@ bool ci_lazy_methodst::operator()(
     }
   }
 
+  // cproverNondetInitialize has to be force-loaded for mocks to return valid
+  // objects (objects which satisfy invariants specified in the
+  // cproverNondetInitialize method)
+  for(const auto &class_name : instantiated_classes)
+  {
+    const irep_idt cprover_validate =
+      id2string(class_name) + ".cproverNondetInitialize:()V";
+    if(symbol_table.symbols.count(cprover_validate))
+      methods_already_populated.insert(cprover_validate);
+  }
+
   // Remove symbols for methods that were declared but never used:
   symbol_tablet keep_symbols;
   // Manually keep @inflight_exception, as it is unused at this stage