diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index b15a54e9935..fa62a53c6d9 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "set_properties.h" +#include + #include #include @@ -111,7 +113,9 @@ void set_properties( set_properties(it->second.body, property_set); if(!property_set.empty()) - throw "property "+id2string(*property_set.begin())+" not found"; + throw invalid_command_line_argument_exceptiont( + "property " + id2string(*property_set.begin()) + " unknown", + "--property id"); } void label_properties(goto_functionst &goto_functions) diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index ed50376570c..df39dee7f71 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -21,6 +21,8 @@ Date: December 2016 #include #include +#include + #include #include @@ -32,8 +34,8 @@ void slice_global_inits(goto_modelt &goto_model) const irep_idt entry_point=goto_functionst::entry_point(); goto_functionst &goto_functions=goto_model.goto_functions; - if(!goto_functions.function_map.count(entry_point)) - throw "entry point not found"; + if(goto_functions.function_map.count(entry_point) == 0) + throw user_input_error_exceptiont("entry point not found"); // Get the call graph restricted to functions reachable from // the entry point: @@ -73,7 +75,8 @@ void slice_global_inits(goto_modelt &goto_model) goto_functionst::function_mapt::iterator f_it; f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION); - assert(f_it!=goto_functions.function_map.end()); + if(f_it == goto_functions.function_map.end()) + throw incorrect_goto_program_exceptiont("initialize function not found"); goto_programt &goto_program=f_it->second.body; diff --git a/src/goto-programs/slice_global_inits.h b/src/goto-programs/slice_global_inits.h index 9067bf83a57..9ba29c8864a 100644 --- a/src/goto-programs/slice_global_inits.h +++ b/src/goto-programs/slice_global_inits.h @@ -14,8 +14,27 @@ Date: December 2016 #ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H #define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H +#include + class goto_modelt; +class user_input_error_exceptiont : public cprover_exception_baset +{ +public: + explicit user_input_error_exceptiont(std::string message) + : message(std::move(message)) + { + } + + std::string what() const override + { + return message; + } + +private: + std::string message; +}; + void slice_global_inits(goto_modelt &); #endif diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 77e954b0aaa..6a6a13ef206 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -16,9 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include -#include #include +#include #include #include @@ -279,9 +280,9 @@ void string_instrumentationt::do_sprintf( if(arguments.size()<2) { - error().source_location=target->source_location; - error() << "sprintf expected to have two or more arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "sprintf expected to have two or more arguments", + target->source_location); } goto_programt tmp; @@ -321,10 +322,9 @@ void string_instrumentationt::do_snprintf( if(arguments.size()<3) { - error().source_location=target->source_location; - error() << "snprintf expected to have three or more arguments" - << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "snprintf expected to have three or more arguments", + target->source_location); } goto_programt tmp; @@ -364,9 +364,8 @@ void string_instrumentationt::do_fscanf( if(arguments.size()<2) { - error().source_location=target->source_location; - error() << "fscanf expected to have two or more arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "fscanf expected to have two or more arguments", target->source_location); } goto_programt tmp; @@ -650,9 +649,8 @@ void string_instrumentationt::do_strchr( if(arguments.size()!=2) { - error().source_location=target->source_location; - error() << "strchr expected to have two arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "strchr expected to have two arguments", target->source_location); } goto_programt tmp; @@ -677,9 +675,8 @@ void string_instrumentationt::do_strrchr( if(arguments.size()!=2) { - error().source_location=target->source_location; - error() << "strrchr expected to have two arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "strrchr expected to have two arguments", target->source_location); } goto_programt tmp; @@ -704,9 +701,8 @@ void string_instrumentationt::do_strstr( if(arguments.size()!=2) { - error().source_location=target->source_location; - error() << "strstr expected to have two arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "strstr expected to have two arguments", target->source_location); } goto_programt tmp; @@ -738,9 +734,8 @@ void string_instrumentationt::do_strtok( if(arguments.size()!=2) { - error().source_location=target->source_location; - error() << "strtok expected to have two arguments" << eom; - throw 0; + throw incorrect_source_program_exceptiont( + "strtok expected to have two arguments", target->source_location); } goto_programt tmp; diff --git a/src/goto-programs/string_instrumentation.h b/src/goto-programs/string_instrumentation.h index 0314fe87305..68ce5d6621f 100644 --- a/src/goto-programs/string_instrumentation.h +++ b/src/goto-programs/string_instrumentation.h @@ -14,9 +14,30 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" +#include + class message_handlert; class goto_modelt; +class incorrect_source_program_exceptiont : public cprover_exception_baset +{ +public: + incorrect_source_program_exceptiont( + std::string message, + source_locationt source_location) + : message(std::move(message)), source_location(std::move(source_location)) + { + } + std::string what() const override + { + return message + " (at: " + source_location.as_string() + ")"; + } + +private: + std::string message; + source_locationt source_location; +}; + void string_instrumentation( symbol_tablet &, message_handlert &, diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 976b1e38733..c8bd3759891 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -13,7 +13,6 @@ Date: June 2011 #include "vcd_goto_trace.h" -#include #include #include @@ -55,8 +54,7 @@ std::string as_vcd_binary( } else if(expr.id()==ID_union) { - assert(expr.operands().size()==1); - return as_vcd_binary(expr.op0(), ns); + return as_vcd_binary(to_union_expr(expr).op(), ns); } // build "xxx" diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index 919af668fd8..8c44985bbf8 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + bool has_nondet(const exprt &dest) { forall_operands(it, dest) @@ -263,6 +265,6 @@ exprt wp( return post; // ignored else if(statement==ID_fence) return post; // ignored - else - throw "sorry, wp("+id2string(statement)+"...) not implemented"; + INVARIANT_WITH_DIAGNOSTICS( + false, "sorry, wp(", id2string(statement), "...) is not implemented"); } diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 3ab58528319..fdebda05b43 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -13,8 +13,10 @@ Author: CM Wintersteiger #include -#include +#include +#include #include +#include #include #include @@ -148,22 +150,18 @@ bool write_goto_binary( irep_serializationt::ireps_containert irepc; irep_serializationt irepconverter(irepc); - switch(version) - { - case 1: - case 2: - case 3: - throw "version no longer supported"; - - case 4: + const int current_goto_version = 4; + if(version < current_goto_version) + throw invalid_command_line_argument_exceptiont( + "version " + std::to_string(version) + " no longer supported", + "supported version = " + std::to_string(current_goto_version)); + else if(version > current_goto_version) + throw invalid_command_line_argument_exceptiont( + "unknown goto binary version " + std::to_string(version), + "supported version = " + std::to_string(current_goto_version)); + else return write_goto_binary_v4( out, symbol_table, goto_functions, irepconverter); - - default: - throw "unknown goto binary version"; - } - - return false; } /// Writes a goto program to disc diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp index afdf4ca5868..66683b0c1a6 100644 --- a/src/util/exception_utils.cpp +++ b/src/util/exception_utils.cpp @@ -64,6 +64,17 @@ incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( std::string incorrect_goto_program_exceptiont::what() const { return message + " (at: " + source_location.as_string() + ")"; + if(source_location.is_nil()) + return message; + else + return message + " (at: " + source_location.as_string() + ")"; +} + +incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( + std::string message) + : message(std::move(message)) +{ + source_location.make_nil(); } unsupported_operation_exceptiont::unsupported_operation_exceptiont( diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h index cb8e52d7c6e..7dd95ca559f 100644 --- a/src/util/exception_utils.h +++ b/src/util/exception_utils.h @@ -86,6 +86,7 @@ class incorrect_goto_program_exceptiont : public cprover_exception_baset incorrect_goto_program_exceptiont( std::string message, source_locationt source_location); + explicit incorrect_goto_program_exceptiont(std::string message); std::string what() const override; private: