Skip to content

WIP: Iterator tracking issues #980

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

Open
wants to merge 45 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
4caee3a
Adjust copy check in environment to better handle regions
vl0w Apr 26, 2022
ed7dffd
Maybe we need to handle TyKind::Ref differently?
vl0w Apr 26, 2022
03b3640
Support associated types in copy check
vl0w Apr 27, 2022
138d98e
Pass type with binder to type_is_copy to better account for regions
vl0w Apr 27, 2022
a408861
Normalize function signature in PureFunctionEncoder to account for as…
vl0w Apr 28, 2022
dbbed0d
Remove check for validity of pure function in process_encoding_queue
vl0w Apr 28, 2022
161b956
Erase all regions in copy check
vl0w Apr 28, 2022
eda1445
Do not perform normalization when there are no projections
vl0w Apr 28, 2022
41aad37
Partially undo removal of code in process_encoding_queue.
vl0w Apr 28, 2022
e2a5467
Rename normalize_to, return original value if normalized value contai…
vl0w Apr 28, 2022
43a5387
Pass ParamEnv to resolve_assoc_types, make it fallible
vl0w Apr 29, 2022
b604cd4
Small cleanups
vl0w Apr 29, 2022
5dc9705
Add custom iterator tests
vl0w Apr 20, 2022
f8f2859
Add flag to add experimental iterator support
vl0w Apr 21, 2022
0da3287
Move predicate normalization in constraint solver for better debugging
vl0w Apr 27, 2022
c1cbead
Do not copy preconditions of base spec to constrained spec
vl0w Apr 27, 2022
59bc78c
Use predicate_must_hold_modulo_regions when resolving ghost constrain…
vl0w Apr 29, 2022
0af45d7
Handle lifetimes in merge_generics
vl0w Apr 29, 2022
c527dc1
Support lifetimes in type models
vl0w May 2, 2022
c8081fb
Relax needs_infer check in Environment::resolve_method_call to ignore…
vl0w May 2, 2022
78c51fb
Merge branch 'master' into iterators-feature-flag
vl0w May 2, 2022
af55da2
Support lifetimes in type models
vl0w May 3, 2022
8c7a2ab
Add first tests
vl0w May 3, 2022
fa1c14a
Verification of Iter in while loop
vl0w May 4, 2022
5e396ff
Create custom Copy/Clone impls for type models (do not derive them)
vl0w May 4, 2022
3afba7c
Adjust flag docs for iterator killswitch
vl0w May 4, 2022
70e5b0f
Normalize substs in Environment::resolve_method_call to account for n…
vl0w May 6, 2022
ed1a7a5
Fix typo
vl0w May 8, 2022
d1d4953
Support associated types in quantifiers
vl0w May 9, 2022
7e7bde4
Remove dead comment in any_type_needs_infer
vl0w May 9, 2022
e3bbbd9
Remove dead code
vl0w May 11, 2022
8e05591
Merge branch 'master' into iterators-feature-flag
vl0w May 23, 2022
116bcd6
Merge branch 'master' into iterators-feature-flag
vl0w May 30, 2022
f16f646
fix for #1033 with test cases
Pointerbender Jun 7, 2022
96ee8b9
snapshot equality
Aurel300 Jul 12, 2022
414e081
remove special Fn*::call* treatment
Aurel300 Jul 18, 2022
2b6d632
test closures using type-dependent contracts
Aurel300 Jul 18, 2022
9142078
Merge remote-tracking branch 'upstream/master' into iterators-feature…
Aurel300 Jul 19, 2022
186e97e
fix
Aurel300 Jul 19, 2022
8ed4eb2
Merge remote-tracking branch 'upstream/master' into iterators-feature…
Aurel300 Jul 22, 2022
dbd4d2d
erase regions less eagerly for method calls
Aurel300 Jul 22, 2022
1eaa7d0
Merge remote-tracking branch 'upstream/master' into iterators-feature…
Aurel300 Jul 27, 2022
c74215b
fix
Aurel300 Jul 27, 2022
e9e5c78
Merge remote-tracking branch 'upstream/master' into iterators-feature…
Aurel300 Jul 29, 2022
fa449f9
another unsafe core proof workaround for trait resolution
Aurel300 Jul 29, 2022
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
fix
Aurel300 committed Jul 20, 2022
commit 186e97e888cf581373b25e2cc4d9d8dd5ae07b95
2 changes: 1 addition & 1 deletion prusti-specs/src/specifications/preparser.rs
Original file line number Diff line number Diff line change
@@ -899,7 +899,7 @@ mod tests {
);
assert_eq!(
parse_prusti(quote! { exists(|x: i32| a === b) }).unwrap().to_string(),
"exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (a , b)) : bool) })",
"exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (& a , & b)) : bool) })",
);
assert_eq!(
parse_prusti(quote! { forall(|x: i32| a ==> b, triggers = [(c,), (d, e)]) }).unwrap().to_string(),
2 changes: 1 addition & 1 deletion prusti-tests/tests/verify/fail/closures/using-type-dep.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compiler-flags: -Penable_ghost_constraints=true
// compile-flags: -Penable_ghost_constraints=true

#![feature(unboxed_closures, fn_traits)]

Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
// ignore-test The function arguments (desugared to a 1-tuple of reference
// here) are probably the issue; then this is similar to #1077 ?

pub fn max_by_key<A, B: Ord>(a: A, b: A, key: impl Fn(&A) -> B) -> A {
if key(&a) > key(&b) { //~ Error: only calls to closures are supported
a
2 changes: 1 addition & 1 deletion prusti-tests/tests/verify/pass/closures/using-type-dep.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compiler-flags: -Penable_ghost_constraints=true
// compile-flags: -Penable_ghost_constraints=true

#![feature(unboxed_closures, fn_traits)]