summaryrefslogtreecommitdiff
path: root/tests/src
diff options
context:
space:
mode:
Diffstat (limited to 'tests/src')
-rw-r--r--tests/src/arrays.rs3
-rw-r--r--tests/src/bitwise.rs1
-rw-r--r--tests/src/constants.rs2
-rw-r--r--tests/src/demo.rs1
-rw-r--r--tests/src/external.rs3
-rw-r--r--tests/src/hashmap.rs8
-rw-r--r--tests/src/hashmap_main.rs6
-rw-r--r--tests/src/hashmap_utils.rs1
-rw-r--r--tests/src/loops.rs3
-rw-r--r--tests/src/nested_borrows.rs2
-rw-r--r--tests/src/no_nested_borrows.rs2
-rw-r--r--tests/src/paper.rs2
-rw-r--r--tests/src/polonius_list.rs2
-rw-r--r--tests/src/traits.rs1
14 files changed, 37 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..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;