summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorNadrieril2024-05-27 17:33:56 +0200
committerNadrieril2024-05-28 11:36:31 +0200
commitc81c96f20b1dbf428a9ed42e83b910e798e1a225 (patch)
treeb01e01eb4bcec7112399647943047bed3b58cad1 /tests/fstar
parent9cc69020773cc77965a6faa6f0d46f179de3d8b8 (diff)
Add some tests
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/Issue194RecursiveStructProjector.fst24
-rw-r--r--tests/fstar/misc/Matches.fst12
2 files changed, 36 insertions, 0 deletions
diff --git a/tests/fstar/misc/Issue194RecursiveStructProjector.fst b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
new file mode 100644
index 00000000..76368f04
--- /dev/null
+++ b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_194_recursive_struct_projector] *)
+module Issue194RecursiveStructProjector
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [issue_194_recursive_struct_projector::AVLNode]
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *)
+type aVLNode_t (t : Type0) =
+{
+ value : t; left : option (aVLNode_t t); right : option (aVLNode_t t);
+}
+
+(** [issue_194_recursive_struct_projector::get_val]:
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *)
+let get_val (t : Type0) (x : aVLNode_t t) : result t =
+ Ok x.value
+
+(** [issue_194_recursive_struct_projector::get_left]:
+ Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *)
+let get_left (t : Type0) (x : aVLNode_t t) : result (option (aVLNode_t t)) =
+ Ok x.left
+
diff --git a/tests/fstar/misc/Matches.fst b/tests/fstar/misc/Matches.fst
new file mode 100644
index 00000000..06a9b6df
--- /dev/null
+++ b/tests/fstar/misc/Matches.fst
@@ -0,0 +1,12 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [matches] *)
+module Matches
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [matches::match_u32]:
+ Source: 'tests/src/matches.rs', lines 4:0-4:27 *)
+let match_u32 (x : u32) : result u32 =
+ begin match x with | 0 -> Ok 0 | 1 -> Ok 1 | _ -> Ok 2 end
+