diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index a971c954af5..59cebe82e2f 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006 #include #endif +#include #include #include @@ -106,6 +107,11 @@ int goto_cc_modet::main(int argc, const char **argv) error() << "Out of memory" << eom; return EX_SOFTWARE; } + catch(const cprover_exception_baset &e) + { + error() << e.what() << eom; + return EX_SOFTWARE; + } } /// prints a message informing the user about incorrect options diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp index 148ddc742cd..d43ccba01d8 100644 --- a/src/util/exception_utils.cpp +++ b/src/util/exception_utils.cpp @@ -7,14 +7,71 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com \*******************************************************************/ #include "exception_utils.h" +#include -std::string invalid_user_input_exceptiont::what() const noexcept +std::string invalid_user_input_exceptiont::what() const { std::string res; - res += "\nInvalid User Input\n"; - res += "Option: " + option + "\n"; - res += "Reason: " + reason; + res += "Invalid User Input"; + res += "\nOption: " + option; + res += "\nReason: " + reason; // Print an optional correct usage message assuming correct input parameters have been passed - res += correct_input + "\n"; + if(!correct_input.empty()) + { + res += "\nSuggestion: " + correct_input; + } return res; } + +invalid_user_input_exceptiont::invalid_user_input_exceptiont( + std::string reason, + std::string option, + std::string correct_input) + : reason(std::move(reason)), + option(std::move(option)), + correct_input(std::move(correct_input)) +{ +} + +system_exceptiont::system_exceptiont(std::string message) + : message(std::move(message)) +{ +} + +std::string system_exceptiont::what() const +{ + return message; +} + +deserialization_exceptiont::deserialization_exceptiont(std::string message) + : message(std::move(message)) +{ +} + +std::string deserialization_exceptiont::what() const +{ + return message; +} + +incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location) + : message(std::move(message)), source_location(std::move(source_location)) +{ +} + +unsupported_operation_exceptiont::unsupported_operation_exceptiont( + std::string message) + : message(std::move(message)) +{ +} + +std::string incorrect_goto_program_exceptiont::what() const +{ + return message + " (at: " + source_location.as_string() + ")"; +} + +std::string unsupported_operation_exceptiont::what() const +{ + return message; +} diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h index 4c871b94fbf..163284cf2ca 100644 --- a/src/util/exception_utils.h +++ b/src/util/exception_utils.h @@ -11,7 +11,24 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com #include -class invalid_user_input_exceptiont +#include "source_location.h" + +/// Base class for exceptions thrown in the cprover project. +/// Intended to be used as a convenient way to have a +/// "catch all and report errors" from application entry points. +class cprover_exception_baset +{ +public: + /// A human readable description of what went wrong. + /// For readability, implementors should not add a leading + /// or trailing newline to this description. + virtual std::string what() const = 0; +}; + +/// Thrown when users pass incorrect command line arguments, +/// for example passing no files to analysis or setting +/// two mutually exclusive flags +class invalid_user_input_exceptiont : public cprover_exception_baset { /// The reason this exception was generated. std::string reason; @@ -25,12 +42,69 @@ class invalid_user_input_exceptiont invalid_user_input_exceptiont( std::string reason, std::string option, - std::string correct_input = "") - : reason(reason), option(option), correct_input(correct_input) - { - } + std::string correct_input = ""); + + std::string what() const override; +}; + +/// Thrown when some external system fails unexpectedly. +/// Examples are IO exceptions (files not present, or we don't +/// have the right permissions to interact with them), timeouts for +/// external processes etc +class system_exceptiont : public cprover_exception_baset +{ +public: + explicit system_exceptiont(std::string message); + std::string what() const override; + +private: + std::string message; +}; + +/// Thrown when failing to deserialize a value from some +/// low level format, like JSON or raw bytes +class deserialization_exceptiont : public cprover_exception_baset +{ +public: + explicit deserialization_exceptiont(std::string message); + + std::string what() const override; + +private: + std::string message; +}; + +/// Thrown when a goto program that's being processed is in an invalid format, +/// for example passing the wrong number of arguments to functions. +/// Note that this only applies to goto programs that are user provided, +/// that internal transformations on goto programs don't produce invalid +/// programs should be guarded by invariants instead. +/// \see invariant.h +class incorrect_goto_program_exceptiont : public cprover_exception_baset +{ +public: + incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location); + std::string what() const override; + +private: + std::string message; + source_locationt source_location; +}; + +/// Thrown when we encounter an instruction, parameters to an instruction etc. +/// in a goto program that has some theoretically valid semantics, +/// but that we don't presently have any support for. +class unsupported_operation_exceptiont : public cprover_exception_baset +{ +public: + explicit unsupported_operation_exceptiont(std::string message); + std::string what() const override; - std::string what() const noexcept; +private: + /// The unsupported operation causing this fault to occur. + std::string message; }; #endif // CPROVER_UTIL_EXCEPTION_UTILS_H diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index b5a1b7e9b1f..770bb4ac31a 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -71,12 +71,16 @@ int parse_options_baset::main() return doit(); } - catch(invalid_user_input_exceptiont &e) + catch(const invalid_user_input_exceptiont &e) { std::cerr << e.what() << "\n"; return CPROVER_EXIT_USAGE_ERROR; } - return CPROVER_EXIT_SUCCESS; + catch(const cprover_exception_baset &e) + { + std::cerr << e.what() << '\n'; + return CPROVER_EXIT_EXCEPTION; + } } std::string