Rebase and address review comments

Author: Sonny Martin

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -550,7 +550,10 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      goto_model.validate(validation_modet::INVARIANT);
+      goto_model.validate(
+        validation_modet::INVARIANT,
+        goto_model_validation_optionst{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     if(
@@ -691,7 +694,10 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      lazy_goto_model.validate(validation_modet::INVARIANT);
+      lazy_goto_model.validate(
+        validation_modet::INVARIANT,
+        goto_model_validation_optionst{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     // Provide show-goto-functions and similar dump functions after symex

src/cbmc/cbmc_parse_options.cpp

@@ -46,10 +46,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/stop_on_fail_verifier.h>
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
-#include <goto-instrument/cover.h>
-#include <goto-instrument/full_slicer.h>
-#include <goto-instrument/nondet_static.h>
-#include <goto-instrument/reachability_slicer.h>
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -60,9 +56,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
@@ -75,6 +68,11 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/validate_goto_model.h>
 
+#include <goto-instrument/cover.h>
+#include <goto-instrument/full_slicer.h>
+#include <goto-instrument/nondet_static.h>
+#include <goto-instrument/reachability_slicer.h>
+
 #include <goto-symex/path_storage.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
@@ -553,12 +551,10 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model_validation_optionst goto_model_validation_options{true};
-    // this option is temporarily disabled until all source locations
-    // are reliably set correctly
-    goto_model_validation_options.check_source_location = false;
     goto_model.validate(
-      validation_modet::INVARIANT, goto_model_validation_options);
+      validation_modet::INVARIANT,
+      goto_model_validation_optionst{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   if(

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -407,7 +407,9 @@ int goto_analyzer_parse_optionst::doit()
   if(cmdline.isset("validate-goto-model"))
   {
     goto_model.validate(
-      validation_modet::INVARIANT, goto_model_validation_optionst{});
+      validation_modet::INVARIANT,
+      goto_model_validation_optionst{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   // show it?

src/goto-cc/compile.cpp

@@ -35,6 +35,7 @@ Date: June 2006
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/read_goto_binary.h>
+#include <goto-programs/validate_goto_model.h>
 #include <goto-programs/write_goto_binary.h>
 
 #include <langapi/language_file.h>
@@ -546,7 +547,10 @@ bool compilet::write_bin_object_file(
   if(validate_goto_model)
   {
     status() << "Validating goto model" << eom;
-    src_goto_model.validate(validation_modet::INVARIANT);
+    src_goto_model.validate(
+      validation_modet::INVARIANT,
+      goto_model_validation_optionst{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   statistics() << "Writing binary format object `"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -28,12 +28,12 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/interpreter.h>
 #include <goto-programs/link_to_library.h>
-#include <goto-programs/remove_returns.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -136,7 +136,9 @@ int goto_instrument_parse_optionst::doit()
       if(validate_only || cmdline.isset("validate-goto-model"))
       {
         goto_model.validate(
-          validation_modet::EXCEPTION, goto_model_validation_optionst{});
+          validation_modet::EXCEPTION,
+          goto_model_validation_optionst{
+            goto_model_validation_optionst::set_optionst::all_true});
 
         if(validate_only)
         {
@@ -150,7 +152,9 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("validate-goto-model"))
     {
       goto_model.validate(
-        validation_modet::INVARIANT, goto_model_validation_optionst{});
+        validation_modet::INVARIANT,
+        goto_model_validation_optionst{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     {

src/goto-programs/abstract_goto_model.h

@@ -57,7 +57,8 @@ class abstract_goto_modelt
   // virtual void validate(const validation_modet vm) const = 0;
   virtual void validate(
     const validation_modet vm,
-    const goto_model_validation_optionst &goto_model_validation_options) const = 0;
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const = 0;
 };
 
 #endif

src/goto-programs/goto_function.cpp

@@ -72,4 +72,3 @@ void goto_functiont::validate(
 
   validate_full_type(type, ns, vm);
 }
-

src/goto-programs/goto_functions.h

@@ -16,7 +16,6 @@ Date: June 2003
 
 #include "goto_function.h"
 
-#include "validate_goto_model.h"
 #include <util/cprover_prefix.h>
 
 /// A collection of goto functions
@@ -117,7 +116,6 @@ class goto_functionst
     const validation_modet vm,
     const goto_model_validation_optionst &goto_model_validation_options) const
   {
-    validate_goto_model(*this, vm, goto_model_validation_options);
     for(const auto &entry : function_map)
     {
       const goto_functiont &goto_function = entry.second;

src/goto-programs/goto_model.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
+#include "validate_goto_model.h"
 
 // A model is a pair consisting of a symbol table
 // and the CFGs for the functions.
@@ -96,10 +97,16 @@ class goto_modelt : public abstract_goto_modelt
   /// reported via DATA_INVARIANT violations or exceptions.
   void validate(
     const validation_modet vm,
-    const goto_model_validation_optionst &goto_model_validation_options) const override
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const override
   {
     symbol_table.validate(vm);
 
+    // Does a number of checks at the function_mapt level to ensure the
+    // goto_program is well formed. Does not call any validate methods
+    // (at the goto_functiont level or below)
+    validate_goto_model(goto_functions, vm, goto_model_validation_options);
+
     const namespacet ns(symbol_table);
     goto_functions.validate(ns, vm, goto_model_validation_options);
   }
@@ -146,12 +153,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt
   /// reported via DATA_INVARIANT violations or exceptions.
   void validate(
     const validation_modet vm,
-    const goto_model_validation_optionst &goto_model_validation_options) const override
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const override
   {
     symbol_table.validate(vm);
 
+    // Does a number of checks at the function_mapt level to ensure the
+    // goto_program is well formed. Does not call any validate methods
+    // (at the goto_functiont level or below)
+    validate_goto_model(goto_functions, vm, goto_model_validation_options);
+
     const namespacet ns(symbol_table);
-    goto_functions.validate(ns, vm,  goto_model_validation_options);
+    goto_functions.validate(ns, vm, goto_model_validation_options);
   }
 
 private:

src/goto-programs/goto_program.cpp

@@ -777,6 +777,8 @@ void goto_programt::instructiont::validate(
       }
     };
 
+  // this option is always set to false until all source locations
+  // are reliably set correctly (future work)
   if(goto_model_validation_options.check_source_location)
   {
     DATA_CHECK(
@@ -787,13 +789,13 @@ void goto_programt::instructiont::validate(
     DATA_CHECK(
       vm,
       code.source_location().is_not_nil(),
-      "each instruction \"code\" field, must have non nil source location");
+      "each instruction code field, must have non nil source location");
 
     DATA_CHECK(
       vm,
       source_location == code.source_location(),
       "instruction source location and"
-      " instruction \"code\" field source location must be the same");
+      " instruction code field source location must be the same");
   }
 
   const symbolt *table_symbol;

src/goto-programs/initialize_goto_model.cpp

@@ -194,8 +194,14 @@ goto_modelt initialize_goto_model(
 
   if(options.is_set("validate-goto-model"))
   {
+    goto_model_validation_optionst goto_model_validation_options{
+      goto_model_validation_optionst ::set_optionst::all_false};
+
+    // temporarily disabled until regression tests fixed
+    goto_model_validation_options.entry_point_exists = false;
+
     goto_model.validate(
-      validation_modet::EXCEPTION, goto_model_validation_optionst{});
+      validation_modet::INVARIANT, goto_model_validation_options);
   }
 
   // stupid hack

src/goto-programs/lazy_goto_model.h

@@ -249,7 +249,8 @@ class lazy_goto_modelt : public abstract_goto_modelt
   /// reported via DATA_INVARIANT violations or exceptions.
   void validate(
     const validation_modet vm,
-    const goto_model_validation_optionst &goto_model_validation_options) const override
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const override
   {
     goto_model->validate(vm, goto_model_validation_options);
   }