Restructure function contracts for readability #142
Merged
Conversation
This file contains hidden or 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
feliperodri
force-pushed
the
update-function-contracts
branch
5 times, most recently
from
84193c9 to
a95faa6
Compare
feliperodri
force-pushed
the
update-function-contracts
branch
2 times, most recently
from
4660d67 to
8b92dc5
Compare
feliperodri
force-pushed
the
update-function-contracts
branch
4 times, most recently
from
2857b79 to
d859f3b
Compare
remi-delmas-3000
suggested changes
Apr 14, 2023
feliperodri
force-pushed
the
update-function-contracts
branch
from
d859f3b to
2e5b790
Compare
feliperodri
force-pushed
the
update-function-contracts
branch
2 times, most recently
from
0225979 to
913afaf
Compare
|
I am trying to verify this PR. The proofs that include cadical are complaining of a command not found. What should be the new CBMC instructions for adding cadical? |
n9wxu
previously approved these changes
Apr 28, 2023
archigup
previously approved these changes
May 1, 2023
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
feliperodri
force-pushed
the
update-function-contracts
branch
from
4966ad0 to
cf8ed2a
Compare
remi-delmas-3000
approved these changes
May 4, 2023
Contributor
Author
archigup
approved these changes
May 8, 2023
n9wxu
approved these changes
May 9, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
Description
Restructure function contracts for readability.
Test Steps
All CBMC harnesses should continue to pass. No fundamental changes are being applied.
Checklist:
Related Issue
None.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.