add --validate-goto-model to goto-cc

This enables tests of the validation without CBMC.

Author: Daniel Kroening

src/goto-cc/compile.cpp

@@ -542,6 +542,11 @@ bool compilet::write_bin_object_file(
   const std::string &file_name,
   const goto_modelt &src_goto_model)
 {
+  status() << "Validating goto model" << eom;
+
+  if(validate_goto_model)
+    src_goto_model.validate(validation_modet::INVARIANT);
+
   statistics() << "Writing binary format object `"
                << file_name << "'" << eom;
 

src/goto-cc/compile.h

@@ -34,6 +34,7 @@ class compilet : public messaget
   bool echo_file_name;
   std::string working_directory;
   std::string override_language;
+  bool validate_goto_model = false;
 
   enum { PREPROCESS_ONLY, // gcc -E
          COMPILE_ONLY, // gcc -c

src/goto-cc/gcc_cmdline.cpp

@@ -49,6 +49,7 @@ const char *goto_cc_options_without_argument[]=
   "--big-endian",
   "--no-arch",
   "--partial-inlining",
+  "--validate-goto-model",
   "-?",
   nullptr
 };