Fix based on reviews

Author: Petr Bauch

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -46,6 +46,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/mode.h>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
 #include <util/unicode.h>
@@ -637,6 +638,12 @@ bool janalyzer_parse_optionst::set_properties()
       ::set_properties(goto_model, cmdline.get_values("property"));
   }
 
+  catch(const incorrect_goto_program_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";
+    return true;
+  }
+
   catch(const char *e)
   {
     error() << e << eom;

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
@@ -577,6 +578,12 @@ bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
       ::set_properties(goto_model, cmdline.get_values("property"));
   }
 
+  catch(const incorrect_goto_program_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";
+    return true;
+  }
+
   catch(const char *e)
   {
     error() << e << eom;

src/cbmc/cbmc_parse_options.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
@@ -545,6 +546,12 @@ bool cbmc_parse_optionst::set_properties()
       ::set_properties(goto_model, cmdline.get_values("property"));
   }
 
+  catch(const incorrect_goto_program_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";
+    return true;
+  }
+
   catch(const char *e)
   {
     error() << e << eom;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -51,6 +51,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
 #include <util/unicode.h>
@@ -691,6 +692,12 @@ bool goto_analyzer_parse_optionst::set_properties()
       ::set_properties(goto_model, cmdline.get_values("property"));
   }
 
+  catch(const incorrect_goto_program_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";
+    return true;
+  }
+
   catch(const char *e)
   {
     error() << e << eom;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -906,10 +906,6 @@ void goto_instrument_parse_optionst::get_goto_program()
   goto_model = std::move(result.value());
 
   config.set(cmdline);
-
-  POSTCONDITION(
-    goto_model.goto_functions.function_map.count(
-      goto_functionst::entry_point()) != 0);
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()

src/goto-programs/slice_global_inits.cpp

@@ -21,6 +21,7 @@ Date:   December 2016
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 
 #include <goto-programs/goto_functions.h>
@@ -34,8 +35,8 @@ void slice_global_inits(goto_modelt &goto_model)
   const irep_idt entry_point=goto_functionst::entry_point();
   goto_functionst &goto_functions=goto_model.goto_functions;
 
-  INVARIANT(
-    goto_functions.function_map.count(entry_point), "entry point not found");
+  if(goto_functions.function_map.count(entry_point) == 0)
+    throw incorrect_goto_program_exceptiont("entry point not found");
 
   // Get the call graph restricted to functions reachable from
   // the entry point:
@@ -75,8 +76,8 @@ void slice_global_inits(goto_modelt &goto_model)
 
   goto_functionst::function_mapt::iterator f_it;
   f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
-  INVARIANT(
-    f_it != goto_functions.function_map.end(), "initialize function not found");
+  if(f_it == goto_functions.function_map.end())
+    throw incorrect_goto_program_exceptiont("initialize function not found");
 
   goto_programt &goto_program=f_it->second.body;
 

src/goto-programs/string_instrumentation.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/message.h>
 #include <util/std_code.h>
@@ -281,7 +280,7 @@ void string_instrumentationt::do_sprintf(
 
   if(arguments.size()<2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "sprintf expected to have two or more arguments",
       target->source_location);
   }
@@ -323,7 +322,7 @@ void string_instrumentationt::do_snprintf(
 
   if(arguments.size()<3)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "snprintf expected to have three or more arguments",
       target->source_location);
   }
@@ -365,7 +364,7 @@ void string_instrumentationt::do_fscanf(
 
   if(arguments.size()<2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "fscanf expected to have two or more arguments", target->source_location);
   }
 
@@ -650,7 +649,7 @@ void string_instrumentationt::do_strchr(
 
   if(arguments.size()!=2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "strchr expected to have two arguments", target->source_location);
   }
 
@@ -676,7 +675,7 @@ void string_instrumentationt::do_strrchr(
 
   if(arguments.size()!=2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "strrchr expected to have two arguments", target->source_location);
   }
 
@@ -702,7 +701,7 @@ void string_instrumentationt::do_strstr(
 
   if(arguments.size()!=2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "strstr expected to have two arguments", target->source_location);
   }
 
@@ -735,7 +734,7 @@ void string_instrumentationt::do_strtok(
 
   if(arguments.size()!=2)
   {
-    throw incorrect_goto_program_exceptiont(
+    throw incorrect_source_program_exceptiont(
       "strtok expected to have two arguments", target->source_location);
   }
 

src/goto-programs/string_instrumentation.h

@@ -14,9 +14,30 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_functions.h"
 
+#include <util/exception_utils.h>
+
 class message_handlert;
 class goto_modelt;
 
+class incorrect_source_program_exceptiont : public cprover_exception_baset
+{
+public:
+  incorrect_source_program_exceptiont(
+    std::string message,
+    source_locationt source_location)
+    : message(std::move(message)), source_location(std::move(source_location))
+  {
+  }
+  std::string what() const
+  {
+    return message + " (at: " + source_location.as_string() + ")";
+  }
+
+private:
+  std::string message;
+  source_locationt source_location;
+};
+
 void string_instrumentation(
   symbol_tablet &,
   message_handlert &,

src/goto-programs/vcd_goto_trace.cpp

@@ -54,7 +54,7 @@ std::string as_vcd_binary(
   }
   else if(expr.id()==ID_union)
   {
-    return as_vcd_binary(to_union_expr(expr).op0(), ns);
+    return as_vcd_binary(to_union_expr(expr).op(), ns);
   }
 
   // build "xxx"

src/goto-programs/write_goto_binary.cpp

@@ -153,11 +153,11 @@ bool write_goto_binary(
   const int current_goto_version = 4;
   if(version < current_goto_version)
     throw invalid_user_input_exceptiont(
-      "version no longer supported",
+      "version " + std::to_string(version) + " no longer supported",
       "supported version = " + std::to_string(current_goto_version));
   else if(version > current_goto_version)
     throw invalid_user_input_exceptiont(
-      "unknown goto binary version",
+      "unknown goto binary version " + std::to_string(version),
       "supported version = " + std::to_string(current_goto_version));
   else
     return write_goto_binary_v4(