Validate goto models in cbmc (if enabled via command line flag)

Author: danpoe

src/cbmc/cbmc_parse_options.cpp

@@ -530,6 +530,11 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::INVARIANT);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -977,6 +982,8 @@ 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"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/validation_interface.h>
 
 #include <langapi/language.h>
 
@@ -73,6 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  OPT_VALIDATE \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-programs/initialize_goto_model.cpp

@@ -165,6 +165,11 @@ goto_modelt initialize_goto_model(
     goto_model.goto_functions,
     message_handler);
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::EXCEPTION);
+  }
+
   // stupid hack
   config.set_object_bits_from_symbol_table(
     goto_model.symbol_table);