Fix based on review comments

Author: Petr Bauch

src/goto-programs/lazy_goto_model.cpp

@@ -95,7 +95,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
   const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    throw invalid_user_input_exceptiont("No program provided", "", "");
+    throw invalid_user_input_exceptiont(
+      "no program provided", "cbmc file.c ...");
   }
 
   std::vector<std::string> binaries, sources;
@@ -134,10 +135,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
         source_locationt location;
         location.set_file(filename);
         msg.error().source_location=location;
-        throw deserialization_exceptiont(
-          "failed to figure out type of file"
-          "\nsource location: " +
-          location.as_string());
+        throw incorrect_goto_program_exceptiont(
+          "failed to figure out type of file", location);
       }
 
       languaget &language=*lf.language;
@@ -148,8 +147,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
 
       if(language.parse(infile, filename))
       {
-        // TODO more helpful error message
-        throw deserialization_exceptiont("PARSING ERROR");
+        throw deserialization_exceptiont("language parsing failed");
       }
 
       lf.get_modules();
@@ -159,8 +157,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
 
     if(language_files.typecheck(symbol_table))
     {
-      // TODO more helpful error message
-      throw deserialization_exceptiont("CONVERSION ERROR");
+      throw deserialization_exceptiont(
+        "type-checking of interface/files/modules failed");
     }
   }
 
@@ -170,8 +168,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
 
     if(read_object_and_link(file, *goto_model, message_handler))
     {
-      // TODO more helpful error message
-      throw deserialization_exceptiont("Failed to read/link goto model");
+      throw deserialization_exceptiont(
+        "failed to read object or link in file `" + file + '\'');
     }
   }
 
@@ -207,8 +205,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
 
   if(entry_point_generation_failed)
   {
-    // TODO more helpful error message
-    throw deserialization_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
+    throw deserialization_exceptiont("failed to generate entry point");
   }
 
   // stupid hack

src/goto-programs/link_goto_model.cpp

@@ -173,8 +173,8 @@ void link_goto_model(
 
   if(linking.typecheck_main())
   {
-    // TODO more helpful error message
-    throw deserialization_exceptiont("Typechecking main failed");
+    throw deserialization_exceptiont(
+      "failed to rename symbols during typechecking phase of linking");
   }
   if(link_functions(
        dest.symbol_table,
@@ -185,6 +185,6 @@ void link_goto_model(
        weak_symbols,
        linking.object_type_updates))
   {
-    throw deserialization_exceptiont("Linking failed");
+    throw deserialization_exceptiont("failed to link functions");
   }
 }

src/goto-programs/osx_fat_reader.cpp

@@ -11,7 +11,6 @@ Module: Read Mach-O
 
 #include "osx_fat_reader.h"
 
-#include <cassert>
 #include <cstdlib>
 #include <util/exception_utils.h>
 #include <util/invariant.h>

src/goto-programs/read_bin_goto_object.cpp

@@ -147,7 +147,7 @@ static bool read_bin_goto_object_v4(
         rev_target_mapt::const_iterator entry=rev_target_map.find(n);
         INVARIANT(
           entry != rev_target_map.end(),
-          "Something from the target map should also be in the reverse target "
+          "something from the target map should also be in the reverse target "
           "map");
         ins->targets.push_back(entry->second);
       }

src/goto-programs/remove_complex.cpp

@@ -32,7 +32,6 @@ static exprt complex_member(const exprt &expr, irep_idt id)
   }
   else
   {
-    PRECONDITION(expr.type().id() == ID_struct);
     const struct_typet &struct_type=
       to_struct_type(expr.type());
     PRECONDITION(struct_type.components().size() == 2);
@@ -229,13 +228,11 @@ static void remove_complex(exprt &expr)
 
   if(expr.id()==ID_complex_real)
   {
-    static_cast<void>(to_complex_real_expr(expr));
-    expr=complex_member(expr.op0(), ID_real);
+    expr = complex_member(to_complex_real_expr(expr).op(), ID_real);
   }
   else if(expr.id()==ID_complex_imag)
   {
-    static_cast<void>(to_complex_imag_expr(expr));
-    expr=complex_member(expr.op0(), ID_imag);
+    expr = complex_member(to_complex_imag_expr(expr).op(), ID_imag);
   }
 
   remove_complex(expr.type());

src/goto-programs/remove_unused_functions.cpp

@@ -77,12 +77,8 @@ void find_used_functions(
         {
           const code_function_callt &call = to_code_function_call(it->code);
 
-          // check that this is actually a simple call
-          INVARIANT(
-            call.function().id() == ID_symbol,
-            "by this point, all kinds of function calls should have been "
-            "converted to simple function calls");
-
+          // to_symbol_exprt checks that by this point, all kinds of function
+          // calls have been converted to simple function calls
           const irep_idt &identifier =
             to_symbol_expr(call.function()).get_identifier();
 

src/goto-programs/remove_vector.cpp

@@ -116,7 +116,7 @@ static void remove_vector(exprt &expr)
     else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
     {
       DATA_INVARIANT(
-        expr.operands().size() == 1, "unary operators have one operands");
+        expr.operands().size() == 1, "unary operators have one operand");
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 

src/goto-programs/replace_calls.cpp

@@ -108,7 +108,7 @@ void replace_callst::operator()(
         const symbol_exprt &se = to_symbol_expr(rhs);
         INVARIANT(
           !has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX),
-          "this happens before returns are removed");
+          "returns must not be removed before replacing calls");
       }
     }
 
@@ -136,7 +136,7 @@ replace_callst::replacement_mapt replace_callst::parse_replacement_list(
     if(!r.second)
     {
       throw invalid_user_input_exceptiont(
-        "Conflicting replacement for function " + original, "--replace-calls");
+        "conflicting replacement for function " + original, "--replace-calls");
     }
   }
 
@@ -152,23 +152,23 @@ void replace_callst::check_replacement_map(
   {
     if(replacement_map.find(p.second) != replacement_map.end())
       throw invalid_user_input_exceptiont(
-        "Function " + id2string(p.second) +
+        "function " + id2string(p.second) +
           " cannot both be replaced and be a replacement",
         "--replace-calls");
 
     auto it2 = goto_functions.function_map.find(p.second);
 
     if(it2 == goto_functions.function_map.end())
       throw invalid_user_input_exceptiont(
-        "Replacement function " + id2string(p.second) + " needs to be present",
+        "replacement function " + id2string(p.second) + " needs to be present",
         "--replace-calls");
 
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
       if(!base_type_eq(it1->second.type, it2->second.type, ns))
         throw invalid_user_input_exceptiont(
-          "Functions " + id2string(p.first) + " and " + id2string(p.second) +
+          "functions " + id2string(p.first) + " and " + id2string(p.second) +
             " are not type-compatible",
           "--replace-calls");
     }

src/util/exception_utils.h

@@ -120,32 +120,4 @@ class analysis_exceptiont : public cprover_exception_baset
   std::string reason;
 };
 
-class system_exceptiont
-{
-private:
-  std::string reason;
-
-public:
-  system_exceptiont(const std::string &reason) : reason(reason)
-  {
-  }
-
-  std::string what() const noexcept
-  {
-    std::string res;
-    res += "System Exception\n";
-    res += "Reason: " + reason + "\n";
-    return res;
-  }
-};
-
-class deserialization_exceptiont
-{
-public:
-  explicit deserialization_exceptiont(std::string message);
-  std::string what() const noexcept;
-private:
-  std::string message;
-};
-
 #endif // CPROVER_UTIL_EXCEPTION_UTILS_H