From 2ae66c2b328de35e5f3b909632d07749569641fa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Apr 2018 19:05:49 +0000 Subject: [PATCH 1/3] Produce a proper error message when catching a std::runtime_error at top level --- src/cbmc/bmc.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 37bedbed2f4..e9bae06e545 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -705,10 +705,10 @@ int bmct::do_language_agnostic_bmc( message.error() << error_msg << message.eom; return CPROVER_EXIT_EXCEPTION; } - catch(...) + catch(std::runtime_error &e) { - message.error() << "unable to get solver" << message.eom; - throw std::current_exception(); + message.error() << e.what() << message.eom; + return CPROVER_EXIT_EXCEPTION; } switch(result) From 89cf6fe6ae1e66b85f997d78c04beedfe33f8484 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Apr 2018 19:06:35 +0000 Subject: [PATCH 2/3] Throw appropriate exceptions when converting constraints --- src/goto-symex/symex_target_equation.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 0d3709dde8e..9554f1fd3a0 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -523,10 +523,19 @@ void symex_target_equationt::convert_constraints( { if(step.is_constraint()) { - if(step.ignore) - continue; - - decision_procedure.set_to_true(step.cond_expr); + if(!step.ignore) + { + try + { + decision_procedure.set_to_true(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting constraints for step", step)); + } + } } } } From 808dade2b6be43516ddb7bad52c6ffbb4aba9588 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Apr 2018 19:07:11 +0000 Subject: [PATCH 3/3] Provide suitable diagnostics for equality-without-matching-types --- src/solvers/flattening/boolbv_equality.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 8621efa3cbe..2e7ac9aa500 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -12,16 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "bv_conversion_exceptions.h" #include "flatten_byte_operators.h" literalt boolbvt::convert_equality(const equal_exprt &expr) { const bool is_base_type_eq = base_type_eq(expr.lhs().type(), expr.rhs().type(), ns); - DATA_INVARIANT( - is_base_type_eq, - std::string("equality without matching types:\n") + "######### lhs: " + - expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty()); + if(!is_base_type_eq) + { + const std::string error_msg = + std::string("equality without matching types:\n") + "######### lhs: " + + expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty(); + throw bitvector_conversion_exceptiont(error_msg, expr); + } // see if it is an unbounded array if(is_unbounded_array(expr.lhs().type()))