Some basic exception types

peterschrammel · peterschrammel · commit b2c6da21a78e · 2017-08-22T19:04:40.000+01:00
diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/replace_expr.h>
+#include <util/invariant_utils.h>
 
 bvt bv_cbmct::convert_waitfor(const exprt &expr)
 {
diff --git a/src/cbmc/cbmc_solvers.cpp b/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=
diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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;
diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h
@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Peter Schrammel, peter.schrammel@diffblue.com
+
+\*******************************************************************/
+
+#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

Original file line number	Diff line number	Diff line change
`@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]`
`10`	`10`
`11`	`11`	`#include <util/arith_tools.h>`
`12`	`12`	`#include <util/replace_expr.h>`
	`13`	`+#include <util/invariant_utils.h>`
`13`	`14`
`14`	`15`	`bvt bv_cbmct::convert_waitfor(const exprt &expr)`
`15`	`16`	`{`
Original file line number	Diff line number	Diff line change
`@@ -206,8 +206,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)`
`206`	`206`	`{`
`207`	`207`	`if(solver==smt1_dect::solvert::GENERIC)`
`208`	`208`	`{`
`209`		`- error() << "please use --outfile" << eom;`
`210`		`- throw 0;`
	`209`	`+ throw user_exceptiont("please use --outfile");`
`211`	`210`	`}`
`212`	`211`
`213`	`212`	`smt1_dect *smt1_dec=`
`@@ -245,8 +244,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)`
`245`	`244`
`246`	`245`	`if(!out)`
`247`	`246`	`{`
`248`		`- error() << "failed to open " << filename << eom;`
`249`		`- throw 0;`
	`247`	`+ IO_EXCEPTION_WITH_FILENAME("failed to open", filename);`
`250`	`248`	`}`
`251`	`249`
`252`	`250`	`smt1_convt *smt1_conv=`
Original file line number	Diff line number	Diff line change
`@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]`
`22`	`22`
`23`	`23`	`#include <util/json.h>`
`24`	`24`	`#include <util/json_expr.h>`
	`25`	`+#include <util/invariant_utils.h>`
`25`	`26`
`26`	`27`	`void bmct::show_vcc_plain(std::ostream &out)`
`27`	`28`	`{`
`@@ -150,7 +151,7 @@ void bmct::show_vcc()`
`150`	`151`	`{`
`151`	`152`	`of.open(filename);`
`152`	`153`	`if(!of)`
`153`		`- throw "failed to open file "+filename;`
	`154`	`+ throw system_exceptiont("failed to open file "+filename);`
`154`	`155`	`}`
`155`	`156`
`156`	`157`	`std::ostream &out=have_file?of:std::cout;`