Merge pull request #1477 from andreast271/travis-NDEBUG-build

Compile cbmc with NDEBUG using gcc tool chain on linux.

Author: tautschnig

.travis.yml

@@ -117,7 +117,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
@@ -140,6 +140,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
@@ -167,6 +168,7 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       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);