diff --git a/.travis.yml b/.travis.yml index 47296a8b5e3..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,6 +166,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 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 // 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);