diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class new file mode 100644 index 00000000000..66e0d073242 Binary files /dev/null and b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class differ diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java new file mode 100644 index 00000000000..16d680bd804 --- /dev/null +++ b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java @@ -0,0 +1,7 @@ +public class TestClass { + public static void f(int y) { + float[][] a1 = new float[y][3]; + int j = 0; + a1[j][0] = 34.5f; + } +} diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc b/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc new file mode 100644 index 00000000000..c9600f50852 --- /dev/null +++ b/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc @@ -0,0 +1,10 @@ +CORE +TestClass.class +--function TestClass.f --cover location --unwind 2 +Source GOTO statement: .* +(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows) +^EXIT=6$ +-- +-- +The exception thrown in this test is the symptom of a bug; the purpose of this +test is the validate the output of that exception diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h new file mode 100644 index 00000000000..f2055c1c9ec --- /dev/null +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Symbolic Execution + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Exceptions that can be raised during the equation conversion phase + +#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H +#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H + +#include + +#include + +#include "symex_target_equation.h" + +class equation_conversion_exceptiont : public std::runtime_error +{ +public: + equation_conversion_exceptiont( + const std::string &message, + const symex_target_equationt::SSA_stept &step) + : runtime_error(message), step(step) + { + std::ostringstream error_msg; + error_msg << runtime_error::what(); + error_msg << "\nSource GOTO statement: " << format(step.source.pc->code); + error_msg << "\nStep:\n"; + step.output(error_msg); + error_message = error_msg.str(); + } + + const char *what() const optional_noexcept override + { + return error_message.c_str(); + } + +private: + symex_target_equationt::SSA_stept step; + std::string error_message; +}; + +#endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 27be83608f1..0d3709dde8e 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -11,13 +11,20 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" +#include #include +#include +#include +// Can be removed once deprecated SSA_stept::output is removed #include -#include -#include + +#include #include +#include +#include +#include "equation_conversion_exceptions.h" #include "goto_symex_state.h" /// read from a shared variable @@ -368,14 +375,23 @@ void symex_target_equationt::constraint( void symex_target_equationt::convert( prop_convt &prop_conv) { - convert_guards(prop_conv); - convert_assignments(prop_conv); - convert_decls(prop_conv); - convert_assumptions(prop_conv); - convert_assertions(prop_conv); - convert_goto_instructions(prop_conv); - convert_io(prop_conv); - convert_constraints(prop_conv); + try + { + convert_guards(prop_conv); + convert_assignments(prop_conv); + convert_decls(prop_conv); + convert_assumptions(prop_conv); + convert_assertions(prop_conv); + convert_goto_instructions(prop_conv); + convert_io(prop_conv); + convert_constraints(prop_conv); + } + catch(const equation_conversion_exceptiont &conversion_exception) + { + // unwrap the except and throw like normal + const std::string full_error = unwrap_exception(conversion_exception); + throw full_error; + } } /// converts assignments @@ -402,7 +418,16 @@ void symex_target_equationt::convert_decls( { // The result is not used, these have no impact on // the satisfiability of the formula. - prop_conv.convert(step.cond_expr); + try + { + prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting decls for step", step)); + } } } } @@ -417,7 +442,18 @@ void symex_target_equationt::convert_guards( if(step.ignore) step.guard_literal=const_literal(false); else - step.guard_literal=prop_conv.convert(step.guard); + { + try + { + step.guard_literal = prop_conv.convert(step.guard); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting guard for step", step)); + } + } } } @@ -433,7 +469,18 @@ void symex_target_equationt::convert_assumptions( if(step.ignore) step.cond_literal=const_literal(true); else - step.cond_literal=prop_conv.convert(step.cond_expr); + { + try + { + step.cond_literal = prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting assumptions for step", step)); + } + } } } } @@ -450,7 +497,18 @@ void symex_target_equationt::convert_goto_instructions( if(step.ignore) step.cond_literal=const_literal(true); else - step.cond_literal=prop_conv.convert(step.cond_expr); + { + try + { + step.cond_literal = prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting goto instructions for step", step)); + } + } } } } @@ -519,7 +577,16 @@ void symex_target_equationt::convert_assertions( step.cond_expr); // do the conversion - step.cond_literal=prop_conv.convert(implication); + try + { + step.cond_literal = prop_conv.convert(implication); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting assertions for step", step)); + } // store disjunct disjuncts.push_back(literal_exprt(!step.cond_literal)); @@ -703,3 +770,118 @@ void symex_target_equationt::SSA_stept::output( out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n'; } + +void symex_target_equationt::SSA_stept::output(std::ostream &out) const +{ + if(source.is_set) + { + out << "Thread " << source.thread_nr; + + if(source.pc->source_location.is_not_nil()) + out << " " << source.pc->source_location << '\n'; + else + out << '\n'; + } + + switch(type) + { + case goto_trace_stept::typet::ASSERT: + out << "ASSERT " << format(cond_expr) << '\n'; + break; + case goto_trace_stept::typet::ASSUME: + out << "ASSUME " << format(cond_expr) << '\n'; + break; + case goto_trace_stept::typet::LOCATION: + out << "LOCATION" << '\n'; + break; + case goto_trace_stept::typet::INPUT: + out << "INPUT" << '\n'; + break; + case goto_trace_stept::typet::OUTPUT: + out << "OUTPUT" << '\n'; + break; + + case goto_trace_stept::typet::DECL: + out << "DECL" << '\n'; + out << format(ssa_lhs) << '\n'; + break; + + case goto_trace_stept::typet::ASSIGNMENT: + out << "ASSIGNMENT ("; + switch(assignment_type) + { + case assignment_typet::HIDDEN: + out << "HIDDEN"; + break; + case assignment_typet::STATE: + out << "STATE"; + break; + case assignment_typet::VISIBLE_ACTUAL_PARAMETER: + out << "VISIBLE_ACTUAL_PARAMETER"; + break; + case assignment_typet::HIDDEN_ACTUAL_PARAMETER: + out << "HIDDEN_ACTUAL_PARAMETER"; + break; + case assignment_typet::PHI: + out << "PHI"; + break; + case assignment_typet::GUARD: + out << "GUARD"; + break; + default: + { + } + } + + out << ")\n"; + break; + + case goto_trace_stept::typet::DEAD: + out << "DEAD\n"; + break; + case goto_trace_stept::typet::FUNCTION_CALL: + out << "FUNCTION_CALL\n"; + break; + case goto_trace_stept::typet::FUNCTION_RETURN: + out << "FUNCTION_RETURN\n"; + break; + case goto_trace_stept::typet::CONSTRAINT: + out << "CONSTRAINT\n"; + break; + case goto_trace_stept::typet::SHARED_READ: + out << "SHARED READ\n"; + break; + case goto_trace_stept::typet::SHARED_WRITE: + out << "SHARED WRITE\n"; + break; + case goto_trace_stept::typet::ATOMIC_BEGIN: + out << "ATOMIC_BEGIN\n"; + break; + case goto_trace_stept::typet::ATOMIC_END: + out << "AUTOMIC_END\n"; + break; + case goto_trace_stept::typet::SPAWN: + out << "SPAWN\n"; + break; + case goto_trace_stept::typet::MEMORY_BARRIER: + out << "MEMORY_BARRIER\n"; + break; + case goto_trace_stept::typet::GOTO: + out << "IF " << format(cond_expr) << " GOTO\n"; + break; + + default: + UNREACHABLE; + } + + if(is_assert() || is_assume() || is_assignment() || is_constraint()) + out << format(cond_expr) << '\n'; + + if(is_assert() || is_constraint()) + out << comment << '\n'; + + if(is_shared_read() || is_shared_write()) + out << format(ssa_lhs) << '\n'; + + out << "Guard: " << format(guard) << '\n'; +} diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 178cbeae7ab..bada3f9d871 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -32,7 +32,6 @@ class prop_convt; class symex_target_equationt:public symex_targett { public: - symex_target_equationt() = default; virtual ~symex_target_equationt() = default; // read event @@ -257,9 +256,12 @@ class symex_target_equationt:public symex_targett { } + DEPRECATED("Use output without ns param") void output( const namespacet &ns, std::ostream &out) const; + + void output(std::ostream &out) const; }; std::size_t count_assertions() const diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index a61e50a0f33..40ddc83e3d6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -152,6 +152,14 @@ bvt boolbvt::conversion_failed(const exprt &expr) return prop.new_variables(width); } +/// Converts an expression into its gate-level representation and returns a +/// vector of literals corresponding to the outputs of the Boolean circuit. +/// \param expr: Expression to convert +/// \return A vector of literals corresponding to the outputs of the Boolean +/// circuit +/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction +/// goes wrong. +/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103). bvt boolbvt::convert_bitvector(const exprt &expr) { if(expr.type().id()==ID_bool) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 0cc2c46bd89..f3841a6f0f3 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -11,10 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include +#include +#include +#include "bv_conversion_exceptions.h" +#include "flatten_byte_extract_exceptions.h" #include "flatten_byte_operators.h" bvt map_bv(const endianness_mapt &map, const bvt &src) @@ -42,8 +45,16 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // if we extract from an unbounded array, call the flattening code if(is_unbounded_array(expr.op().type())) { - exprt tmp=flatten_byte_extract(expr, ns); - return convert_bv(tmp); + try + { + exprt tmp = flatten_byte_extract(expr, ns); + return convert_bv(tmp); + } + catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception) + { + util_throw_with_nested( + bitvector_conversion_exceptiont("Can't convert byte_extraction", expr)); + } } std::size_t width=boolbv_width(expr.type()); diff --git a/src/solvers/flattening/bv_conversion_exceptions.h b/src/solvers/flattening/bv_conversion_exceptions.h new file mode 100644 index 00000000000..2d3bbd2410b --- /dev/null +++ b/src/solvers/flattening/bv_conversion_exceptions.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Bit vector conversion + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Exceptions that can be raised in bv_conversion + +#ifndef CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H +#define CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H + +#include +#include + +#include + +class bitvector_conversion_exceptiont : public std::runtime_error +{ +public: + bitvector_conversion_exceptiont( + const std::string &exception_message, + const exprt &bv_expr) + : runtime_error(exception_message), bv_expr(bv_expr) + { + } + +private: + exprt bv_expr; +}; + +#endif // CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H diff --git a/src/solvers/flattening/flatten_byte_extract_exceptions.h b/src/solvers/flattening/flatten_byte_extract_exceptions.h new file mode 100644 index 00000000000..a5ae22791b3 --- /dev/null +++ b/src/solvers/flattening/flatten_byte_extract_exceptions.h @@ -0,0 +1,144 @@ +/*******************************************************************\ + +Module: Byte flattening + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H +#define CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H + +#include +#include +#include + +#include +#include + +class flatten_byte_extract_exceptiont : public std::runtime_error +{ +public: + explicit flatten_byte_extract_exceptiont(const std::string &exception_message) + : runtime_error(exception_message) + { + } +}; + +class non_const_array_sizet : public flatten_byte_extract_exceptiont +{ +public: + non_const_array_sizet(const array_typet &array_type, const exprt &max_bytes) + : flatten_byte_extract_exceptiont("cannot unpack array of non-const size"), + max_bytes(max_bytes), + array_type(array_type) + { + std::ostringstream error_message; + error_message << runtime_error::what() << "\n"; + error_message << "array_type: " << array_type.pretty(); + error_message << "\nmax_bytes: " << max_bytes.pretty(); + computed_error_message = error_message.str(); + } + + const char *what() const optional_noexcept override + { + return computed_error_message.c_str(); + } + +private: + exprt max_bytes; + array_typet array_type; + + std::string computed_error_message; +}; + +class non_byte_alignedt : public flatten_byte_extract_exceptiont +{ +public: + non_byte_alignedt( + const struct_typet &struct_type, + const struct_union_typet::componentt &component, + const mp_integer &byte_width) + : flatten_byte_extract_exceptiont( + "cannot unpack struct with non-byte aligned components"), + struct_type(struct_type), + component(component), + byte_width(byte_width) + { + std::ostringstream error_message; + error_message << runtime_error::what() << "\n"; + error_message << "width: " << byte_width << "\n"; + error_message << "component:" << component.get_name() << "\n"; + error_message << "struct_type: " << struct_type.pretty(); + computed_error_message = error_message.str(); + } + + const char *what() const optional_noexcept override + { + return computed_error_message.c_str(); + } + +private: + const struct_typet struct_type; + const struct_union_typet::componentt component; + const mp_integer byte_width; + + std::string computed_error_message; +}; + +class non_constant_widtht : public flatten_byte_extract_exceptiont +{ +public: +public: + non_constant_widtht(const exprt &src, const exprt &max_bytes) + : flatten_byte_extract_exceptiont( + "cannot unpack object of non-constant width"), + src(src), + max_bytes(max_bytes) + { + std::ostringstream error_message; + error_message << runtime_error::what() << "\n"; + error_message << "array_type: " << src.pretty(); + error_message << "\nmax_bytes: " << max_bytes.pretty(); + computed_error_message = error_message.str(); + } + + const char *what() const optional_noexcept override + { + return computed_error_message.c_str(); + } + +private: + exprt src; + exprt max_bytes; + + std::string computed_error_message; +}; + +class non_const_byte_extraction_sizet : public flatten_byte_extract_exceptiont +{ +public: + explicit non_const_byte_extraction_sizet( + const byte_extract_exprt &unpack_expr) + : flatten_byte_extract_exceptiont( + "byte_extract flatting with non-constant size"), + unpack_expr(unpack_expr) + { + std::ostringstream error_message; + error_message << runtime_error::what() << "\n"; + error_message << "unpack_expr: " << unpack_expr.pretty(); + computed_error_message = error_message.str(); + } + + const char *what() const optional_noexcept override + { + return computed_error_message.c_str(); + } + +private: + const byte_extract_exprt unpack_expr; + + std::string computed_error_message; +}; + +#endif // CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index c564b48df02..42054cc61dc 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "flatten_byte_extract_exceptions.h" #include "flatten_byte_operators.h" /// rewrite an object into its individual bytes @@ -25,6 +26,9 @@ Author: Daniel Kroening, kroening@kroening.com /// max_bytes if not nil, use as upper bound of the number of bytes to unpack /// ns namespace for type lookups /// \return array of bytes in the sequence found in memory +/// \throws flatten_byte_extract_exceptiont Raised is unable to unpack the +/// object because of either non constant size, byte misalignment or +/// non-constant component width. static exprt unpack_rec( const exprt &src, bool little_endian, @@ -63,7 +67,9 @@ static exprt unpack_rec( mp_integer num_elements; if(to_integer(max_bytes, num_elements) && to_integer(array_type.size(), num_elements)) - throw "cannot unpack array of non-const size:\n"+type.pretty(); + { + throw non_const_array_sizet(array_type, max_bytes); + } // all array members will have the same structure; do this just // once and then replace the dummy symbol by a suitable index @@ -97,8 +103,9 @@ static exprt unpack_rec( // the next member would be misaligned, abort if(element_width<=0 || element_width%8!=0) - throw "cannot unpack struct with non-byte aligned components:\n"+ - struct_type.pretty(); + { + throw non_byte_alignedt(struct_type, comp, element_width); + } member_exprt member(src, comp.get_name(), comp.type()); exprt sub=unpack_rec(member, little_endian, max_bytes, ns, true); @@ -115,8 +122,9 @@ static exprt unpack_rec( if(bits<0) { if(to_integer(max_bytes, bits)) - throw "cannot unpack object of non-constant width:\n"+ - src.pretty(); + { + throw non_constant_widtht(src, max_bytes); + } else bits*=8; } @@ -300,8 +308,9 @@ exprt flatten_byte_extract( { mp_integer op0_bits=pointer_offset_bits(unpacked.op().type(), ns); if(op0_bits<0) - throw "byte_extract flatting with non-constant size:\n"+ - unpacked.pretty(); + { + throw non_const_byte_extraction_sizet(unpacked); + } else size_bits=op0_bits; } diff --git a/src/util/Makefile b/src/util/Makefile index cb9d221dd60..74fc5aec412 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -96,6 +96,7 @@ SRC = arith_tools.cpp \ unicode.cpp \ union_find.cpp \ union_find_replace.cpp \ + unwrap_nested_exception.cpp \ xml.cpp \ xml_expr.cpp \ xml_irep.cpp \ diff --git a/src/util/throw_with_nested.h b/src/util/throw_with_nested.h new file mode 100644 index 00000000000..444a7a60e6b --- /dev/null +++ b/src/util/throw_with_nested.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + +Module: util + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_THROW_WITH_NESTED_H +#define CPROVER_UTIL_THROW_WITH_NESTED_H + +#include + +#ifdef _MSC_VER +#include +// TODO(tkiley): Nested exception logging not supported on windows due to a bug +// TODO(tkiley): in MSVC++ Compiler (diffblue/cbmc#2104): +// TODO(tkiley): https://blogs.msdn.microsoft.com/vcblog/2016/01/22/vs-2015-update-2s-stl-is-c17-so-far-feature-complete + +#define DISABLE_NESTED_EXCEPTIONS + +class non_nested_exception_support : public std::runtime_error +{ +public: + non_nested_exception_support() + : std::runtime_error("Nested exception printing not supported on Windows") + { + } +}; + +#endif + +template +#ifdef __GNUC__ +__attribute__((noreturn)) +#endif +void util_throw_with_nested(T &&t) +{ +#ifndef DISABLE_NESTED_EXCEPTIONS + std::throw_with_nested(t); +#else + throw t; +#endif +} + +template +void util_rethrow_if_nested(const E &e) +{ +#ifndef DISABLE_NESTED_EXCEPTIONS + std::rethrow_if_nested(e); +#else + // Check we've not already thrown the non_nested_support_exception + if(!dynamic_cast(&e)) + { + throw non_nested_exception_support(); + } +#endif +} + +#endif // CPROVER_UTIL_THROW_WITH_NESTED_H diff --git a/src/util/unwrap_nested_exception.cpp b/src/util/unwrap_nested_exception.cpp new file mode 100644 index 00000000000..0689391466b --- /dev/null +++ b/src/util/unwrap_nested_exception.cpp @@ -0,0 +1,54 @@ +/*******************************************************************\ + +Module: util + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "unwrap_nested_exception.h" +#include "invariant.h" +#include "string_utils.h" +#include "suffix.h" +#include "throw_with_nested.h" + +#include +#include + +/// Given a potentially nested exception, produce a string with all of nested +/// exceptions information. If a nested exception string contains new lines +/// then the newlines are indented to the correct level. +/// \param e: The outer exeception +/// \param level: How many exceptions have already been unrolled +/// \return A string with all nested exceptions printed and indented +std::string unwrap_exception(const std::exception &e, int level) +{ + const std::string msg = e.what(); + std::vector lines; + split_string(msg, '\n', lines, false, true); + std::ostringstream message_stream; + message_stream << std::string(level, ' ') << "exception: "; + join_strings( + message_stream, lines.begin(), lines.end(), "\n" + std::string(level, ' ')); + + try + { + util_rethrow_if_nested(e); + } + catch(const std::exception &e) + { + std::string nested_message = unwrap_exception(e, level + 1); + // Some exception messages already end in a new line (e.g. as they have + // dumped an irept. Most do not so add a new line on. + if(nested_message.back() != '\n') + { + message_stream << '\n'; + } + message_stream << nested_message; + } + catch(...) + { + UNREACHABLE; + } + return message_stream.str(); +} diff --git a/src/util/unwrap_nested_exception.h b/src/util/unwrap_nested_exception.h new file mode 100644 index 00000000000..4e2903c2c00 --- /dev/null +++ b/src/util/unwrap_nested_exception.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +Module: util + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H +#define CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H + +#include +#include + +std::string unwrap_exception(const std::exception &e, int level = 0); + +#endif // CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H