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/arrays.rs            | 3 +++
 tests/src/bitwise.rs           | 1 +
 tests/src/constants.rs         | 2 ++
 tests/src/demo.rs              | 1 +
 tests/src/external.rs          | 3 +++
 tests/src/hashmap.rs           | 8 ++++++++
 tests/src/hashmap_main.rs      | 6 ++++++
 tests/src/hashmap_utils.rs     | 1 +
 tests/src/loops.rs             | 3 +++
 tests/src/nested_borrows.rs    | 2 ++
 tests/src/no_nested_borrows.rs | 2 ++
 tests/src/paper.rs             | 2 ++
 tests/src/polonius_list.rs     | 2 ++
 tests/src/traits.rs            | 1 +
 14 files changed, 37 insertions(+)

(limited to 'tests/src')

diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs
index 1f094541..ddad2ad3 100644
--- a/tests/src/arrays.rs
+++ b/tests/src/arrays.rs
@@ -1,3 +1,6 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-split-files
 //! Exercise the translation of arrays, with features supported by Eurydice
 
 pub enum AB {
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 9f48cb04..15962047 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,3 +1,4 @@
+//@ aeneas-args=-test-trans-units
 //! Exercise the bitwise operations
 
 pub fn shift_u32(a: u32) -> u32 {
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index 83904eed..925c62b1 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! Tests with constants
 
 // Integers
diff --git a/tests/src/demo.rs b/tests/src/demo.rs
index bc74cc8b..b9bb7ca2 100644
--- a/tests/src/demo.rs
+++ b/tests/src/demo.rs
@@ -1,3 +1,4 @@
+//@ [coq,fstar] aeneas-args=-use-fuel
 #![allow(clippy::needless_lifetimes)]
 
 /* Simple functions */
diff --git a/tests/src/external.rs b/tests/src/external.rs
index 521749d6..ddd5539f 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,3 +1,6 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-state -split-files
+//@ aeneas-args=-test-trans-units
 //! This module uses external types and functions
 
 use std::cell::Cell;
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:
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
index 45dfa6e2..0c827844 100644
--- a/tests/src/hashmap_main.rs
+++ b/tests/src/hashmap_main.rs
@@ -1,3 +1,9 @@
+//@ charon-args=--opaque=hashmap_utils
+//@ aeneas-args=-state -split-files
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+// Possible to add `--no-code-duplication` if we use the optimized MIR
+// TODO: reactivate -test-trans-units
 mod hashmap;
 mod hashmap_utils;
 
diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs
index cd7b481f..33de49e1 100644
--- a/tests/src/hashmap_utils.rs
+++ b/tests/src/hashmap_utils.rs
@@ -1,3 +1,4 @@
+//@ skip
 use crate::hashmap::*;
 
 /// Serialize a hash map - we don't have traits, so we fix the type of the
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
index 2f71d75b..8692c60e 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,3 +1,6 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-split-files
 use std::vec::Vec;
 
 /// No borrows
diff --git a/tests/src/nested_borrows.rs b/tests/src/nested_borrows.rs
index 94db0cec..d4d8cf73 100644
--- a/tests/src/nested_borrows.rs
+++ b/tests/src/nested_borrows.rs
@@ -1,3 +1,5 @@
+//@ skip
+//@ charon-args=--no-code-duplication
 //! This module contains functions with nested borrows in their signatures.
 
 pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T {
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 9a7604e6..78163371 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
 
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 156f13ab..07453098 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! The examples from the ICFP submission, all in one place.
 
 // 2.1
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index 8c64110d..a8d51e40 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--polonius
+//@ aeneas-args=-test-trans-units
 #![allow(dead_code)]
 
 pub enum List<T> {
diff --git a/tests/src/traits.rs b/tests/src/traits.rs
index 27c90586..fd50db8c 100644
--- a/tests/src/traits.rs
+++ b/tests/src/traits.rs
@@ -1,3 +1,4 @@
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 pub trait BoolTrait {
     // Required method
     fn get_bool(&self) -> bool;
-- 
cgit v1.2.3


From 093ebced6d22f6b805147783c978af13a7a03caa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:51:54 +0200
Subject: runner: Specify subdirectory in magic comments

---
 tests/src/bitwise.rs           | 1 +
 tests/src/constants.rs         | 1 +
 tests/src/demo.rs              | 1 +
 tests/src/external.rs          | 1 +
 tests/src/loops.rs             | 1 +
 tests/src/no_nested_borrows.rs | 1 +
 tests/src/paper.rs             | 1 +
 tests/src/polonius_list.rs     | 1 +
 8 files changed, 8 insertions(+)

(limited to 'tests/src')

diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 15962047..fda8eff3 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,4 +1,5 @@
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! Exercise the bitwise operations
 
 pub fn shift_u32(a: u32) -> u32 {
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index 925c62b1..ac24dcd4 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! Tests with constants
 
 // Integers
diff --git a/tests/src/demo.rs b/tests/src/demo.rs
index b9bb7ca2..0a589338 100644
--- a/tests/src/demo.rs
+++ b/tests/src/demo.rs
@@ -1,4 +1,5 @@
 //@ [coq,fstar] aeneas-args=-use-fuel
+//@ [lean] subdir=Demo
 #![allow(clippy::needless_lifetimes)]
 
 /* Simple functions */
diff --git a/tests/src/external.rs b/tests/src/external.rs
index ddd5539f..baea76e4 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,6 +1,7 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-state -split-files
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! This module uses external types and functions
 
 use std::cell::Cell;
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
index 8692c60e..afc52ace 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,6 +1,7 @@
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [fstar] aeneas-args=-split-files
+//@ [coq,fstar] subdir=misc
 use std::vec::Vec;
 
 /// No borrows
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 78163371..a250748c 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
 
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 07453098..6a4a7c31 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! The examples from the ICFP submission, all in one place.
 
 // 2.1
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index a8d51e40..b029ad02 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--polonius
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
 pub enum List<T> {
-- 
cgit v1.2.3


From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 11:22:37 +0200
Subject: runner: Support negative tests

---
 tests/src/mutually-recursive-traits.lean.out | 17 +++++++++++++++++
 tests/src/mutually-recursive-traits.rs       | 11 +++++++++++
 tests/src/string-chars.lean.out              | 21 +++++++++++++++++++++
 tests/src/string-chars.rs                    |  6 ++++++
 4 files changed, 55 insertions(+)
 create mode 100644 tests/src/mutually-recursive-traits.lean.out
 create mode 100644 tests/src/mutually-recursive-traits.rs
 create mode 100644 tests/src/string-chars.lean.out
 create mode 100644 tests/src/string-chars.rs

(limited to 'tests/src')

diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
new file mode 100644
index 00000000..33206fe5
--- /dev/null
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -0,0 +1,17 @@
+[Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
+[Error] In file Translate.ml, line 813:
+Mutually recursive trait declarations are not supported
+
+Uncaught exception:
+  
+  (Failure
+    "In file Translate.ml, line 813:\
+   \nIn file Translate.ml, line 813:\
+   \nMutually recursive trait declarations are not supported")
+
+Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
+Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1502, characters 5-42
+Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs
new file mode 100644
index 00000000..351763b2
--- /dev/null
+++ b/tests/src/mutually-recursive-traits.rs
@@ -0,0 +1,11 @@
+//@ [lean] known-failure
+//@ [coq,fstar] skip
+//@ subdir=misc
+pub trait Trait1 {
+    type T: Trait2;
+}
+
+pub trait Trait2: Trait1 {}
+
+pub trait T1<T: T2<Self>>: Sized {}
+pub trait T2<T: T1<Self>>: Sized {}
diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out
new file mode 100644
index 00000000..0d28744f
--- /dev/null
+++ b/tests/src/string-chars.lean.out
@@ -0,0 +1,21 @@
+[Info ] Imported: tests/llbc/string_chars.llbc
+[Error] In file SymbolicToPure.ml, line 588:
+ADTs containing borrows are not supported yet
+Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20
+
+Uncaught exception:
+  
+  (Failure
+    "In file SymbolicToPure.ml, line 588:\
+   \nIn file SymbolicToPure.ml, line 588:\
+   \nADTs containing borrows are not supported yet\
+   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\
+   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20")
+
+Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
+Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113
+Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42
+Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
+Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33
+Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
new file mode 100644
index 00000000..5ba9a2d6
--- /dev/null
+++ b/tests/src/string-chars.rs
@@ -0,0 +1,6 @@
+//@ [lean] known-failure
+//@ [coq,fstar] skip
+fn main() {
+    let s = "hello";
+    let _chs: Vec<char> = s.chars().collect();
+}
-- 
cgit v1.2.3


From fb16d0af4caacd2c9a3463f6d2b455209b755697 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:34:12 +0200
Subject: runner: Add `no-check-output` option for unstable outputs

---
 tests/src/string-chars.lean.out | 21 ---------------------
 tests/src/string-chars.rs       |  1 +
 2 files changed, 1 insertion(+), 21 deletions(-)
 delete mode 100644 tests/src/string-chars.lean.out

(limited to 'tests/src')

diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out
deleted file mode 100644
index 0d28744f..00000000
--- a/tests/src/string-chars.lean.out
+++ /dev/null
@@ -1,21 +0,0 @@
-[Info ] Imported: tests/llbc/string_chars.llbc
-[Error] In file SymbolicToPure.ml, line 588:
-ADTs containing borrows are not supported yet
-Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20
-
-Uncaught exception:
-  
-  (Failure
-    "In file SymbolicToPure.ml, line 588:\
-   \nIn file SymbolicToPure.ml, line 588:\
-   \nADTs containing borrows are not supported yet\
-   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\
-   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20")
-
-Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
-Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113
-Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42
-Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
-Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33
-Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
index 5ba9a2d6..f8490e76 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,6 @@
 //@ [lean] known-failure
 //@ [coq,fstar] skip
+//@ no-check-output
 fn main() {
     let s = "hello";
     let _chs: Vec<char> = s.chars().collect();
-- 
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 ++++++++++++++++++++++++++++-
 tests/src/hashmap_main.rs  | 22 ----------------------
 tests/src/hashmap_utils.rs | 13 -------------
 3 files changed, 28 insertions(+), 36 deletions(-)
 delete mode 100644 tests/src/hashmap_main.rs
 delete mode 100644 tests/src/hashmap_utils.rs

(limited to 'tests/src')

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
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
deleted file mode 100644
index 0c827844..00000000
--- a/tests/src/hashmap_main.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-//@ charon-args=--opaque=hashmap_utils
-//@ aeneas-args=-state -split-files
-//@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
-// Possible to add `--no-code-duplication` if we use the optimized MIR
-// TODO: reactivate -test-trans-units
-mod hashmap;
-mod hashmap_utils;
-
-use crate::hashmap::*;
-use crate::hashmap_utils::*;
-
-pub fn insert_on_disk(key: Key, value: u64) {
-    // Deserialize
-    let mut hm = deserialize();
-    // Update
-    hm.insert(key, value);
-    // Serialize
-    serialize(hm);
-}
-
-pub fn main() {}
diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs
deleted file mode 100644
index 33de49e1..00000000
--- a/tests/src/hashmap_utils.rs
+++ /dev/null
@@ -1,13 +0,0 @@
-//@ skip
-use crate::hashmap::*;
-
-/// 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!();
-}
-- 
cgit v1.2.3


From 9cc69020773cc77965a6faa6f0d46f179de3d8b8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:22:07 +0200
Subject: runner: Store options for crate tests in a separate file

---
 tests/src/betree/aeneas-test-options | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 tests/src/betree/aeneas-test-options

(limited to 'tests/src')

diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
new file mode 100644
index 00000000..c71e01df
--- /dev/null
+++ b/tests/src/betree/aeneas-test-options
@@ -0,0 +1,4 @@
+charon-args=--polonius --opaque=betree_utils
+aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[coq] aeneas-args=-use-fuel
+[fstar] aeneas-args=-decreases-clauses -template-clauses
-- 
cgit v1.2.3


From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:33:56 +0200
Subject: Add some tests

---
 tests/src/infinite-loop.rs                        | 11 +++++++++++
 tests/src/issue-194-recursive-struct-projector.rs | 16 ++++++++++++++++
 tests/src/matches.rs                              | 10 ++++++++++
 3 files changed, 37 insertions(+)
 create mode 100644 tests/src/infinite-loop.rs
 create mode 100644 tests/src/issue-194-recursive-struct-projector.rs
 create mode 100644 tests/src/matches.rs

(limited to 'tests/src')

diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
new file mode 100644
index 00000000..906fc1fa
--- /dev/null
+++ b/tests/src/infinite-loop.rs
@@ -0,0 +1,11 @@
+//@ [coq,fstar,lean] skip
+//@ [coq,fstar] aeneas-args=-use-fuel
+//@ [coq,fstar] subdir=misc
+// FIXME: make it work
+fn bar() {}
+
+fn foo() {
+    loop {
+        bar()
+    }
+}
diff --git a/tests/src/issue-194-recursive-struct-projector.rs b/tests/src/issue-194-recursive-struct-projector.rs
new file mode 100644
index 00000000..9ebdc2bc
--- /dev/null
+++ b/tests/src/issue-194-recursive-struct-projector.rs
@@ -0,0 +1,16 @@
+//@ [coq,fstar] subdir=misc
+struct AVLNode<T> {
+    value: T,
+    left: AVLTree<T>,
+    right: AVLTree<T>,
+}
+
+type AVLTree<T> = Option<Box<AVLNode<T>>>;
+
+fn get_val<T>(x: AVLNode<T>) -> T {
+    x.value
+}
+
+fn get_left<T>(x: AVLNode<T>) -> AVLTree<T> {
+    x.left
+}
diff --git a/tests/src/matches.rs b/tests/src/matches.rs
new file mode 100644
index 00000000..5710a604
--- /dev/null
+++ b/tests/src/matches.rs
@@ -0,0 +1,10 @@
+//@ [coq] skip
+//@ [coq,fstar] subdir=misc
+//^ note: coq gives "invalid notation for pattern"
+fn match_u32(x: u32) -> u32 {
+    match x {
+        0 => 0,
+        1 => 1,
+        _ => 2,
+    }
+}
-- 
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')

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


From ae075db15638ee8878bebe3d31affb1aa320e90f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 28 May 2024 18:05:01 +0200
Subject: Reactivate the infinite-loop.rs test

---
 tests/src/infinite-loop.rs | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tests/src')

diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
index 906fc1fa..0e247d20 100644
--- a/tests/src/infinite-loop.rs
+++ b/tests/src/infinite-loop.rs
@@ -1,4 +1,3 @@
-//@ [coq,fstar,lean] skip
 //@ [coq,fstar] aeneas-args=-use-fuel
 //@ [coq,fstar] subdir=misc
 // FIXME: make it work
-- 
cgit v1.2.3