From 4fa3ba50152a768833a24476044fa7a359a9a3ec Mon Sep 17 00:00:00 2001
From: Andreas Tiemeyer <andreas.tiemeyer@gmx.com>
Date: Fri, 13 Oct 2017 07:50:21 +0100
Subject: [PATCH 1/2] Create separate clang build with NDEBUG and
 CPROVER_INVARIANT_DO_NOT_CHECK Fix INVARIANT macros for
 CPROVER_INVARIANT_DO_NOT_CHECK and CPROVER_INVARIANT_ASSERT In NDEBUG build,
 disable known warnings caused by the disabled versions of the INVARIANT
 macros.

---
 .travis.yml          | 27 +++++++++++++++++++++++++++
 src/util/invariant.h | 11 +++++++----
 2 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 47296a8b5e3..00ef60eb6cc 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -165,6 +165,33 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    # Ubuntu Linux with glibc using clang++-3.7, no-debug mode
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      sudo: false
+      compiler: clang
+      cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - llvm-toolchain-precise-3.7
+          packages:
+            - libwww-perl
+            - clang-3.7
+            - libstdc++-5-dev
+            - libubsan0
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - export CCACHE_CPP2=yes
+      env:
+        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - CCACHE_CPP2=yes
+        # Disable known warnings caused by -DCPROVER_INVARIANT_DO_NOT_CHECK.
+        - EXTRA_CXXFLAGS="-DNDEBUG -DCPROVER_INVARIANT_DO_NOT_CHECK -Wno-return-type -Wno-unused-variable -Wno-sometimes-uninitialized -Wno-unused-function"
+      script: echo "Not running any tests for a debug build."
+
+    # cmake build using g++-5
     - stage: Test different OS/CXX/Flags
       os: linux
       cache: ccache
diff --git a/src/util/invariant.h b/src/util/invariant.h
index cd8fa2c8e01..03d33692ce8 100644
--- a/src/util/invariant.h
+++ b/src/util/invariant.h
@@ -83,7 +83,6 @@ class invariant_failedt: public std::logic_error
     const std::string &reason);
 
  public:
-
   const std::string file;
   const std::string function;
   const int line;
@@ -117,20 +116,24 @@ class invariant_failedt: public std::logic_error
 #define INVARIANT(CONDITION, REASON) \
   __CPROVER_assert((CONDITION), "Invariant : " REASON)
 
+#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
+  INVARIANT(CONDITION, "")
 
 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
 // For performance builds, invariants can be ignored
 // This is *not* recommended as it can result in unpredictable behaviour
 // including silently reporting incorrect results.
 // This is also useful for checking side-effect freedom.
-#define INVARIANT(CONDITION, REASON, ...) do {} while(0)
+#define INVARIANT(CONDITION, REASON) do {} while(0)
+#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(0)
 
 #elif defined(CPROVER_INVARIANT_ASSERT)
 // Not recommended but provided for backwards compatability
 #include <cassert>
 // NOLINTNEXTLINE(*)
-#define INVARIANT(CONDITION, REASON, ...) assert((CONDITION) && ((REASON), true))
-
+#define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
+// NOLINTNEXTLINE(*)
+#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
 #else
 
 void print_backtrace(std::ostream &out);

From 2177bbc901e09faad8027a723f62a4f75bf5ebb2 Mon Sep 17 00:00:00 2001
From: Andreas Tiemeyer <andreas.tiemeyer@gmx.com>
Date: Wed, 1 Nov 2017 07:58:09 +0000
Subject: [PATCH 2/2] Remove extra build with NDEBUG that compiles but doesn't
 test. Instead, add NDEBUG to a linux clang build that runs regression.

---
 .travis.yml | 29 ++---------------------------
 1 file changed, 2 insertions(+), 27 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 00ef60eb6cc..44ef3053c5f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -115,7 +115,7 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    # Ubuntu Linux with glibc using clang++-3.7
+    # Ubuntu Linux with glibc using clang++-3.7, no-debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -138,6 +138,7 @@ jobs:
       env:
         - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
+        - EXTRA_CXXFLAGS="-DNDEBUG"
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
     - stage: Test different OS/CXX/Flags
@@ -165,32 +166,6 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    # Ubuntu Linux with glibc using clang++-3.7, no-debug mode
-    - stage: Test different OS/CXX/Flags
-      os: linux
-      sudo: false
-      compiler: clang
-      cache: ccache
-      addons:
-        apt:
-          sources:
-            - ubuntu-toolchain-r-test
-            - llvm-toolchain-precise-3.7
-          packages:
-            - libwww-perl
-            - clang-3.7
-            - libstdc++-5-dev
-            - libubsan0
-      before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
-        - export CCACHE_CPP2=yes
-      env:
-        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
-        - CCACHE_CPP2=yes
-        # Disable known warnings caused by -DCPROVER_INVARIANT_DO_NOT_CHECK.
-        - EXTRA_CXXFLAGS="-DNDEBUG -DCPROVER_INVARIANT_DO_NOT_CHECK -Wno-return-type -Wno-unused-variable -Wno-sometimes-uninitialized -Wno-unused-function"
-      script: echo "Not running any tests for a debug build."
-
     # cmake build using g++-5
     - stage: Test different OS/CXX/Flags
       os: linux