Invariant cleanup goto programs sz

Author: Petr Bauch

src/goto-programs/set_properties.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "set_properties.h"
 
+#include <util/invariant.h>
+
 #include <algorithm>
 #include <unordered_set>
 
@@ -110,8 +112,11 @@ void set_properties(
     if(!it->second.is_inlined())
       set_properties(it->second.body, property_set);
 
-  if(!property_set.empty())
-    throw "property "+id2string(*property_set.begin())+" not found";
+  INVARIANT_WITH_DIAGNOSTICS(
+    property_set.empty(),
+    "Property ",
+    id2string(*property_set.begin()),
+    " not found.");
 }
 
 void label_properties(goto_functionst &goto_functions)

src/goto-programs/show_symbol_table.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <util/invariant.h>
 #include <util/json_irep.h>
 
 #include "goto_model.h"
@@ -51,8 +52,11 @@ void show_symbol_table_brief_plain(
     else
     {
       ptr=get_language_from_mode(symbol.mode);
-      if(ptr==nullptr)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
+      INVARIANT_WITH_DIAGNOSTICS(
+        ptr != nullptr,
+        "Symbol ",
+        id2string(symbol.name),
+        " has unknown mode.");
     }
 
     std::string type_str;
@@ -95,8 +99,8 @@ void show_symbol_table_plain(
       ptr=get_language_from_mode(symbol.mode);
     }
 
-    if(!ptr)
-      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    INVARIANT_WITH_DIAGNOSTICS(
+      ptr != nullptr, "Symbol ", id2string(symbol.name), " has unknown mode.");
 
     std::string type_str, value_str;
 
@@ -183,8 +187,8 @@ static void show_symbol_table_json_ui(
       ptr=get_language_from_mode(symbol.mode);
     }
 
-    if(!ptr)
-      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    INVARIANT_WITH_DIAGNOSTICS(
+      ptr != nullptr, "Symbol ", id2string(symbol.name), " has unknown mode.");
 
     std::string type_str, value_str;
 
@@ -258,8 +262,8 @@ static void show_symbol_table_brief_json_ui(
       ptr=get_language_from_mode(symbol.mode);
     }
 
-    if(!ptr)
-      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    INVARIANT_WITH_DIAGNOSTICS(
+      ptr != nullptr, "Symbol ", id2string(symbol.name), " has unknown mode.");
 
     std::string type_str, value_str;
 

src/goto-programs/slice_global_inits.cpp

@@ -15,11 +15,12 @@ Date:   December 2016
 
 #include <analyses/call_graph.h>
 
+#include <util/cprover_prefix.h>
 #include <util/find_symbols.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
-#include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/remove_skip.h>
@@ -32,8 +33,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;
 
-  if(!goto_functions.function_map.count(entry_point))
-    throw "entry point not found";
+  INVARIANT(
+    goto_functions.function_map.count(entry_point), "Entry point not found.");
 
   // Get the call graph restricted to functions reachable from
   // the entry point:
@@ -73,7 +74,9 @@ void slice_global_inits(goto_modelt &goto_model)
 
   goto_functionst::function_mapt::iterator f_it;
   f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
-  assert(f_it!=goto_functions.function_map.end());
+  INVARIANT(
+    f_it != goto_functions.function_map.end(),
+    "Initialize function not found.");
 
   goto_programt &goto_program=f_it->second.body;
 

src/goto-programs/string_instrumentation.cpp

@@ -16,9 +16,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/message.h>
-#include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/format_strings.h>
@@ -281,7 +282,7 @@ void string_instrumentationt::do_sprintf(
   {
     error().source_location=target->source_location;
     error() << "sprintf expected to have two or more arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -324,7 +325,7 @@ void string_instrumentationt::do_snprintf(
     error().source_location=target->source_location;
     error() << "snprintf expected to have three or more arguments"
             << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -366,7 +367,7 @@ void string_instrumentationt::do_fscanf(
   {
     error().source_location=target->source_location;
     error() << "fscanf expected to have two or more arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -652,7 +653,7 @@ void string_instrumentationt::do_strchr(
   {
     error().source_location=target->source_location;
     error() << "strchr expected to have two arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -679,7 +680,7 @@ void string_instrumentationt::do_strrchr(
   {
     error().source_location=target->source_location;
     error() << "strrchr expected to have two arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -706,7 +707,7 @@ void string_instrumentationt::do_strstr(
   {
     error().source_location=target->source_location;
     error() << "strstr expected to have two arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;
@@ -740,7 +741,7 @@ void string_instrumentationt::do_strtok(
   {
     error().source_location=target->source_location;
     error() << "strtok expected to have two arguments" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   goto_programt tmp;

src/goto-programs/vcd_goto_trace.cpp

@@ -13,9 +13,9 @@ Date: June 2011
 
 #include "vcd_goto_trace.h"
 
-#include <cassert>
 #include <ctime>
 
+#include <util/invariant.h>
 #include <util/numbering.h>
 #include <util/pointer_offset_size.h>
 
@@ -55,7 +55,7 @@ std::string as_vcd_binary(
   }
   else if(expr.id()==ID_union)
   {
-    assert(expr.operands().size()==1);
+    INVARIANT(expr.operands().size() == 1, "Union only takes 1 operand.");
     return as_vcd_binary(expr.op0(), ns);
   }
 

src/goto-programs/wp.cpp

@@ -13,9 +13,10 @@ Author: Daniel Kroening, [email protected]
 
 // #include <langapi/language_util.h>
 
-#include <util/std_expr.h>
-#include <util/std_code.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 bool has_nondet(const exprt &dest)
 {
@@ -263,6 +264,6 @@ exprt wp(
     return post; // ignored
   else if(statement==ID_fence)
     return post; // ignored
-  else
-    throw "sorry, wp("+id2string(statement)+"...) not implemented";
+  INVARIANT_WITH_DIAGNOSTICS(
+    false, "Sorry, wp(", id2string(statement), "...) is not implemented.");
 }

src/goto-programs/write_goto_binary.cpp

@@ -13,8 +13,9 @@ Author: CM Wintersteiger
 
 #include <fstream>
 
-#include <util/message.h>
+#include <util/invariant.h>
 #include <util/irep_serialization.h>
+#include <util/message.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_model.h>
@@ -148,22 +149,9 @@ bool write_goto_binary(
   irep_serializationt::ireps_containert irepc;
   irep_serializationt irepconverter(irepc);
 
-  switch(version)
-  {
-  case 1:
-  case 2:
-  case 3:
-    throw "version no longer supported";
-
-  case 4:
-    return write_goto_binary_v4(
-      out, symbol_table, goto_functions, irepconverter);
-
-  default:
-    throw "unknown goto binary version";
-  }
-
-  return false;
+  INVARIANT(version > 3, "Version no longer supported.");
+  INVARIANT(version == 4, "Unknown goto binary version.");
+  return write_goto_binary_v4(out, symbol_table, goto_functions, irepconverter);
 }
 
 /// Writes a goto program to disc