diff options
| author | Guillaume Boisseau | 2024-05-24 17:10:02 +0200 |
|---|---|---|
| committer | GitHub | 2024-05-24 17:10:02 +0200 |
| commit | 4971b7edf4538144df735f9fa5327fe4d0e2e003 (patch) | |
| tree | 979ed531f66c3b0040fa5714fa70db606ca786c0 /tests/src | |
| parent | fbfa0e13ab56ee847e891fa7d798d2eb226b6794 (diff) | |
| parent | 3adbe18d36df3767e98f30b760ccd9c6ace640ad (diff) | |
Merge pull request #206 from AeneasVerif/subdir
Diffstat (limited to '')
| -rw-r--r-- | tests/src/bitwise.rs | 1 | ||||
| -rw-r--r-- | tests/src/constants.rs | 1 | ||||
| -rw-r--r-- | tests/src/demo.rs | 1 | ||||
| -rw-r--r-- | tests/src/external.rs | 1 | ||||
| -rw-r--r-- | tests/src/loops.rs | 1 | ||||
| -rw-r--r-- | tests/src/no_nested_borrows.rs | 1 | ||||
| -rw-r--r-- | tests/src/paper.rs | 1 | ||||
| -rw-r--r-- | tests/src/polonius_list.rs | 1 |
8 files changed, 8 insertions, 0 deletions
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs index 15962047..fda8eff3 100644 --- a/tests/src/bitwise.rs +++ b/tests/src/bitwise.rs @@ -1,4 +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 925c62b1..ac24dcd4 100644 --- a/tests/src/constants.rs +++ b/tests/src/constants.rs @@ -1,5 +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 b9bb7ca2..0a589338 100644 --- a/tests/src/demo.rs +++ b/tests/src/demo.rs @@ -1,4 +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 ddd5539f..baea76e4 100644 --- a/tests/src/external.rs +++ b/tests/src/external.rs @@ -1,6 +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/loops.rs b/tests/src/loops.rs index 8692c60e..afc52ace 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,6 +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/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 78163371..a250748c 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -1,5 +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 07453098..6a4a7c31 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,5 +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 a8d51e40..b029ad02 100644 --- a/tests/src/polonius_list.rs +++ b/tests/src/polonius_list.rs @@ -1,5 +1,6 @@ //@ charon-args=--polonius //@ aeneas-args=-test-trans-units +//@ [coq,fstar] subdir=misc #![allow(dead_code)] pub enum List<T> { |