Invariant cleanup util dir tz files req exception review

src/util/tempdir.cpp

@@ -32,7 +32,7 @@ Author: CM Wintersteiger
 #include <unistd.h>
 #endif
 
-#include "invariant.h"
+#include "exception_utils.h"
 #include "file_util.h"
 
 std::string get_temporary_directory(const std::string &name_template)
@@ -45,7 +45,9 @@ std::string get_temporary_directory(const std::string &name_template)
     DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer);
 
     if(dwRetVal > dwBufSize || (dwRetVal == 0))
-      throw "GetTempPath failed"; // NOLINT(readability/throw)
+    {
+      throw system_exceptiont("Couldn't get temporary path");
+    }
 
     // GetTempFileNameA produces <path>\<pre><uuuu>.TMP
     // where <pre> = "TLO"
@@ -54,12 +56,18 @@ std::string get_temporary_directory(const std::string &name_template)
     char t[MAX_PATH];
     UINT uRetVal=GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
     if(uRetVal == 0)
-      throw "GetTempFileName failed"; // NOLINT(readability/throw)
+    {
+      throw system_exceptiont(
+        std::string("Couldn't get new temporary file name in directory") +
+        lpPathBuffer);
+    }
 
     unlink(t);
-    if(_mkdir(t)!=0)
-      throw "_mkdir failed";
-
+    if(_mkdir(t) != 0)
+    {
+      throw system_exceptiont(
+        std::string("Couldn't create temporary directory at ") + t);
+    }
     result=std::string(t);
 
   #else
@@ -75,7 +83,7 @@ std::string get_temporary_directory(const std::string &name_template)
     t.push_back('\0'); // add the zero
     const char *td = mkdtemp(t.data());
     if(!td)
-      throw "mkdtemp failed";
+      throw system_exceptiont("Failed to create temporary directory");
     result=std::string(td);
   #endif
 

src/util/tempfile.cpp

@@ -31,6 +31,8 @@ Author: Daniel Kroening
 #include <cstdio>
 #include <cstring>
 
+#include "exception_utils.h"
+
 #if defined(__linux__) || \
     defined(__FreeBSD_kernel__) || \
     defined(__GNU__) || \
@@ -104,7 +106,7 @@ std::string get_temporary_file(
       lpTempPathBuffer); // buffer for path
 
   if(dwRetVal>MAX_PATH || (dwRetVal==0))
-    throw "GetTempPath failed"; // NOLINT(readability/throw)
+    throw system_exceptiont("Failed to get temporary directory");
 
   // the path returned by GetTempPath ends with a backslash
   std::string t_template=
@@ -127,7 +129,7 @@ std::string get_temporary_file(
   int fd=mkstemps(t_ptr, suffix.size());
 
   if(fd<0)
-    throw "mkstemps failed";
+    throw system_exceptiont("Failed to open temporary file");
 
   close(fd);
 

src/util/type_eq.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "type_eq.h"
 
+#include "invariant.h"
 #include "namespace.h"
 #include "std_types.h"
 #include "symbol.h"
@@ -35,18 +36,14 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
   if(const auto symbol_type1 = type_try_dynamic_cast<symbol_typet>(type1))
   {
     const symbolt &symbol = ns.lookup(*symbol_type1);
-    if(!symbol.is_type)
-      throw "symbol "+id2string(symbol.name)+" is not a type";
-
+    CHECK_RETURN(symbol.is_type);
     return type_eq(symbol.type, type2, ns);
   }
 
   if(const auto symbol_type2 = type_try_dynamic_cast<symbol_typet>(type2))
   {
     const symbolt &symbol = ns.lookup(*symbol_type2);
-    if(!symbol.is_type)
-      throw "symbol "+id2string(symbol.name)+" is not a type";
-
+    CHECK_RETURN(symbol.is_type);
     return type_eq(type1, symbol.type, ns);
   }
 

src/util/union_find.cpp

@@ -46,16 +46,15 @@ void unsigned_union_find::isolate(size_type a)
   if(is_root(a))
   {
     size_type c=nodes[a].count;
+    DATA_INVARIANT(c != 0, "a root cannot have a node count of zero");
 
     // already isolated?
     if(c==1)
       return;
 
-    assert(c>=2);
-
     // find a new root
     size_type new_root=get_other(a);
-    assert(new_root!=a);
+    CHECK_RETURN(new_root != a);
 
     re_root(a, new_root);
   }
@@ -64,8 +63,6 @@ void unsigned_union_find::isolate(size_type a)
   // get its root
   size_type r=find(a);
 
-  // assert(r!=a);
-
   nodes[r].count--;
   nodes[a].parent=a;
   nodes[a].count=1;
@@ -80,13 +77,11 @@ void unsigned_union_find::re_root(size_type old_root, size_type new_root)
   old_root=find(old_root);
 
   // same set?
-  // assert(find(new_root)==old_root);
   if(find(new_root)!=old_root)
     return;
 
-  // make sure we actually do something
-  assert(new_root!=old_root);
-  assert(nodes[old_root].count>=2);
+  PRECONDITION(!is_root(new_root));
+  PRECONDITION(nodes[old_root].count >= 2);
 
   nodes[new_root].parent=new_root;
   nodes[new_root].count=nodes[old_root].count;
@@ -110,7 +105,8 @@ unsigned_union_find::size_type unsigned_union_find::get_other(size_type a)
   check_index(a);
   a=find(a);
 
-  assert(nodes[a].count>=2);
+  // Cannot find another node in a singleton set
+  PRECONDITION(nodes[a].count >= 2);
 
   // find a different member of the same set
   for(size_type i=0; i<size(); i++)

src/util/union_find.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <vector>
 
+#include "invariant.h"
 #include "numbering.h"
 
 // Standard union find with weighting and path compression.
@@ -63,8 +64,11 @@ class unsigned_union_find
 
   void resize(size_type size)
   {
-    // We only enlarge. Shrinking is yet to be implemented.
-    assert(nodes.size()<=size);
+    if(size < nodes.size())
+    {
+      INVARIANT(false, "we don't implement shrinking yet");
+    }
+
     nodes.reserve(size);
     while(nodes.size()<size)
       nodes.push_back(nodet(nodes.size()));

src/util/xml.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include "exception_utils.h"
 #include "string2int.h"
 
 void xmlt::clear()
@@ -240,7 +241,7 @@ std::string xmlt::unescape(const std::string &str)
         result+=c;
       }
       else
-        throw "XML escape code not implemented"; // NOLINT(readability/throw)
+        throw deserialization_exceptiont("unknown XML escape code: " + tmp);
     }
     else
       result+=*it;

src/util/xml_expr.cpp

@@ -13,14 +13,15 @@ Author: Daniel Kroening
 
 #include "xml_expr.h"
 
-#include "namespace.h"
-#include "expr.h"
-#include "xml.h"
 #include "arith_tools.h"
-#include "ieee_float.h"
+#include "config.h"
+#include "expr.h"
 #include "fixedbv.h"
+#include "ieee_float.h"
+#include "invariant.h"
+#include "namespace.h"
 #include "std_expr.h"
-#include "config.h"
+#include "xml.h"
 
 xmlt xml(const source_locationt &location)
 {
@@ -273,7 +274,7 @@ xmlt xml(
     {
       const struct_typet &struct_type=to_struct_type(type);
       const struct_typet::componentst &components=struct_type.components();
-      assert(components.size()==expr.operands().size());
+      PRECONDITION(components.size() == expr.operands().size());
 
       for(unsigned m=0; m<expr.operands().size(); m++)
       {
@@ -285,15 +286,12 @@ xmlt xml(
   }
   else if(expr.id()==ID_union)
   {
+    const union_exprt &union_expr = to_union_expr(expr);
     result.name="union";
 
-    assert(expr.operands().size()==1);
-
     xmlt &e=result.new_element("member");
-    e.new_element(xml(expr.op0(), ns));
-    e.set_attribute(
-      "member_name",
-      id2string(to_union_expr(expr).get_component_name()));
+    e.new_element(xml(union_expr.op(), ns));
+    e.set_attribute("member_name", id2string(union_expr.get_component_name()));
   }
   else
     result.name="unknown";