From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 15:47:20 +0200
Subject: runner: Pass options in special comments

---
 tests/src/hashmap.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests/src/hashmap.rs')

diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 58d22acd..4552e4f2 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,3 +1,11 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ aeneas-args=-split-files
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [lean] aeneas-args=-no-gen-lib-entry
+// ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not
+// want to overwrite it.
+// TODO: reactivate -test-trans-units
+
 //! A hashmap implementation.
 //!
 //! Current limitations:
-- 
cgit v1.2.3


From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:59:10 +0200
Subject: tests: Merge the hashmap test files

---
 tests/src/hashmap.rs | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

(limited to 'tests/src/hashmap.rs')

diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 4552e4f2..ccb96e1e 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,9 +1,11 @@
+//@ charon-args=--opaque=hashmap_utils
+//@ aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
-//@ aeneas-args=-split-files
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
 // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not
 // want to overwrite it.
+// Possible to add `--no-code-duplication` if we use the optimized MIR
 // TODO: reactivate -test-trans-units
 
 //! A hashmap implementation.
@@ -314,6 +316,31 @@ impl<T> HashMap<T> {
     }
 }
 
+// This is a module so we can tell charon to leave it opaque
+mod hashmap_utils {
+    use crate::*;
+
+    /// Serialize a hash map - we don't have traits, so we fix the type of the
+    /// values (this is not the interesting part anyway)
+    pub(crate) fn serialize(_hm: HashMap<u64>) {
+        unimplemented!();
+    }
+    /// Deserialize a hash map - we don't have traits, so we fix the type of the
+    /// values (this is not the interesting part anyway)
+    pub(crate) fn deserialize() -> HashMap<u64> {
+        unimplemented!();
+    }
+}
+
+pub fn insert_on_disk(key: Key, value: u64) {
+    // Deserialize
+    let mut hm = hashmap_utils::deserialize();
+    // Update
+    hm.insert(key, value);
+    // Serialize
+    hashmap_utils::serialize(hm);
+}
+
 /// I currently can't retrieve functions marked with the attribute #[test],
 /// while I want to extract the unit tests and use the normalize on them,
 /// so I have to define the test functions somewhere and call them from
-- 
cgit v1.2.3


From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 11:18:35 +0200
Subject: tests: Rename hashmap_utils -> utils

---
 tests/src/hashmap.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/src/hashmap.rs')

diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index ccb96e1e..19832a84 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,4 +1,4 @@
-//@ charon-args=--opaque=hashmap_utils
+//@ charon-args=--opaque=utils
 //@ aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
@@ -317,7 +317,7 @@ impl<T> HashMap<T> {
 }
 
 // This is a module so we can tell charon to leave it opaque
-mod hashmap_utils {
+mod utils {
     use crate::*;
 
     /// Serialize a hash map - we don't have traits, so we fix the type of the
@@ -334,11 +334,11 @@ mod hashmap_utils {
 
 pub fn insert_on_disk(key: Key, value: u64) {
     // Deserialize
-    let mut hm = hashmap_utils::deserialize();
+    let mut hm = utils::deserialize();
     // Update
     hm.insert(key, value);
     // Serialize
-    hashmap_utils::serialize(hm);
+    utils::serialize(hm);
 }
 
 /// I currently can't retrieve functions marked with the attribute #[test],
-- 
cgit v1.2.3