summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon HO2023-11-28 08:04:43 +0100
committerGitHub2023-11-28 08:04:43 +0100
commitb78850a81dfea78bc280f1b5b6d2fdcb421e386a (patch)
tree3a4807b26856c0c2e21f1a8a4cdf80da136c26ec /tests/fstar
parentbacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (diff)
parenta3a3ab9723348e24f83073a52145128f34022265 (diff)
Merge pull request #46 from AeneasVerif/son_improves
Minor improvements for the extraction
Diffstat (limited to '')
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst2
-rw-r--r--tests/fstar/betree/BetreeMain.FunsExternal.fsti (renamed from tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti)2
-rw-r--r--tests/fstar/betree/BetreeMain.Types.fst (renamed from tests/fstar/betree_back_stateful/BetreeMain.Types.fsti)4
-rw-r--r--tests/fstar/betree/BetreeMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti (renamed from tests/fstar/betree/BetreeMain.Opaque.fsti)2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Types.fst (renamed from tests/fstar/betree/BetreeMain.Types.fsti)4
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst2
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti)2
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Types.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti)4
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/misc/External.Funs.fst2
-rw-r--r--tests/fstar/misc/External.FunsExternal.fsti (renamed from tests/fstar/misc/External.Opaque.fsti)2
-rw-r--r--tests/fstar/misc/External.Types.fst8
-rw-r--r--tests/fstar/misc/External.TypesExternal.fsti (renamed from tests/fstar/misc/External.Types.fsti)4
-rw-r--r--tests/fstar/traits/Traits.fst10
17 files changed, 53 insertions, 27 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 537ec32e..fef8a8e1 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
module BetreeMain.Funs
open Primitives
include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
include BetreeMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
index b89c8718..cd2f956f 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
+module BetreeMain.FunsExternal
open Primitives
include BetreeMain.Types
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
(** [betree_main]: type definitions *)
module BetreeMain.Types
open Primitives
+include BetreeMain.TypesExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
@@ -58,6 +59,3 @@ type betree_BeTree_t =
root : betree_Node_t;
}
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index a2586431..b912a316 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
module BetreeMain.Funs
open Primitives
include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
include BetreeMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index b89c8718..cd2f956f 100644
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
+module BetreeMain.FunsExternal
open Primitives
include BetreeMain.Types
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
(** [betree_main]: type definitions *)
module BetreeMain.Types
open Primitives
+include BetreeMain.TypesExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
@@ -58,6 +59,3 @@ type betree_BeTree_t =
root : betree_Node_t;
}
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index fa570309..f2d09a38 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -3,7 +3,7 @@
module HashmapMain.Funs
open Primitives
include HashmapMain.Types
-include HashmapMain.Opaque
+include HashmapMain.FunsExternal
include HashmapMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
index 1f47eb33..b00bbcde 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
@@ -1,6 +1,6 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [hashmap_main]: external function declarations *)
-module HashmapMain.Opaque
+module HashmapMain.FunsExternal
open Primitives
include HashmapMain.Types
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
index e77954ad..afebcde3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -2,6 +2,7 @@
(** [hashmap_main]: type definitions *)
module HashmapMain.Types
open Primitives
+include HashmapMain.TypesExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
@@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) =
slots : alloc_vec_Vec (hashmap_List_t t);
}
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
new file mode 100644
index 00000000..75747408
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external type declarations *)
+module HashmapMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 4d13fb71..00995634 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -3,7 +3,7 @@
module External.Funs
open Primitives
include External.Types
-include External.Opaque
+include External.FunsExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index ea1a70c2..923a1101 100644
--- a/tests/fstar/misc/External.Opaque.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -1,6 +1,6 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: external function declarations *)
-module External.Opaque
+module External.FunsExternal
open Primitives
include External.Types
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
new file mode 100644
index 00000000..4fbcec47
--- /dev/null
+++ b/tests/fstar/misc/External.Types.fst
@@ -0,0 +1,8 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+module External.Types
+open Primitives
+include External.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 0cb9fd0e..4bfbe0c5 100644
--- a/tests/fstar/misc/External.Types.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -1,6 +1,6 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
+(** [external]: external type declarations *)
+module External.TypesExternal
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 4cb9fbf1..895a1cac 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -307,15 +307,11 @@ let test_where2
=
Return ()
-(** [alloc::string::String]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *)
-assume type alloc_string_String_t : Type0
-
(** Trait declaration: [traits::ParentTrait0]
Source: 'src/traits.rs', lines 200:0-200:22 *)
noeq type parentTrait0_t (self : Type0) = {
tW : Type0;
- get_name : self -> result alloc_string_String_t;
+ get_name : self -> result string;
get_w : self -> result tW;
}
@@ -333,9 +329,7 @@ noeq type childTrait_t (self : Type0) = {
(** [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 *)
let test_child_trait1
- (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
- result alloc_string_String_t
- =
+ (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
childTraitTInst.parentTrait0SelfInst.get_name x
(** [traits::test_child_trait2]: forward function