From 4f824528f5e0c0f898b20917c6c06821efb934da Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 27 Oct 2023 12:12:18 +0200 Subject: Regenerate some of the F* test files --- tests/fstar/misc/External.Opaque.fsti | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tests/fstar/misc/External.Opaque.fsti') diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti index 2e19f767..85cf285c 100644 --- a/tests/fstar/misc/External.Opaque.fsti +++ b/tests/fstar/misc/External.Opaque.fsti @@ -7,7 +7,7 @@ include External.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [core::mem::swap]: forward function *) -val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit) +val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit) (** [core::mem::swap]: backward function 0 *) val core_mem_swap_back0 @@ -18,10 +18,10 @@ val core_mem_swap_back1 (t : Type0) : t -> t -> state -> state -> result (state & t) (** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *) -val core_num_nonzero_non_zero_u32_new_fwd - : u32 -> state -> result (state & (option core_num_nonzero_non_zero_u32_t)) +val core_num_nonzero_NonZeroU32_new + : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t)) (** [core::option::Option::{0}::unwrap]: forward function *) -val core_option_option_unwrap_fwd +val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) -- cgit v1.2.3 From 5e92ae6b361f9221f5c5f9a39ab4c28a36597a77 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 11:40:59 +0100 Subject: Regenerate most of the test files --- tests/fstar/misc/External.Opaque.fsti | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests/fstar/misc/External.Opaque.fsti') diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti index 85cf285c..3914a8eb 100644 --- a/tests/fstar/misc/External.Opaque.fsti +++ b/tests/fstar/misc/External.Opaque.fsti @@ -17,11 +17,11 @@ val core_mem_swap_back0 val core_mem_swap_back1 (t : Type0) : t -> t -> state -> state -> result (state & t) -(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *) +(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function *) val core_num_nonzero_NonZeroU32_new : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t)) -(** [core::option::Option::{0}::unwrap]: forward function *) +(** [core::option::{core::option::Option}::unwrap]: forward function *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) -- cgit v1.2.3 From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:57:38 +0100 Subject: Regenerate the files --- tests/fstar/misc/External.Opaque.fsti | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'tests/fstar/misc/External.Opaque.fsti') diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti index 3914a8eb..ea1a70c2 100644 --- a/tests/fstar/misc/External.Opaque.fsti +++ b/tests/fstar/misc/External.Opaque.fsti @@ -6,22 +6,27 @@ include External.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [core::mem::swap]: forward function *) +(** [core::mem::swap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit) -(** [core::mem::swap]: backward function 0 *) +(** [core::mem::swap]: backward function 0 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) val core_mem_swap_back0 (t : Type0) : t -> t -> state -> state -> result (state & t) -(** [core::mem::swap]: backward function 1 *) +(** [core::mem::swap]: backward function 1 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) val core_mem_swap_back1 (t : Type0) : t -> t -> state -> state -> result (state & t) -(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function *) +(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) val core_num_nonzero_NonZeroU32_new : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t)) -(** [core::option::{core::option::Option}::unwrap]: forward function *) +(** [core::option::{core::option::Option}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) -- cgit v1.2.3 From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 09:37:31 +0100 Subject: Update the generation of files for external definitions and regenerate the tests --- tests/fstar/misc/External.Opaque.fsti | 32 -------------------------------- 1 file changed, 32 deletions(-) delete mode 100644 tests/fstar/misc/External.Opaque.fsti (limited to 'tests/fstar/misc/External.Opaque.fsti') diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti deleted file mode 100644 index ea1a70c2..00000000 --- a/tests/fstar/misc/External.Opaque.fsti +++ /dev/null @@ -1,32 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: external function declarations *) -module External.Opaque -open Primitives -include External.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [core::mem::swap]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) -val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit) - -(** [core::mem::swap]: backward function 0 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) -val core_mem_swap_back0 - (t : Type0) : t -> t -> state -> state -> result (state & t) - -(** [core::mem::swap]: backward function 1 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) -val core_mem_swap_back1 - (t : Type0) : t -> t -> state -> state -> result (state & t) - -(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) -val core_num_nonzero_NonZeroU32_new - : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t)) - -(** [core::option::{core::option::Option}::unwrap]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) -val core_option_Option_unwrap - (t : Type0) : option t -> state -> result (state & t) - -- cgit v1.2.3