JBMC: add property checks on a per-function basis

src/analyses/goto_check.cpp

@@ -1753,10 +1753,11 @@ void goto_checkt::goto_check(
 void goto_check(
   const namespacet &ns,
   const optionst &options,
+  const irep_idt &mode,
   goto_functionst::goto_functiont &goto_function)
 {
   goto_checkt goto_check(ns, options);
-  goto_check.goto_check(goto_function, irep_idt());
+  goto_check.goto_check(goto_function, mode);
 }
 
 void goto_check(

src/analyses/goto_check.h

@@ -26,6 +26,7 @@ void goto_check(
 void goto_check(
   const namespacet &ns,
   const optionst &options,
+  const irep_idt &mode,
   goto_functionst::goto_functiont &goto_function);
 
 void goto_check(

src/goto-programs/convert_nondet.cpp

@@ -130,6 +130,20 @@ void convert_nondet(
   }
 }
 
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters)
+{
+  convert_nondet(
+    function.get_goto_function().body,
+    function.get_symbol_table(),
+    message_handler,
+    object_factory_parameters);
+
+  function.compute_location_numbers();
+}
+
 void convert_nondet(
   goto_functionst &goto_functions,
   symbol_tablet &symbol_table,

src/goto-programs/convert_nondet.h

@@ -17,6 +17,7 @@ Author: Reuben Thomas, [email protected]
 class goto_functionst;
 class symbol_tablet;
 class goto_modelt;
+class goto_model_functiont;
 class message_handlert;
 struct object_factory_parameterst;
 
@@ -38,4 +39,15 @@ void convert_nondet(
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation.
+/// \param function: goto program to modify
+/// \param message_handler: For error logging.
+/// \param object_factory_parameters: Parameters for the generation of nondet
+///   objects.
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters);
+
 #endif

src/goto-programs/lazy_goto_model.h

@@ -51,9 +51,9 @@ class lazy_goto_modelt
     message_handlert &message_handler)
   {
     return lazy_goto_modelt(
-      [&handler] (goto_model_functiont &function)
+      [&handler, &options] (goto_model_functiont &function)
       {
-        handler.process_goto_function(function);
+        handler.process_goto_function(function, options);
       },
       [&handler, &options] (goto_modelt &goto_model) -> bool
       {