summaryrefslogtreecommitdiff
path: root/tests/src
diff options
context:
space:
mode:
Diffstat (limited to 'tests/src')
-rw-r--r--tests/src/betree/aeneas-test-options4
-rw-r--r--tests/src/hashmap.rs29
-rw-r--r--tests/src/hashmap_main.rs22
-rw-r--r--tests/src/hashmap_utils.rs13
-rw-r--r--tests/src/infinite-loop.rs11
-rw-r--r--tests/src/issue-194-recursive-struct-projector.rs16
-rw-r--r--tests/src/matches.rs10
7 files changed, 69 insertions, 36 deletions
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/hashmap.rs b/tests/src/hashmap.rs
index 4552e4f2..19832a84 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,9 +1,11 @@
+//@ charon-args=--opaque=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 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 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!();
-}
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,
+ }
+}