Collections: Add contract usage #2796
Open
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
Delja
force-pushed
the
collections_contract
branch
from
e45d35b to
a117432
Compare
Delja
force-pushed
the
collections_contract
branch
2 times, most recently
from
4b30899 to
ada9853
Compare
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Delja
force-pushed
the
collections_contract
branch
from
ada9853 to
244dd06
Compare
Delja
force-pushed
the
collections_contract
branch
from
6267159 to
29c4b26
Compare
Delja
force-pushed
the
collections_contract
branch
from
29c4b26 to
530b9aa
Compare
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Deactivation of contracts on the collection wrapper. Contracts on real_collection are always applied. Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Delja
force-pushed
the
collections_contract
branch
from
530b9aa to
2c3d586
Compare
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Improve comment to be more explicit of the purpose of `mcontract_facet` Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Improve comment to be more explicit of the purpose of `mcontract_facet` Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Move the contract options in the appropriate module contract Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Update man page to add `--in-out-invariant` option Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Added a parameter to provide the type of receiver rather than using the intro type of the property Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
replace the parameter to take care of the invariant Signed-off-by: Delja <deljarry.florian@gmail.com>
Add --all-ensure, --all-expect, --all-invariant, --true-contract Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Signed-off-by: Delja <deljarry.florian@gmail.com>
Delja
force-pushed
the
collections_contract
branch
from
43f4e57 to
c15a931
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 pr add contract usage in lib/core/collection. All assert that was used as a pre-post condition are replaced by contracts expects ensures.