diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile index b561a960830..96c4a9e8077 100644 --- a/regression/invariants/Makefile +++ b/regression/invariants/Makefile @@ -4,7 +4,8 @@ SRC = driver.cpp INCLUDES = -I ../../src -OBJ += ../../src/util/util$(LIBEXT) +OBJ += ../../src/big-int/big-int$(LIBEXT) \ + ../../src/util/util$(LIBEXT) include ../../src/config.inc include ../../src/common diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index 824ae588c03..c0627bbd341 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -12,6 +12,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include #include +#include +#include /// An example of structured invariants-- this contains fields to /// describe the error to a catcher, and also produces a human-readable @@ -83,6 +85,8 @@ int main(int argc, char** argv) DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT else if(arg=="data-invariant-string") DATA_INVARIANT(false, "Test invariant failure"); + else if(arg=="irep") + INVARIANT_WITH_IREP(false, "error with irep", pointer_typet(void_typet())); else return 1; } diff --git a/regression/invariants/invariant-failure13/test.desc b/regression/invariants/invariant-failure13/test.desc new file mode 100644 index 00000000000..331889e1eb7 --- /dev/null +++ b/regression/invariants/invariant-failure13/test.desc @@ -0,0 +1,14 @@ +CORE +dummy_parameter.c +irep +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Invariant check failed +error with irep +pointer +0: empty +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/src/util/Makefile b/src/util/Makefile index 6a94cabdb88..fbea7fc6a57 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -31,6 +31,7 @@ SRC = arith_tools.cpp \ irep_hash_container.cpp \ irep_ids.cpp \ irep_serialization.cpp \ + invariant_utils.cpp \ json.cpp \ json_expr.cpp \ json_irep.cpp \ diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp index d3f750041a3..835a00b4409 100644 --- a/src/util/invariant.cpp +++ b/src/util/invariant.cpp @@ -129,7 +129,7 @@ std::string invariant_failedt::get_invariant_failed_message( << " function " << function << " line " << line << '\n' << "Reason: " << reason - << "Backtrace:\n" + << "\nBacktrace:\n" << backtrace << '\n'; return out.str(); } diff --git a/src/util/invariant_utils.cpp b/src/util/invariant_utils.cpp new file mode 100644 index 00000000000..6e1c897da54 --- /dev/null +++ b/src/util/invariant_utils.cpp @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Invariant helper utilities + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +/// \file +/// Invariant helper utilities + +#include "invariant_utils.h" + +std::string pretty_print_invariant_with_irep( + const irept &problem_node, + const std::string &description) +{ + if(problem_node.is_nil()) + return description; + else + { + std::string ret=description; + ret+="\nProblem irep:\n"; + ret+=problem_node.pretty(0,0); + return ret; + } +} diff --git a/src/util/invariant_utils.h b/src/util/invariant_utils.h new file mode 100644 index 00000000000..d448fedfeb3 --- /dev/null +++ b/src/util/invariant_utils.h @@ -0,0 +1,48 @@ +/*******************************************************************\ + +Module: Invariant helper utilities + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_INVARIANT_TYPES_H +#define CPROVER_UTIL_INVARIANT_TYPES_H + +#include "invariant.h" + +#include + +#include + +/// Produces a plain string error description from an irep and some +/// explanatory text. If `problem_node` is nil, returns `description`. +/// \param problem_node: irep to pretty-print +/// \param description: descriptive text to prepend +/// \return error message +std::string pretty_print_invariant_with_irep( + const irept &problem_node, + const std::string &description); + +/// Equivalent to +/// `INVARIANT_STRUCTURED(CONDITION, invariant_failedt, +/// pretty_print_invariant_with_irep(IREP, DESCRIPTION))` +#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_STRUCTURED( \ + CONDITION, \ + invariant_failedt, \ + pretty_print_invariant_with_irep((IREP), (DESCRIPTION))) + +/// See `INVARIANT_WITH_IREP` +#define PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) +#define POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) +#define CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) +#define UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) +#define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ + INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) + +#endif