Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

1 files changed, 25 insertions, 0 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
new file mode 100644
index 00000000..a03dc407
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
@@ -0,0 +1,25 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external function declarations *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_FunsExternal.
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_FunsExternal.