From 997b51af066776d9394076631be3d1657e376584 Mon Sep 17 00:00:00 2001
From: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Date: Tue, 26 May 2020 15:37:39 +0100
Subject: [PATCH] Add pretty printing for exprts in Catch assertions

Without a pretty printer exprt's just show up as ? in
catch assertions, which isn't very helpful.
---
 unit/testing-utils/catch_pretty_print_expr.h | 39 ++++++++++++++++++++
 unit/testing-utils/use_catch.h               |  2 +
 2 files changed, 41 insertions(+)
 create mode 100644 unit/testing-utils/catch_pretty_print_expr.h

diff --git a/unit/testing-utils/catch_pretty_print_expr.h b/unit/testing-utils/catch_pretty_print_expr.h
new file mode 100644
index 00000000000..fa86e93146c
--- /dev/null
+++ b/unit/testing-utils/catch_pretty_print_expr.h
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Pretty print exprts in Catch assertions
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_TESTING_UTILS_CATCH_PRETTY_PRINT_EXPR_H
+#define CPROVER_TESTING_UTILS_CATCH_PRETTY_PRINT_EXPR_H
+
+// this file is expected to be included from `use_catch.hpp`,
+// this include is only here to make editor syntax highlighting
+// work better
+#include <catch/catch.hpp>
+
+#include <ansi-c/expr2c.h>
+#include <util/expr.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+namespace Catch // NOLINT
+{
+template <>
+struct StringMaker<exprt> // NOLINT
+{
+  static std::string convert(const exprt &expr)
+  {
+    // expr2c doesn’t capture everything that’s contained
+    // within an expr, but it’s fairly compact.
+    // expr.pretty() could also work and is more precise,
+    // but leads to very large output multiple lines which
+    // makes it hard to see differences.
+    return expr2c(expr, namespacet{symbol_tablet{}});
+  }
+};
+} // namespace Catch
+
+#endif // CPROVER_TESTING_UTILS_CATCH_PRETTY_PRINT_EXPR_H
diff --git a/unit/testing-utils/use_catch.h b/unit/testing-utils/use_catch.h
index 430c8a51c02..a25b46b718a 100644
--- a/unit/testing-utils/use_catch.h
+++ b/unit/testing-utils/use_catch.h
@@ -39,4 +39,6 @@ Author: Michael Tautschnig
 /// Add to the end of test tags to mark a test that is expected to fail
 #define XFAIL "[.][!shouldfail]"
 
+#include "catch_pretty_print_expr.h"
+
 #endif // CPROVER_TESTING_UTILS_USE_CATCH_H