From 099540ec52b69166946e882a968d4568e39e674f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 8 Mar 2022 16:29:23 +0100
Subject: [PATCH] [aorai] enable dune tests
---
src/plugins/aorai/.gitignore | 2 --
src/plugins/aorai/tests/ptests_config | 4 ++--
src/plugins/aorai/tests/test_config | 2 +-
.../aorai/tests/{test_config_prove.in => test_config_prove} | 2 +-
src/plugins/aorai/tests/ya/dune | 6 ++++++
5 files changed, 10 insertions(+), 6 deletions(-)
rename src/plugins/aorai/tests/{test_config_prove.in => test_config_prove} (62%)
create mode 100644 src/plugins/aorai/tests/ya/dune
diff --git a/src/plugins/aorai/.gitignore b/src/plugins/aorai/.gitignore
index a43b915b9e7..ad6e08d6507 100644
--- a/src/plugins/aorai/.gitignore
+++ b/src/plugins/aorai/.gitignore
@@ -1,9 +1,7 @@
-/tests/*/dune
/aorai_eva_analysis.ml
/Makefile
/*parser*.output
/ptests_local_config.ml
/tests/*/result
-/tests/test_config_prove
/tests/*/result_prove
/top
diff --git a/src/plugins/aorai/tests/ptests_config b/src/plugins/aorai/tests/ptests_config
index a9b80be978b..34b21cc6188 100644
--- a/src/plugins/aorai/tests/ptests_config
+++ b/src/plugins/aorai/tests/ptests_config
@@ -1,2 +1,2 @@
-IGNORE= DEFAULT_SUITES= ya
-IGNORE= prove_SUITES= ya
+DEFAULT_SUITES= ya
+prove_SUITES= ya
diff --git a/src/plugins/aorai/tests/test_config b/src/plugins/aorai/tests/test_config
index 9ff1b014011..641f2fa59a9 100644
--- a/src/plugins/aorai/tests/test_config
+++ b/src/plugins/aorai/tests/test_config
@@ -1,4 +1,4 @@
-PLUGIN: aorai eva,from,scope report wp,rtegen
+PLUGIN: aorai eva,from,scope,inout report wp,rtegen
COMMENT: Path to the library from the test file
LIBS: @PTEST_SUITE_DIR@/../Aorai_test
diff --git a/src/plugins/aorai/tests/test_config_prove.in b/src/plugins/aorai/tests/test_config_prove
similarity index 62%
rename from src/plugins/aorai/tests/test_config_prove.in
rename to src/plugins/aorai/tests/test_config_prove
index ae55e4b9462..3c896a77468 100644
--- a/src/plugins/aorai/tests/test_config_prove.in
+++ b/src/plugins/aorai/tests/test_config_prove
@@ -3,4 +3,4 @@ PLUGIN: aorai eva,from,scope report wp,rtegen
COMMENT: Path to the library from the test file
LIBS: @PTEST_SUITE_DIR@/../Aorai_test
-MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -wp-cache-env -aorai-test-prove-aux-spec
+MACRO: PROVE_OPTIONS -wp-cache-env -aorai-test-prove-aux-spec
diff --git a/src/plugins/aorai/tests/ya/dune b/src/plugins/aorai/tests/ya/dune
new file mode 100644
index 00000000000..1a8230ea13c
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/dune
@@ -0,0 +1,6 @@
+(library
+ (name Name_projects)
+ (modules Name_projects)
+ (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel)
+ (flags -open Frama_c_kernel)
+)
--
GitLab