summaryrefslogtreecommitdiff
path: root/tests/fstar/array
diff options
context:
space:
mode:
authorSon Ho2023-10-27 12:26:20 +0200
committerSon Ho2023-10-27 12:26:20 +0200
commit67fb76ae5801fdb8f134394425e466dbe611a54b (patch)
tree943235f1771e36fea607636dc09d25c21dab30e8 /tests/fstar/array
parent1c4b1222dbf5e090c26e613694d63577343ab2fd (diff)
Regenerate more F* files
Diffstat (limited to 'tests/fstar/array')
-rw-r--r--tests/fstar/array/Array.Funs.fst4
-rw-r--r--tests/fstar/array/Array.Opaque.fsti24
-rw-r--r--tests/fstar/array/Array.Types.fst2
-rw-r--r--tests/fstar/array/Primitives.fst4
4 files changed, 30 insertions, 4 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst
index a6808c98..8f0bfbbd 100644
--- a/tests/fstar/array/Array.Funs.fst
+++ b/tests/fstar/array/Array.Funs.fst
@@ -277,12 +277,12 @@ let deref_array_mut_borrow_back (x : array u32 2) : result (array u32 2) =
let* _ = array_index_usize u32 2 x 0 in Return x
(** [array::take_array_t]: forward function *)
-let take_array_t (a : array ab_t 2) : result unit =
+let take_array_t (a : array aB_t 2) : result unit =
Return ()
(** [array::non_copyable_array]: forward function *)
let non_copyable_array : result unit =
- let* _ = take_array_t (mk_array ab_t 2 [ ABA; ABB ]) in Return ()
+ let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return ()
(** [array::sum]: loop 0: forward function *)
let rec sum_loop
diff --git a/tests/fstar/array/Array.Opaque.fsti b/tests/fstar/array/Array.Opaque.fsti
new file mode 100644
index 00000000..484cb9ee
--- /dev/null
+++ b/tests/fstar/array/Array.Opaque.fsti
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [array]: external function declarations *)
+module Array.Opaque
+open Primitives
+include Array.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::array::[T; N]::{15}::index]: forward function *)
+val core_array_[T; N]_index_fwd
+ (t i : Type0) (n : usize) (inst : core_ops_index_Index (slice t) i) :
+ array t n -> i -> result inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: forward function *)
+val core_array_[T; N]_index_mut_fwd
+ (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+ array t n -> i -> result inst.index_inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: backward function 0 *)
+val core_array_[T; N]_index_mut_back
+ (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+ array t n -> i -> inst.index_inst.core_ops_index_Index_Output -> result
+ (array t n)
+
diff --git a/tests/fstar/array/Array.Types.fst b/tests/fstar/array/Array.Types.fst
index 0ec9c12f..4e8d5566 100644
--- a/tests/fstar/array/Array.Types.fst
+++ b/tests/fstar/array/Array.Types.fst
@@ -6,5 +6,5 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [array::AB] *)
-type ab_t = | ABA : ab_t | ABB : ab_t
+type aB_t = | AB_A : aB_t | AB_B : aB_t
diff --git a/tests/fstar/array/Primitives.fst b/tests/fstar/array/Primitives.fst
index 3110b247..71d75c11 100644
--- a/tests/fstar/array/Primitives.fst
+++ b/tests/fstar/array/Primitives.fst
@@ -707,5 +707,7 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
Lemma (
alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x ==
- alloc_vec_Vec_update_usize v i x) =
+ alloc_vec_Vec_update_usize v i x)
+ [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)]
+ =
admit()