diff options
Diffstat (limited to '')
-rw-r--r-- | tests/src/betree/aeneas-test-options | 4 | ||||
-rw-r--r-- | tests/src/hashmap.rs | 29 | ||||
-rw-r--r-- | tests/src/hashmap_main.rs | 22 | ||||
-rw-r--r-- | tests/src/hashmap_utils.rs | 13 | ||||
-rw-r--r-- | tests/src/infinite-loop.rs | 11 | ||||
-rw-r--r-- | tests/src/issue-194-recursive-struct-projector.rs | 16 | ||||
-rw-r--r-- | tests/src/matches.rs | 10 |
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, + } +} |