Reworked based on PR #3123

Using DATA_CHECK instead of calling error handling directly.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -515,10 +515,6 @@ int cbmc_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
-  INVARIANT(
-    !goto_model.check_internal_invariants(*this),
-    "goto program internal invariants failed");
-
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
@@ -530,6 +526,12 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    namespacet ns(goto_model.symbol_table);
+    goto_model.validate(ns, validation_modet::INVARIANT);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -976,6 +978,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --validate-goto-model        enables additional well-formedness checks on the goto program\n" // NOLINT(*)
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -72,6 +72,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  "(validate-goto-model)" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-programs/goto_model.h

@@ -100,29 +100,19 @@ class goto_modelt : public abstract_goto_modelt
 
   /// Iterates over the functions inside the goto model and checks invariants
   /// in all of them. Prints out error message collected.
-  /// \param msg message instance to collect errors
-  /// \return true if any violation was found
-  bool check_internal_invariants(messaget &msg) const
+  /// \param ns namespace for the environment
+  /// \param vm validation mode to be used for error reporting
+  void validate(const namespacet &ns, const validation_modet &vm) const
   {
-    bool found_violation = false;
-    namespacet ns(symbol_table);
     forall_goto_functions(it, goto_functions)
     {
-      if(!base_type_eq(
-           it->second.type, symbol_table.lookup_ref(it->first).type, ns))
-      {
-        msg.error() << id2string(it->first) << " type inconsistency\n"
-                    << "goto program type: " << it->second.type.id_string()
-                    << "\nsymbol table type: "
-                    << symbol_table.lookup_ref(it->first).type.id_string()
-                    << messaget::eom;
-
-        msg.error() << "" << messaget::eom;
-        found_violation = true;
-      }
+      DATA_CHECK(
+        base_type_eq(
+          it->second.type, symbol_table.lookup_ref(it->first).type, ns),
+        id2string(it->first) + " type inconsistency\ngoto program type: " +
+          it->second.type.id_string() + "\nsymbol table type: " +
+          symbol_table.lookup_ref(it->first).type.id_string());
     }
-
-    return found_violation;
   }
 };
 

src/util/expr.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_EXPR_H
 
 #include "type.h"
+#include "validate.h"
 
 #include <functional>
 #include <list>