test(hax-lib/macros): handle correctly &mut Self arguments in `ensu…

…res`
cryspen · Jan 22, 2025 · e384b95 · e384b95
1 parent 6ef83cf
commit e384b95
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 5 deletions.
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -114,6 +114,18 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
 
 unfold let add x y = x + y
 '''
+"Attributes.Issue_1266_.fst" = '''
+module Attributes.Issue_1266_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_T (v_Self: Type0) = {
+  f_v_pre:v_Self -> Type0;
+  f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true};
+  f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
+}
+'''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

diff --git a/tests/Cargo.lock b/tests/Cargo.lock
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
@@ -381,3 +381,11 @@ mod requires_mut {
         }
     }
 }
+
+mod issue_1266 {
+    #[hax_lib::attributes]
+    trait T {
+        #[hax_lib::ensures(|_|true)]
+        fn v(x: &mut Self);
+    }
+}