JBMC: support validation

This invokes validation using the same arguments as CBMC.

Author: smowton

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -369,6 +369,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
 
+  if(cmdline.isset("validate-ssa-equation"))
+  {
+    options.set_option("validate-ssa-equation", true);
+  }
+
+  if(cmdline.isset("validate-goto-model"))
+  {
+    options.set_option("validate-goto-model", true);
+  }
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
   if(cmdline.isset("no-lazy-methods"))
@@ -553,6 +563,11 @@ int jbmc_parse_optionst::doit()
     if(set_properties(goto_model))
       return 7; // should contemplate EX_USAGE from sysexits.h
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      goto_model.validate(validation_modet::INVARIANT);
+    }
+
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
     return bmct::do_language_agnostic_bmc(
@@ -585,6 +600,11 @@ int jbmc_parse_optionst::doit()
     // particular function:
     add_failed_symbols(lazy_goto_model.symbol_table);
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      lazy_goto_model.validate(validation_modet::INVARIANT);
+    }
+
     // Provide show-goto-functions and similar dump functions after symex
     // executes. If --paths is active, these dump routines run after every
     // paths iteration. Its return value indicates that if we ran any dump
@@ -1141,6 +1161,7 @@ void jbmc_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

jbmc/src/jbmc/jbmc_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>
 
@@ -80,6 +81,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   "(java-threading)" \
   OPT_GOTO_TRACE \
+  OPT_VALIDATE \
   "(symex-driven-lazy-loading)"
 // clang-format on