Merge pull request #2930 from hannes-steffenhagen-diffblue/feature-irep_diagnostic

Add way to have irep pretty printed as diagnostic

Author: hannes-steffenhagen-diffblue

regression/invariants/driver.cpp

@@ -12,10 +12,13 @@ Author: Chris Smowton, [email protected]
 #include <string>
 #include <sstream>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/invariant_utils.h>
+#include <util/irep.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/c_types.h>
 
 /// 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;
 }

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

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)
+{
+}

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<irep_pretty_diagnosticst>
+{
+  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
+  {
+    return irep.irep.pretty();
+  }
+};
+
 #endif // CPROVER_UTIL_IREP_H