No-assertions should not affect assertions in built-ins #681
Conversation
|
Is there then any way at all to disable the built-in checks? |
|
Currently not. Shall we distinguish between no-assertions at all and no-user-assertions? |
|
On Thu, 2017-03-23 at 01:50 -0700, Peter Schrammel wrote:
Shall we distinguish between no-assertions at all and no-user-assertions?
I can see a possible use for this in other languages which have some
assertions added as part of the semantics, but, on the other hand, I can
see that this could lead to a proliferation of flags. What is the
original need / use case for this?
|
|
It's a customer request who wants to disable his own assertions while keeping the checks in built-ins (Eg memory checks in free()). |
|
I believe a user's assertions can be disabled by compiling/running with -DNDEBUG. So maybe more fine-grained control to permit disabled built-in assertions is required. |
|
Overall, the first two commits are great, the third one seems debatable. |
|
The third commit was the actual reason for the PR ;) The current description of the option --no-assertion says "ignore user assertions", which is confusing because it also disables built-in assertions. A user cannot really understand the difference between an instrumented assertion and a built-in assertion. The user only understands what her own assertions are and then sees assertions being added by CBMC. Suggestion:
More fine-grained control over the latter can be introduced if requested. |
This commit changes the behahaviour of --no-assertions so that only user assertions are ignored. Built-in assertions can be hidden by the new option --no-built-in-assertions.
peterschrammel
force-pushed
the
no-assertions-for-user-only
branch
from
9dee64e to
85a7566
Compare
|
@tautschnig, this is green now. |
This PR includes a clean-up of various checks whether something is a built-in.