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