Use goto-analyzer to add assumptions, assertions and code contracts #7964
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
martin-cs
requested review from
peterschrammel,
jimgrundy,
TGWDB,
kroening,
tautschnig and
NlightNFotis
as code owners
martin-cs
force-pushed
the
feature/goto-analyzer-instrument-task
branch
from
6e78afd to
1d4a86e
Compare
| /// Gives a Boolean condition that is true for all values represented by the | ||
| /// domain. This allows domains to be converted into program invariants. | ||
| virtual exprt to_predicate(void) const | ||
| /// Gives a Boolean condition involving expression from the set that |
There was a problem hiding this comment.
Gives a Boolean condition involving expressions from the given set that... ?
| exprt target = value_stack.to_expression(); | ||
|
|
||
| // This is simple if there are no restrictions: | ||
| if(scope.size() == 0) |
| #include <iosfwd> | ||
|
|
||
| // What kind of instrumentation to add | ||
| enum class instrument_actiont |
There was a problem hiding this comment.
❓ Maybe this should (eventually also) consider the contracts work that @remi-delmas-3000 et al are doing? Or at least it should be considered to avoid that the design is unnecessarily incompatible with it (I doubt it is, but might be worth checking).
There was a problem hiding this comment.
We are in contact and the goal is to fit with and support @remi-delmas-3000 's work. Thanks for the link though, if I didn't know about what he was doing it would be very important to find out!
An abstract domain may contain information about variables from a calling context which are not valid in an assertion in a different function. This commit changes the interface to give a limiting scope. This is particularly fiddly in the case of pointers to things that are out of scope.
martin-cs
force-pushed
the
feature/goto-analyzer-instrument-task
branch
from
1d4a86e to
c0dc3a6
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a work-in-progress PR posted for general feedback and early opinions. It adds a new 'task' to goto-analyzer which runs the abstract interpreter, converts the domains to predicates and then adds them into the goto program as assumptions, assertions or as contracts. Assumptions are intended to aid other analysis tools which can use (but not necessarily create) inductive invariants. Assertions are intended to give a way to cross-test the abstract interpreter using CBMC. Contracts are intended to give better default contracts for code that does not have them and to help users in writing the obvious but tedious parts.
Things that still need some work:
__CPROVER_returnin the contracts.truewhich is correct and over-approximate but not very helpful. It is not immediately clear what the "right" approach is.assignscontracts are not generated yet as they need additional support for domain difference.