From 186e97e888cf581373b25e2cc4d9d8dd5ae07b95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Tue, 19 Jul 2022 16:47:54 +0200 Subject: [PATCH] fix --- prusti-specs/src/specifications/preparser.rs | 2 +- prusti-tests/tests/verify/fail/closures/using-type-dep.rs | 2 +- prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs | 3 +++ prusti-tests/tests/verify/pass/closures/using-type-dep.rs | 2 +- 4 files changed, 6 insertions(+), 3 deletions(-) diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index d93aa3e133c..39ce91ddfe7 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -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(), diff --git a/prusti-tests/tests/verify/fail/closures/using-type-dep.rs b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs index 769b411aeca..fe526f7027b 100644 --- a/prusti-tests/tests/verify/fail/closures/using-type-dep.rs +++ b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs @@ -1,4 +1,4 @@ -// compiler-flags: -Penable_ghost_constraints=true +// compile-flags: -Penable_ghost_constraints=true #![feature(unboxed_closures, fn_traits)] diff --git a/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs b/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs index 6830f318cf3..f79ea4f8f0b 100644 --- a/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs +++ b/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs @@ -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: A, b: A, key: impl Fn(&A) -> B) -> A { if key(&a) > key(&b) { //~ Error: only calls to closures are supported a diff --git a/prusti-tests/tests/verify/pass/closures/using-type-dep.rs b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs index b58e6a72519..37096357de2 100644 --- a/prusti-tests/tests/verify/pass/closures/using-type-dep.rs +++ b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs @@ -1,4 +1,4 @@ -// compiler-flags: -Penable_ghost_constraints=true +// compile-flags: -Penable_ghost_constraints=true #![feature(unboxed_closures, fn_traits)]