Replace assertions in some core libraries.

These also serve as examples of which annotations to use.

Author: martin

src/util/expr.cpp

@@ -9,14 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
-#include <cassert>
-
 #include <stack>
 
 #include "string2int.h"
 #include "mp_arith.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
+#include "invariant.h"
 #include "expr.h"
 #include "rational.h"
 #include "rational_tools.h"
@@ -203,15 +202,16 @@ void exprt::negate()
       else
       {
         make_nil();
-        assert(false);
+        UNREACHABLE;
       }
     }
     else
     {
       if(id()==ID_unary_minus)
       {
         exprt tmp;
-        assert(operands().size()==1);
+        DATA_INVARIANT(operands().size()==1,
+                       "Unary minus must have one operand");
         tmp.swap(op0());
         swap(tmp);
       }
@@ -245,7 +245,7 @@ bool exprt::is_zero() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_zero();
     }
     else if(type_id==ID_unsignedbv ||
@@ -291,7 +291,7 @@ bool exprt::is_one() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_one();
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)

src/util/expr_util.cpp

@@ -36,14 +36,14 @@ exprt make_binary(const exprt &expr)
   const typet &type=expr.type();
 
   exprt previous=operands.front();
-  assert(previous.type()==type);
+  PRECONDITION(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
-    assert(it->type()==type);
+    PRECONDITION(it->type()==type);
 
     exprt tmp=expr;
     tmp.operands().clear();
@@ -59,7 +59,7 @@ exprt make_binary(const exprt &expr)
 with_exprt make_with_expr(const update_exprt &src)
 {
   const exprt::operandst &designator=src.designator();
-  assert(!designator.empty());
+  PRECONDITION(!designator.empty());
 
   with_exprt result;
   exprt *dest=&result;
@@ -78,7 +78,7 @@ with_exprt make_with_expr(const update_exprt &src)
       //  to_member_designator(*it).get_component_name();
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     *dest=tmp;
     dest=&to_with_expr(*dest).new_value();
@@ -108,7 +108,7 @@ exprt is_not_zero(
     src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
 
   exprt zero=from_integer(0, src_type);
-  assert(zero.is_not_nil());
+  CHECK_RETURN(zero.is_not_nil());
 
   binary_exprt comparison(src, id, zero, bool_typet());
   comparison.add_source_location()=src.source_location();
@@ -142,8 +142,8 @@ bool has_subexpr(const exprt &src, const irep_idt &id)
 
 if_exprt lift_if(const exprt &src, std::size_t operand_number)
 {
-  assert(operand_number<src.operands().size());
-  assert(src.operands()[operand_number].id()==ID_if);
+  PRECONDITION(operand_number<src.operands().size());
+  PRECONDITION(src.operands()[operand_number].id()==ID_if);
 
   const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
   const exprt true_case=if_expr.true_case();

src/util/irep.cpp

@@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Internal Representation
 
-#include <cassert>
 #include <ostream>
 
+#include "invariant.h"
+
 #include "string2int.h"
 #include "irep.h"
 #include "string_hash.h"
@@ -87,7 +88,7 @@ void irept::detach()
     remove_ref(old_data);
   }
 
-  assert(data->ref_count==1);
+  POSTCONDITION(data->ref_count==1);
 
   #ifdef IREP_DEBUG
   std::cout << "DETACH2: " << data << '\n';
@@ -105,7 +106,7 @@ void irept::remove_ref(dt *old_data)
   nonrecursive_destructor(old_data);
   #else
 
-  assert(old_data->ref_count!=0);
+  PRECONDITION(old_data->ref_count!=0);
 
   #ifdef IREP_DEBUG
   std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
@@ -147,7 +148,7 @@ void irept::nonrecursive_destructor(dt *old_data)
     if(d==&empty_d)
       continue;
 
-    assert(d->ref_count!=0);
+    INVARIANT(d->ref_count!=0, "All contents of the stack must be in use");
     d->ref_count--;
 
     if(d->ref_count==0)
@@ -456,7 +457,8 @@ bool irept::ordering(const irept &other) const
         return false;
     }
 
-    assert(it1==X.sub.end() && it2==Y.sub.end());
+    INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
+              "Unequal lengths will return before this");
   }
 
   if(X.named_sub.size()<Y.named_sub.size())
@@ -484,7 +486,8 @@ bool irept::ordering(const irept &other) const
         return false;
     }
 
-    assert(it1==X.named_sub.end() && it2==Y.named_sub.end());
+    INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
+              "Unequal lengths will return before this");
   }
 
   return false;
@@ -521,7 +524,8 @@ int irept::compare(const irept &i) const
         return r;
     }
 
-    assert(it1==get_sub().end() && it2==i.get_sub().end());
+    INVARIANT(it1==get_sub().end() && it2==i.get_sub().end(),
+              "Unequal lengths will return before this");
   }
 
   const named_subt::size_type n_size=get_named_sub().size(),
@@ -549,8 +553,9 @@ int irept::compare(const irept &i) const
         return r;
     }
 
-    assert(it1==get_named_sub().end() &&
-           it2==i.get_named_sub().end());
+    INVARIANT(it1==get_named_sub().end() &&
+              it2==i.get_named_sub().end(),
+              "Unequal lengths will return before this");
   }
 
   // equal