diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/src/arrays.rs | 3 | ||||
| -rw-r--r-- | tests/src/bitwise.rs | 2 | ||||
| -rw-r--r-- | tests/src/constants.rs | 3 | ||||
| -rw-r--r-- | tests/src/demo.rs | 2 | ||||
| -rw-r--r-- | tests/src/external.rs | 4 | ||||
| -rw-r--r-- | tests/src/hashmap.rs | 8 | ||||
| -rw-r--r-- | tests/src/hashmap_main.rs | 6 | ||||
| -rw-r--r-- | tests/src/hashmap_utils.rs | 1 | ||||
| -rw-r--r-- | tests/src/loops.rs | 4 | ||||
| -rw-r--r-- | tests/src/nested_borrows.rs | 2 | ||||
| -rw-r--r-- | tests/src/no_nested_borrows.rs | 3 | ||||
| -rw-r--r-- | tests/src/paper.rs | 3 | ||||
| -rw-r--r-- | tests/src/polonius_list.rs | 3 | ||||
| -rw-r--r-- | tests/src/traits.rs | 1 |
14 files changed, 45 insertions, 0 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/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..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..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/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..a250748c 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/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; |