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

modifies Clauses for Function Contracts #2800

Merged
merged 80 commits into from
Feb 2, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
80 commits
Select commit Hold shift + click to select a range
2e6bed3
WIP
JustusAdam Sep 30, 2023
c772a10
Sketch for new modifies clause
JustusAdam Sep 30, 2023
ed2e79d
Add explicit lifetimes to arguments and reorder code
JustusAdam Oct 1, 2023
5a8f746
Sketch for the internal mechanisms
JustusAdam Oct 1, 2023
2759469
Debugging proc-macro code
JustusAdam Oct 2, 2023
9dd55a4
Fixed the assigns bug
JustusAdam Nov 2, 2023
ba27ab6
Using lifetime decoupling for `modifies`
JustusAdam Nov 2, 2023
bbc4e99
Fix lifetime decoupling trait
JustusAdam Nov 3, 2023
00157cb
Make assigns existence optional again
JustusAdam Nov 3, 2023
3db104d
Merge remote-tracking branch 'fork/main' into new-assigns-check
JustusAdam Nov 3, 2023
559cf81
Reviving havoc protection for reentry tracker
JustusAdam Nov 3, 2023
f6d939c
Fixed recursion tracker havocking
JustusAdam Nov 7, 2023
187c56f
Fmt
JustusAdam Nov 11, 2023
54727e2
Cargo fix
JustusAdam Nov 12, 2023
b7c8e63
Fix two test cases + support impl call
JustusAdam Nov 14, 2023
27ebf4f
Fix another test case
JustusAdam Nov 14, 2023
d9e921c
Simple havoc
JustusAdam Nov 14, 2023
ffcdc76
Fixing Formatting and clippy
JustusAdam Nov 19, 2023
b833438
Kani fmt
JustusAdam Nov 19, 2023
64f7e5f
Fix simlpe havoc
JustusAdam Nov 21, 2023
0c3cea7
Fix static exclude for recursion tracker
JustusAdam Nov 22, 2023
4b451cf
Some changes had accidentally been reverted
JustusAdam Nov 22, 2023
0b6ba1e
Formatting
JustusAdam Nov 22, 2023
9362624
Allow pointer transmutes
JustusAdam Nov 22, 2023
7148bac
turns out these need to be refs
JustusAdam Nov 22, 2023
ba4a73e
Gracefully handle if the contract artifact is absent
JustusAdam Nov 22, 2023
9610a9e
Clippy ...
JustusAdam Nov 22, 2023
03ef3ce
Ignoring this error for now
JustusAdam Nov 23, 2023
7b788c7
Changing how contracts communicate
JustusAdam Nov 29, 2023
904ef0e
Merge remote-tracking branch 'fork/main' into new-assigns-check
JustusAdam Nov 29, 2023
981a465
Formatting
JustusAdam Nov 29, 2023
f9b4ef3
Fix Warnings
JustusAdam Nov 29, 2023
12a993d
Consistent use of file paths for recursion tracker
JustusAdam Nov 30, 2023
1843442
Simplify check function editingˆ
JustusAdam Nov 30, 2023
00518b0
Fix ordering for havoc and postconditions
JustusAdam Nov 30, 2023
862a5d7
Extra test cases
JustusAdam Nov 30, 2023
e229ad0
Formatting
JustusAdam Nov 30, 2023
9d95def
Grouping test cases and adding more
JustusAdam Dec 1, 2023
15a596b
Documentation, dead code removal and unique arguments in `modifies`
JustusAdam Dec 1, 2023
af780f1
Test case for unique generated argument names
JustusAdam Dec 1, 2023
e76d0b3
Added missing `expected` files
JustusAdam Dec 1, 2023
907a7f9
Another missing `expected` file
JustusAdam Dec 1, 2023
1c71508
Revert some clippy changes
JustusAdam Dec 1, 2023
e4f3cfd
Remove not strictly necessary dep
JustusAdam Dec 1, 2023
9f3d102
Some basic write-sets documentation
JustusAdam Dec 1, 2023
0573d09
Missing formatting
JustusAdam Dec 1, 2023
384c2f6
Forgot to commit this one
JustusAdam Dec 1, 2023
f7578a8
Typo
JustusAdam Dec 1, 2023
1fffd53
Tinkering with the vector test case.
JustusAdam Dec 4, 2023
34e3a1b
Addressing code review
JustusAdam Dec 14, 2023
f01b619
Apply suggestions from code review
JustusAdam Dec 14, 2023
f283759
Addressing code review leftovers
JustusAdam Dec 14, 2023
6192f3e
Merge remote-tracking branch 'origin/new-assigns-check' into new-assi…
JustusAdam Dec 14, 2023
00bfe6e
Added missing expected file
JustusAdam Dec 14, 2023
9c6b876
Fixed the expected file
JustusAdam Dec 15, 2023
a5dfccd
Added test cases for global variable modifications
JustusAdam Dec 15, 2023
c5b6a2b
Apply suggestions from code review
JustusAdam Dec 23, 2023
6892afc
Suggestions from @feliperodri
JustusAdam Dec 23, 2023
0819432
Merge remote-tracking branch 'origin/new-assigns-check' into new-assi…
JustusAdam Dec 23, 2023
55c5583
Merge remote-tracking branch 'fork/main' into new-assigns-check
JustusAdam Dec 25, 2023
455373c
Update contract code to stable MIR
JustusAdam Dec 26, 2023
68a7f6e
Merge remote-tracking branch 'origin/new-assigns-check' into new-assi…
JustusAdam Dec 26, 2023
0980cbc
Addressing code review comments
JustusAdam Jan 29, 2024
fac45b6
Copyright
JustusAdam Jan 29, 2024
96d4b12
Clippy suggestions
JustusAdam Jan 29, 2024
63d2d7a
Merge remote-tracking branch 'fork/main' into new-assigns-check
JustusAdam Jan 29, 2024
d105b87
Update error reporting
JustusAdam Jan 29, 2024
5eab701
Fixing manes used by contracts metadata
JustusAdam Jan 30, 2024
4bd7583
Fix test case
JustusAdam Jan 30, 2024
0a4503a
Formatting
JustusAdam Jan 31, 2024
6414e22
Clippy complained
JustusAdam Jan 31, 2024
6bbbb24
Whoops
JustusAdam Jan 31, 2024
9b17d94
Name the other Rc test case 'fixme'
JustusAdam Jan 31, 2024
52e703a
Forgot that this now needs formatting
JustusAdam Feb 1, 2024
40e3abe
Used the wrong name
JustusAdam Feb 1, 2024
8db7d20
Merge branch 'main' into new-assigns-check
feliperodri Feb 1, 2024
75a554d
Suggestions from code review
JustusAdam Feb 2, 2024
edd7bf8
Forgot to stage after renaming
JustusAdam Feb 2, 2024
7d08810
Moving all the contract communication logic into the compiler
JustusAdam Feb 2, 2024
1807020
Wrong import
JustusAdam Feb 2, 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
Next Next commit
Missing formatting
  • Loading branch information
JustusAdam committed Dec 1, 2023
commit 0573d09e197d92069433459dea27d1e5d5175a3c
2 changes: 1 addition & 1 deletion library/kani/src/contracts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -225,4 +225,4 @@
//! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T`
//! must implement [`Arbitrary`](super::Arbitrary). This is used to assign
//! `kani::any()` to the location when the function is used in a `stub_verified`.
pub use super::{ensures, proof_for_contract, requires, stub_verified, modifies};
pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified};
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,11 @@ fn two_pointers(a: &mut u32, b: &mut u32) {
*b = 2;
}


#[kani::proof_for_contract(two_pointers)]
fn test_contract() {
two_pointers(&mut kani::any(), &mut kani::any());
}


#[kani::proof]
#[kani::stub_verified(two_pointers)]
fn test_stubbing() {
Expand Down
Loading