tests: add tests for copy_from_slice

hacspec · Oct 31, 2023 · 77c7c24 · 77c7c24
1 parent c5f6e56
commit 77c7c24
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 3 deletions.
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
@@ -50,13 +50,31 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
     Rust_primitives.Hax.update_at v
       x
-      (Core.Slice.impl__copy_from_slice (Core.Ops.Index.IndexMut.index_mut v x <: t_Slice u8) a
-        <:
-        t_Slice u8)
+      (Core.Slice.impl__copy_from_slice (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
   in
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.update_at v (sz 1) 3uy in
   ()
 
+let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
+  let x:t_Array u8 (sz 12) =
+    Rust_primitives.Hax.update_at x
+      ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 })
+      (Core.Slice.impl__copy_from_slice (x.[ {
+                Core.Ops.Range.f_start = sz 4;
+                Core.Ops.Range.f_end = sz 5
+              } ]
+            <:
+            t_Slice u8)
+          (Rust_primitives.unsize (let list = [1uy; 2uy] in
+                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+                Rust_primitives.Hax.array_of_list list)
+            <:
+            t_Slice u8)
+        <:
+        t_Slice u8)
+  in
+  42uy
+
 let build_vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   Alloc.Slice.impl__into_vec (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list =
                 [1uy; 2uy; 3uy]

diff --git a/tests/mut-ref-functionalization/src/lib.rs b/tests/mut-ref-functionalization/src/lib.rs
@@ -6,6 +6,11 @@ fn index_mutation(x: core::ops::Range<usize>, a: &'static [u8]) {
     v[1] = 3;
 }
 
+fn index_mutation_unsize(mut x: [u8; 12]) -> u8 {
+    x[4..5].copy_from_slice(&[1, 2]);
+    42
+}
+
 fn build_vec() -> Vec<u8> {
     vec![1, 2, 3]
 }