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

Author: danpoe

src/cbmc/cbmc_parse_options.cpp

@@ -530,6 +530,12 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    const 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);
 }
@@ -977,6 +983,9 @@ 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)
+    " --validate-goto-model        enable additional well-formedness checks on the\n"
+    "                              goto program\n"
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -73,6 +73,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/initialize_goto_model.cpp

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