JBMC: add property checks on a per-function basis

Author: smowton

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/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
       {

src/jbmc/jbmc_parse_options.cpp

@@ -636,7 +636,8 @@ int jbmc_parse_optionst::get_goto_program(
 }
 
 void jbmc_parse_optionst::process_goto_function(
-  goto_model_functiont &function)
+  goto_model_functiont &function,
+  const optionst &options)
 {
   symbol_tablet &symbol_table = function.get_symbol_table();
   goto_functionst::goto_functiont &goto_function = function.get_goto_function();
@@ -675,6 +676,13 @@ void jbmc_parse_optionst::process_goto_function(
       function,
       get_message_handler(),
       factory_params);
+
+    // add generic checks
+    goto_check(
+      namespacet(function.get_symbol_table()),
+      options,
+      ID_java,
+      function.get_goto_function());
   }
 
   catch(const char *e)
@@ -712,10 +720,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
-    goto_check(options, goto_model);
-
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
 

src/jbmc/jbmc_parse_options.h

@@ -80,7 +80,8 @@ class jbmc_parse_optionst:
     const char **argv,
     const std::string &extra_options);
 
-  void process_goto_function(goto_model_functiont &function);
+  void process_goto_function(
+    goto_model_functiont &function, const optionst &options);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
 protected: