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

@@ -64,8 +64,9 @@ class lazy_goto_modelt : public can_produce_functiont
     message_handlert &message_handler)
   {
     return lazy_goto_modelt(
-      [&handler] (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
-        handler.process_goto_function(fun, cpf);
+      [&handler, &options]
+      (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
+        handler.process_goto_function(fun, cpf, options);
       },
       [&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*)
         return handler.process_goto_functions(goto_model, options);

src/jbmc/jbmc_parse_options.cpp

@@ -643,9 +643,11 @@ int jbmc_parse_optionst::get_goto_program(
 
 void jbmc_parse_optionst::process_goto_function(
   goto_model_functiont &function,
-  const can_produce_functiont &available_functions)
+  const can_produce_functiont &available_functions,
+  const optionst &options)
 {
   symbol_tablet &symbol_table = function.get_symbol_table();
+  namespacet ns(symbol_table);
   goto_functionst::goto_functiont &goto_function = function.get_goto_function();
   try
   {
@@ -688,6 +690,9 @@ void jbmc_parse_optionst::process_goto_function(
       function,
       get_message_handler(),
       factory_params);
+
+    // add generic checks
+    goto_check(ns, options, ID_java, function.get_goto_function());
   }
 
   catch(const char *e)
@@ -725,10 +730,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

@@ -86,7 +86,8 @@ class jbmc_parse_optionst:
 
   void process_goto_function(
     goto_model_functiont &function,
-    const can_produce_functiont &);
+    const can_produce_functiont &,
+    const optionst &);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
 protected: