Some basic exception types

Author: peterschrammel

src/cbmc/bv_cbmc.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/replace_expr.h>
+#include <util/invariant_utils.h>
 
 bvt bv_cbmct::convert_waitfor(const exprt &expr)
 {

src/cbmc/cbmc_solvers.cpp

@@ -206,8 +206,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
   {
     if(solver==smt1_dect::solvert::GENERIC)
     {
-      error() << "please use --outfile" << eom;
-      throw 0;
+      throw user_exceptiont("please use --outfile");
     }
 
     smt1_dect *smt1_dec=
@@ -245,8 +244,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     if(!out)
     {
-      error() << "failed to open " << filename << eom;
-      throw 0;
+      IO_EXCEPTION_WITH_FILENAME("failed to open", filename);
     }
 
     smt1_convt *smt1_conv=

src/cbmc/show_vcc.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/json.h>
 #include <util/json_expr.h>
+#include <util/invariant_utils.h>
 
 void bmct::show_vcc_plain(std::ostream &out)
 {
@@ -150,7 +151,7 @@ void bmct::show_vcc()
   {
     of.open(filename);
     if(!of)
-      throw "failed to open file "+filename;
+      throw system_exceptiont("failed to open file "+filename);
   }
 
   std::ostream &out=have_file?of:std::cout;

src/util/exception_utils.h

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Peter Schrammel, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_EXCEPTION_UTILS_H
+#define CPROVER_UTIL_EXCEPTION_UTILS_H
+
+#include "invariant.h"
+
+/// A logic error to be used for OS-related errors (I/O etc)
+class system_exceptiont: public std::logic_error
+{
+public:
+  system_exceptiont(
+    const std::string &_reason):
+    std::logic_error(_reason)
+  {
+  }
+};
+
+/// A logic error to be used for user interface errors
+class ui_exceptiont: public std::logic_error
+{
+public:
+  ui_exceptiont(
+    const std::string &_reason):
+    std::logic_error(_reason)
+  {
+  }
+};
+
+/// A user interface exception with source locations
+class input_src_exceptiont: public ui_exceptiont
+{
+public:
+  input_src_exceptiont(
+    const source_locationt &_source_location,
+    const std::string &_reason):
+    ui_exceptiont(_reason),
+    source_location(_source_location)
+  {
+  }
+  
+  source_locationt source_location;
+};
+
+#endif // CPROVER_UTIL_EXCEPTION_UTILS_H