Skip to content

Compile cbmc with NDEBUG using gcc tool chain on linux. #1477

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Nov 30, 2017
Merged

Compile cbmc with NDEBUG using gcc tool chain on linux. #1477

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4fa3ba5
Create separate clang build with NDEBUG and CPROVER_INVARIANT_DO_NOT_…
andreast271 Oct 13, 2017
2177bbc
Remove extra build with NDEBUG that compiles but doesn't test.
andreast271 Nov 1, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
11 changes: 7 additions & 4 deletions src/util/invariant.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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, "")
Copy link
Collaborator

@martin-cs martin-cs Nov 21, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Structured Invariant" might be a tad better but ... only if you are editing anyway.


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

Copy link
Contributor Author

@andreast271 andreast271 Oct 27, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having the ellipsis in the macro definition results in a warning, and without defining INVARIANT_STRUCTURED compilation will always fail. How did this ever work?

Copy link
Collaborator

@tautschnig tautschnig Oct 27, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Which warning would that be? It would be surprising that you are the first one to observe it?!

Copy link
Contributor Author

@andreast271 andreast271 Oct 27, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was surprised as well. See the discussion of the first commit.

Copy link
Collaborator

@martin-cs martin-cs Nov 21, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect it didn't. The structured invariant stuff was added after the initial invariant support and it may have simply not been tested. I don't recall reviewing it.

#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);
Expand Down