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.

Sign up for GitHub

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
Merged

Add regular & fixme tests for function contracts #3371

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
9813172
Test contract support to parameter patterns
celinval Jul 22, 2024
aac359f
Add fixme tests for contracts for different issues
celinval Jul 26, 2024
01fa123
Merge branch 'main' into issue-3206-tests
celinval Jul 26, 2024
eaf3c68
Merge branch 'main' into issue-3206-tests
feliperodri Aug 2, 2024
ea91888
Apply suggestions from code review
celinval Aug 13, 2024
2fd0fe4
update tests
carolynzech Oct 21, 2024
62f2855
remove charon submodule
carolynzech Oct 21, 2024
f742cd2
remove test copy
carolynzech Oct 21, 2024
d231bcc
Merge branch 'main' into issue-3206-tests
celinval Oct 24, 2024
44b282d
Apply suggestions from code review
celinval Oct 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Apply suggestions from code review 
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
  • Loading branch information
@celinval @zhassan-aws
celinval and zhassan-aws authored Oct 24, 2024
commit 44b282dd374125bf3fc36fc03cd6b2a1364a9f2e
1 change: 0 additions & 1 deletion tests/kani/FunctionContracts/fixme_receiver_contracts.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,6 @@ mod verify {
#[kani::proof_for_contract(CharASCII::set_mut_ref)]
fn check_mut_ref() {
let mut obj = CharASCII::any();
let original = obj.0;
let new_val: u8 = kani::any();
unsafe { obj.set_mut_ref(new_val) };
}
Expand Down
2 changes: 1 addition & 1 deletion tests/kani/FunctionContracts/modify_slice_elem.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Check that Kani correctly verify the contract that modifies slices.
//! Check that Kani correctly verifies the contract that modifies slices.
//!
//! Note that this test used to crash while parsing the annotations.
// kani-flags: -Zfunction-contracts
Expand Down
Loading