Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add regular & fixme tests for function contracts #3371

Merged
merged 10 commits into from
Oct 24, 2024

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Jul 22, 2024

I'm adding a few fix-me tests that I bumped into while working on #3363. Most of them will be fixed by #3363, except the one related to #3370.

The original PR is already quite large, so I decided to just push all of these as fixme tests for now. This is now ready for review!

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@celinval celinval changed the title Test contract support to parameter patterns Add fixme tests for function contracts Jul 26, 2024
@celinval celinval marked this pull request as ready for review July 26, 2024 22:06
@celinval celinval requested a review from a team as a code owner July 26, 2024 22:06
@feliperodri feliperodri added this to the Function Contracts milestone Jul 31, 2024
@tautschnig tautschnig added the Z-Contracts Issue related to code contracts label Aug 1, 2024
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
@carolynzech carolynzech changed the title Add fixme tests for function contracts Add regular & fixme tests for function contracts Oct 21, 2024
charon Outdated Show resolved Hide resolved
tests/kani/FunctionContracts/fixme_receiver_contracts.rs Outdated Show resolved Hide resolved
tests/kani/FunctionContracts/modify_slice_elem.rs Outdated Show resolved Hide resolved
celinval and others added 2 commits October 24, 2024 12:48
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
@celinval celinval added this pull request to the merge queue Oct 24, 2024
Merged via the queue into model-checking:main with commit a8a28ee Oct 24, 2024
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-Contracts Issue related to code contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants