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

Author: danpoe

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -406,6 +406,11 @@ int goto_analyzer_parse_optionst::doit()
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::INVARIANT);
+  }
+
   // show it?
   if(cmdline.isset("show-symbol-table"))
   {
@@ -875,6 +880,7 @@ void goto_analyzer_parse_optionst::help()
     HELP_GOTO_CHECK
     "\n"
     "Other options:\n"
+    HELP_VALIDATE
     " --version                    show version and exit\n"
     HELP_FLUSH
     HELP_TIMESTAMP

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -101,9 +101,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
+#include <util/validation_interface.h>
 
 #include <langapi/language.h>
 
@@ -148,6 +149,7 @@ class optionst;
   "(show)(verify)(simplify):" \
   "(location-sensitive)(concurrent)" \
   "(no-simplify-slicing)" \
+  OPT_VALIDATE \
 // clang-format on
 
 class goto_analyzer_parse_optionst: