Properly converts conditions into assertions and assumptions in function contracts #6049
Conversation
feliperodri
commented
Apr 22, 2021
feliperodri
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
feliperodri
added
bugfix
aws
feliperodri
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
regression/contracts/assigns_enforce_functions_in_contracts/header.h
Outdated
Show resolved
Hide resolved
regression/contracts/assigns_enforce_functions_in_contracts/utility.h
Outdated
Show resolved
Hide resolved
regression/contracts/assigns_enforce_functions_in_contracts/main.c
Outdated
Show resolved
Hide resolved
src/goto-instrument/code_contracts.h
Outdated
| @@ -104,6 +104,12 @@ class code_contractst | |||
| /// \brief Enforce contract of a single function | |||
| bool enforce_contract(const std::string &); | |||
|
|
|||
| /// \brief Create code corresponding to assertion/assumption | |||
There was a problem hiding this comment.
This comment could be reworded for clarity.
- Is it supposed to work only for assertions / assumptions?
- It creates goto instructions (not
codet), so saying "create code" might be confusing.
Meta comment about the approach: the function seems to be creating a goto_convert and just making a single call to it. Can we make this converter a private member of the code_contractst class instead, and just call the converter.goto_convert directly?
There was a problem hiding this comment.
I update the comment as suggested, but I don't see how adding converter as a member of this class would be beneficial here.
There was a problem hiding this comment.
I meant that converter is being initialized with the same 2 arguments:
goto_convertt converter(symbol_table, log.get_message_handler());
so why not make it a private/protected member, initialize it within code_contractst constructor, and directly call converter.goto_convert in place of convert_to_goto?
But we only call it twice anyway, so not a big deal.
Codecov Report
@@ Coverage Diff @@
## develop #6049 +/- ##
===========================================
+ Coverage 74.30% 74.42% +0.11%
===========================================
Files 1444 1444
Lines 157453 157470 +17
===========================================
+ Hits 116995 117195 +200
+ Misses 40458 40275 -183
Continue to review full report at Codecov.
|
feliperodri
force-pushed
the
fix-contracts-asserts-and-assumes
branch
from
d324317 to
7aefc75
Compare
|
@SaswatPadhi thank you for the comments, could you take another look? |
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
New test checks whether CBMC properly verify function contracts with functions. At this point, we still don't check for purity, i.e., if functions in contracts are only predicates. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
feliperodri
force-pushed
the
fix-contracts-asserts-and-assumes
branch
from
7aefc75 to
3363d8c
Compare
