diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp index e1652695796..9d5d514d3c8 100644 --- a/src/cbmc/bv_cbmc.cpp +++ b/src/cbmc/bv_cbmc.cpp @@ -10,15 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include bvt bv_cbmct::convert_waitfor(const exprt &expr) { if(expr.operands().size()!=4) - { - error().source_location=expr.find_source_location(); - error() << "waitfor expected to have four operands" << eom; - throw 0; - } + throw input_src_exceptiont( + expr.find_source_location(), + "waitfor expected to have four operands"); exprt new_cycle; const exprt &old_cycle=expr.op0(); @@ -30,11 +29,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) mp_integer bound_value; if(to_integer(bound, bound_value)) - { - error().source_location=expr.find_source_location(); - error() << "waitfor bound must be a constant" << eom; - throw 0; - } + throw input_src_exceptiont( + expr.find_source_location(), + "waitfor bound must be a constant"); { // constraint: new_cycle>=old_cycle @@ -135,11 +132,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr) { if(expr.operands().size()!=1) - { - error().source_location=expr.find_source_location(); - error() << "waitfor_symbol expected to have one operand" << eom; - throw 0; - } + throw input_src_exceptiont( + expr.find_source_location(), + "waitfor_symbol expected to have one operand"); exprt result; const exprt &bound=expr.op0(); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 239b34d9b8c..ba71b1b05fc 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -69,7 +69,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "xml_interface.h" cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): - parse_options_baset(CBMC_OPTIONS, argc, argv), + parse_optionst(CBMC_OPTIONS, argc, argv, ui_message_handler), xml_interfacet(cmdline), language_uit(cmdline, ui_message_handler), ui_message_handler(cmdline, "CBMC " CBMC_VERSION) @@ -80,7 +80,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( int argc, const char **argv, const std::string &extra_options): - parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv), + parse_optionst( + CBMC_OPTIONS+extra_options, argc, argv, ui_message_handler), xml_interfacet(cmdline), language_uit(cmdline, ui_message_handler), ui_message_handler(cmdline, "CBMC " CBMC_VERSION) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index ef91683ee0e..b174c3e2002 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -72,7 +72,7 @@ class optionst; "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) class cbmc_parse_optionst: - public parse_options_baset, + public parse_optionst, public xml_interfacet, public language_uit { diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 2c5287fc199..6846ca78499 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -205,10 +206,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver) if(filename=="") { if(solver==smt1_dect::solvert::GENERIC) - { - error() << "please use --outfile" << eom; - throw 0; - } + throw ui_exceptiont("please use --outfile"); smt1_dect *smt1_dec= new smt1_dect( @@ -244,10 +242,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver) #endif if(!out) - { - error() << "failed to open " << filename << eom; - throw 0; - } + throw system_exceptiont("failed to open "+filename); smt1_convt *smt1_conv= new smt1_convt( @@ -273,10 +268,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver) if(filename=="") { if(solver==smt2_dect::solvert::GENERIC) - { - error() << "please use --outfile" << eom; - throw 0; - } + throw ui_exceptiont("please use --outfile"); smt2_dect *smt2_dec= new smt2_dect( @@ -318,10 +310,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver) #endif if(!*out) - { - error() << "failed to open " << filename << eom; - throw 0; - } + throw system_exceptiont("failed to open " +filename); smt2_convt *smt2_conv= new smt2_convt( @@ -344,10 +333,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver) void cbmc_solverst::no_beautification() { if(options.get_bool_option("beautify")) - { - error() << "sorry, this solver does not support beautification" << eom; - throw 0; - } + throw ui_exceptiont("sorry, this solver does not support beautification"); } void cbmc_solverst::no_incremental_check() @@ -355,8 +341,6 @@ void cbmc_solverst::no_incremental_check() if(options.get_bool_option("all-properties") || options.get_option("cover")!="" || options.get_option("incremental-check")!="") - { - error() << "sorry, this solver does not support incremental solving" << eom; - throw 0; - } + throw ui_exceptiont( + "sorry, this solver does not support incremental solving"); } diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp index f42f2dcdd13..e5721ee23e7 100644 --- a/src/cbmc/show_vcc.cpp +++ b/src/cbmc/show_vcc.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include 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 new file mode 100644 index 00000000000..fc1e2fb71a9 --- /dev/null +++ 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 diff --git a/src/util/invariant_utils.h b/src/util/invariant_utils.h index d448fedfeb3..993790cbe5d 100644 --- a/src/util/invariant_utils.h +++ b/src/util/invariant_utils.h @@ -6,8 +6,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com \*******************************************************************/ -#ifndef CPROVER_UTIL_INVARIANT_TYPES_H -#define CPROVER_UTIL_INVARIANT_TYPES_H +#ifndef CPROVER_UTIL_INVARIANT_UTILS_H +#define CPROVER_UTIL_INVARIANT_UTILS_H #include "invariant.h" @@ -45,4 +45,4 @@ std::string pretty_print_invariant_with_irep( #define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) -#endif +#endif // CPROVER_UTIL_INVARIANT_UTILS_H diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 79feb29bc8f..25f0d4d4163 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "parse_options.h" +#include "exception_utils.h" #include @@ -65,3 +66,31 @@ int parse_options_baset::main() return doit(); } + +int parse_optionst::main() +{ + // catch all exceptions here so that this code is not duplicated + // for each tool + try + { + return parse_options_baset::main(); + } + catch(const system_exceptiont &e) + { + message.error() << e.what() << messaget::eom; + } + catch(const input_src_exceptiont &e) + { + message.error().source_location=e.source_location; + message.error() << e.what() << messaget::eom; + } + catch(const ui_exceptiont &e) + { + message.error() << e.what() << messaget::eom; + } + catch(const invariant_failedt &e) + { + message.error() << e.what() << messaget::eom; + } + return 6; +} diff --git a/src/util/parse_options.h b/src/util/parse_options.h index b2e64722e85..b3a700c436a 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "cmdline.h" +#include "message.h" class parse_options_baset { @@ -35,4 +36,23 @@ class parse_options_baset bool parse_result; }; +class parse_optionst: public parse_options_baset +{ +public: + parse_optionst( + const std::string &optstring, + int argc, + const char **argv, + message_handlert &message_handler): + parse_options_baset(optstring, argc, argv), + message(message_handler) + { + } + + int main() override; + +protected: + messaget message; +}; + #endif // CPROVER_UTIL_PARSE_OPTIONS_H