Merge branch 'main' into son/loops2

21 files changed, 140 insertions, 28 deletions

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/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
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 9f48cb04..fda8eff3 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,3 +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 83904eed..ac24dcd4 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,3 +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 bc74cc8b..0a589338 100644
--- a/tests/src/demo.rs
+++ b/tests/src/demo.rs
@@ -1,3 +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 521749d6..baea76e4 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,3 +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/hashmap.rs b/tests/src/hashmap.rs
index 58d22acd..19832a84 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,3 +1,13 @@
+//@ charon-args=--opaque=utils
+//@ aeneas-args=-state -split-files
+//@ [coq] aeneas-args=-use-fuel
+//@ [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.
 //!
 //! Current limitations:
@@ -306,6 +316,31 @@ impl<T> HashMap<T> {
     }
 }
 
+// This is a module so we can tell charon to leave it opaque
+mod 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 = utils::deserialize();
+    // Update
+    hm.insert(key, value);
+    // Serialize
+    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 45dfa6e2..00000000
--- a/tests/src/hashmap_main.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-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 cd7b481f..00000000
--- a/tests/src/hashmap_utils.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-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!();
-}
diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
new file mode 100644
index 00000000..0e247d20
--- /dev/null
+++ b/tests/src/infinite-loop.rs
@@ -0,0 +1,10 @@
+//@ [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/loops.rs b/tests/src/loops.rs
index 2f71d75b..afc52ace 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,3 +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/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,
+    }
+}
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/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 88c0bc09..6d3074ef 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,3 +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 156f13ab..6a4a7c31 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,3 +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 8c64110d..b029ad02 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,3 +1,6 @@
+//@ charon-args=--polonius
+//@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
 pub enum List<T> {
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
new file mode 100644
index 00000000..f8490e76
--- /dev/null
+++ b/tests/src/string-chars.rs
@@ -0,0 +1,7 @@
+//@ [lean] known-failure
+//@ [coq,fstar] skip
+//@ no-check-output
+fn main() {
+    let s = "hello";
+    let _chs: Vec<char> = s.chars().collect();
+}
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;