Use invariant instead of abort()

Author: peterschrammel

src/cpp/cpp_typecheck_expr.cpp

@@ -11,7 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
-#include <cstdlib>
+#ifdef DEBUG
+#include <iostream>
+#endif
 
 #include <util/pointer_offset_size.h>
 #include <util/std_types.h>
@@ -20,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
 
 #include <util/c_types.h>
 #include <ansi-c/c_qualifiers.h>
@@ -69,25 +72,27 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr)
     typecheck_expr_explicit_constructor_call(expr);
   else if(expr.is_nil())
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got nil\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_code)
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got code\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_symbol)
   {
-    #if 0
-    std::cout << "E: " << expr.pretty() << '\n';
+    // ignore here
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got symbol\n";
-    abort();
-    #endif
+#endif
   }
   else if(expr.id()=="__is_base_of")
   {

src/goto-symex/goto_symex_state.cpp

@@ -50,12 +50,9 @@ void goto_symex_statet::level0t::operator()(
     return;
 
   const symbolt *s;
-
-  if(ns.lookup(obj_identifier, s))
-  {
-    std::cerr << "level0: failed to find " << obj_identifier << '\n';
-    abort();
-  }
+  const bool found_l0 = !ns.lookup(obj_identifier, s);
+  DATA_INVARIANT(
+    found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||

src/solvers/refinement/refine_arithmetic.cpp

@@ -226,8 +226,6 @@ void bv_refinementt::check_SAT(approximationt &a)
               << "==" << integer2binary(result.pack(), spec.width()) << eom;
     #endif
 
-    // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
-
     if(a.over_state<config_.max_node_refinement)
     {
       bvt r;

src/util/cmdline.cpp

@@ -8,9 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "cmdline.h"
 
-#include <cassert>
-#include <cstdlib>
-#include <iostream>
+#include <util/invariant.h>
 
 cmdlinet::cmdlinet()
 {
@@ -124,11 +122,8 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring)
   {
     optiont option;
 
-    if(optstring[0]==':')
-    {
-      std::cerr << "cmdlinet::parse: Invalid option string\n";
-      abort();
-    }
+    DATA_INVARIANT(
+      optstring[0] != ':', "cmdlinet::parse: Invalid option string\n");
 
     if(optstring[0]=='(')
     {