From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:33:56 +0200 Subject: Add some tests --- .../misc/Issue194RecursiveStructProjector.fst | 24 ++++++++++++++++++++++ tests/fstar/misc/Matches.fst | 12 +++++++++++ 2 files changed, 36 insertions(+) create mode 100644 tests/fstar/misc/Issue194RecursiveStructProjector.fst create mode 100644 tests/fstar/misc/Matches.fst (limited to 'tests/fstar') 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 + -- cgit v1.2.3