Merge pull request #4389 from smowton/smowton/cleanup/validate-model-before-show

Move validate-goto-model before show-goto-functions

Author: smowton

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -549,11 +549,6 @@ 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();
-    }
-
     if(
       options.get_bool_option("program-only") ||
       options.get_bool_option("show-vcc"))
@@ -769,6 +764,11 @@ int jbmc_parse_optionst::get_goto_program(
     if(goto_model == nullptr)
       return 6;
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      goto_model->validate();
+    }
+
     // show it?
     if(cmdline.isset("show-loops"))
     {

src/cbmc/cbmc_parse_options.cpp

@@ -557,11 +557,6 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
-  if(cmdline.isset("validate-goto-model"))
-  {
-    goto_model.validate();
-  }
-
   if(
     options.get_bool_option("program-only") ||
     options.get_bool_option("show-vcc"))
@@ -713,6 +708,11 @@ int cbmc_parse_optionst::get_goto_program(
     if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
       return CPROVER_EXIT_INTERNAL_ERROR;
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      goto_model.validate();
+    }
+
     // show it?
     if(cmdline.isset("show-loops"))
     {