diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index aadfac36fd5..b19b443576b 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -12,10 +12,13 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +#include +#include #include #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 @@ -149,6 +152,15 @@ int main(int argc, char** argv) "an invariant with some custom diagnostics", DiagnosticA{}, DiagnosticB{}); + else if(arg == "invariant-with-irep-diagnostics") + { + INVARIANT_WITH_DIAGNOSTICS( + false, + "an invariant with irep diagnostics", + irep_pretty_diagnosticst{ + plus_exprt{from_integer(8, signedbv_typet(32)), + from_integer(13, signedbv_typet(32))}}); + } else return 1; } diff --git a/regression/invariants/invariant-irep-diagnostic/test.desc b/regression/invariants/invariant-irep-diagnostic/test.desc new file mode 100644 index 00000000000..a975023b7b4 --- /dev/null +++ b/regression/invariants/invariant-irep-diagnostic/test.desc @@ -0,0 +1,9 @@ +CORE +dummy_parameter.c +invariant-with-irep-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Invariant check failed +value: 00000000000000000000000000001000 +value: 00000000000000000000000000001101 diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 1eec748f5d3..b403ea96550 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -689,3 +689,8 @@ std::string irept::pretty(unsigned indent, unsigned max_indent) const return result; } + +irep_pretty_diagnosticst::irep_pretty_diagnosticst(const irept &irep) + : irep(irep) +{ +} diff --git a/src/util/irep.h b/src/util/irep.h index f1fb120fa2c..706fb60db26 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -463,4 +463,19 @@ struct irep_full_eq } }; +struct irep_pretty_diagnosticst +{ + const irept &irep; + explicit irep_pretty_diagnosticst(const irept &irep); +}; + +template <> +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep) + { + return irep.irep.pretty(); + } +}; + #endif // CPROVER_UTIL_IREP_H