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

@@ -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

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);