From 20835991b1b84bd5ad6bf699526e42f354ca3aef Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 28 Apr 2021 17:07:36 +0200
Subject: [PATCH] [ptests] more use of the MODULE directive
---
tests/misc/global_decl_loc.i | 3 +-
tests/misc/global_decl_loc2.i | 5 ++-
tests/misc/oracle/global_decl_loc.res.oracle | 2 +-
tests/misc/oracle/global_decl_loc2.res.oracle | 2 +-
tests/misc/test_config | 3 +-
tests/pdg/dyn_dpds.c | 4 +--
tests/saveload/deps.i | 18 ++++++----
tests/saveload/oracle/deps_sav.res | 4 +--
tests/saveload/serialized_queue.i | 4 +--
tests/slicing/adpcm.c | 6 ++--
tests/slicing/combine.i | 6 ++--
tests/slicing/ex_spec_interproc.i | 6 ++--
tests/slicing/mark_all_slices.i | 6 ++--
tests/slicing/merge.i | 6 ++--
tests/slicing/min_call.c | 6 ++--
tests/slicing/select_by_annot.i | 36 +++++++++----------
tests/slicing/select_simple.c | 6 ++--
tests/slicing/simple_intra_slice.i | 6 ++--
tests/slicing/slice_no_body.i | 6 ++--
tests/slicing/switch.i | 6 ++--
tests/slicing/test_config | 3 +-
21 files changed, 75 insertions(+), 69 deletions(-)
diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i
index d13cbce8473..e0f0ea85b89 100644
--- a/tests/misc/global_decl_loc.i
+++ b/tests/misc/global_decl_loc.i
@@ -1,4 +1,5 @@
/* run.config
- OPT: @PTEST_DIR@/global_decl_loc2.i -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: global_decl_loc
+ OPT: @PTEST_DIR@/global_decl_loc2.i
*/
int g;
diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i
index 348015c7c22..5f1867c879f 100644
--- a/tests/misc/global_decl_loc2.i
+++ b/tests/misc/global_decl_loc2.i
@@ -1,7 +1,6 @@
/* run.config*
- EXIT: 0
-
- OPT: @PTEST_DIR@/global_decl_loc.i -load-module @PTEST_DIR@/global_decl_loc.cmxs
+ MODULE: global_decl_loc
+ OPT: @PTEST_DIR@/global_decl_loc.i
*/
extern int g;
diff --git a/tests/misc/oracle/global_decl_loc.res.oracle b/tests/misc/oracle/global_decl_loc.res.oracle
index 91dcbad389e..ebeec539157 100644
--- a/tests/misc/oracle/global_decl_loc.res.oracle
+++ b/tests/misc/oracle/global_decl_loc.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:4
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
diff --git a/tests/misc/oracle/global_decl_loc2.res.oracle b/tests/misc/oracle/global_decl_loc2.res.oracle
index cb0dd4ebc1e..454d932e2db 100644
--- a/tests/misc/oracle/global_decl_loc2.res.oracle
+++ b/tests/misc/oracle/global_decl_loc2.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:4
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
diff --git a/tests/misc/test_config b/tests/misc/test_config
index 49f38b4a622..111c3478837 100644
--- a/tests/misc/test_config
+++ b/tests/misc/test_config
@@ -1 +1,2 @@
-EXECNOW: make -s @PTEST_DIR@/global_decl_loc.cmxs
+MODULE: global_decl_loc
+MODULE:
diff --git a/tests/pdg/dyn_dpds.c b/tests/pdg/dyn_dpds.c
index 8c40c94f19d..ac0cc5c1557 100644
--- a/tests/pdg/dyn_dpds.c
+++ b/tests/pdg/dyn_dpds.c
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -deps"
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-deps"
*/
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index ee704399b40..267cbfcdb30 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,11 +1,15 @@
/* run.config
- EXECNOW: make -s ./tests/saveload/deps_A.cmxs ./tests/saveload/deps_B.cmxs ./tests/saveload/deps_C.cmxs ./tests/saveload/deps_D.cmxs ./tests/saveload/deps_E.cmxs
- EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module ./tests/saveload/deps_A.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
- STDOPT: +"-load-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
- STDOPT: +"-load-module ./tests/saveload/deps_B -load ./tests/saveload/result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./tests/saveload/deps_C -load ./tests/saveload/result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./tests/saveload/deps_D -load ./tests/saveload/result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./tests/saveload/deps_E -load ./tests/saveload/result/deps.sav -out -input -deps "
+ MODULE: deps_A
+ EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
+ STDOPT: +"-load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
+ MODULE: deps_B
+ STDOPT: +"-load ./tests/saveload/result/deps.sav -out -input -deps "
+ MODULE: deps_C
+ STDOPT: +"-load ./tests/saveload/result/deps.sav -out -input -deps "
+ MODULE: deps_D
+ STDOPT: +"-load ./tests/saveload/result/deps.sav -out -input -deps "
+ MODULE: deps_E
+ STDOPT: +"-load ./tests/saveload/result/deps.sav -out -input -deps "
*/
int main() {
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 40f9aeda114..dcd6cc73934 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/saveload/deps.i:15: starting to merge loop iterations
-[eva:alarm] tests/saveload/deps.i:15: Warning:
+[eva] tests/saveload/deps.i:19: starting to merge loop iterations
+[eva:alarm] tests/saveload/deps.i:19: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/saveload/serialized_queue.i b/tests/saveload/serialized_queue.i
index 3d2c450536e..cff84088124 100644
--- a/tests/saveload/serialized_queue.i
+++ b/tests/saveload/serialized_queue.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+ OPT:
*/
// empty C file, we're only interested in the script itself
diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c
index a3efe43e78c..c32b08423fe 100644
--- a/tests/slicing/adpcm.c
+++ b/tests/slicing/adpcm.c
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -machdep x86_32 -ulevel -1 -deps -slicing-level 2 -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -machdep x86_32 -ulevel -1 -deps -slicing-level 2
*/
#include "../test/adpcm.c"
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 0f9079399f4..704851ba393 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps
*/
//@ assigns \result \from x;
diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i
index d767426b85f..5436193b3db 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps
*/
int X, Y;
diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index 9b5441dd0b4..8f0d154cfd2 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers
*/
int A, B, C, D;
int A2, B2, C2, D2;
diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i
index b255a2c2fe7..568d5231c75 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -journal-disable
+ MODULE: libSelect libAnim @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps -slicing-level 3
*/
int G1, G2, G3;
diff --git a/tests/slicing/min_call.c b/tests/slicing/min_call.c
index 5e833483762..6ed48e08f23 100644
--- a/tests/slicing/min_call.c
+++ b/tests/slicing/min_call.c
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -journal-disable -slicing-level 3
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -slicing-level 3
*/
/* dummy source file in order to test minimal calls feature
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 500831ba3d7..6d0e19a38c4 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,23 +1,23 @@
/* run.config
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- MODULE: @PTEST_NAME@
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable
+
+ MODULE: libSelect @PTEST_NAME@
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main
+
MODULE:
- CMD: bin/toplevel.opt
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
*/
struct Tstr { int a; int b; } S;
diff --git a/tests/slicing/select_simple.c b/tests/slicing/select_simple.c
index de81f2fc724..735494d4169 100644
--- a/tests/slicing/select_simple.c
+++ b/tests/slicing/select_simple.c
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps
*/
/* dummy source file in order to test select_simple.ml */
diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i
index 24d8beb4b83..b3992a123e7 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -no-slice-callers -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps -no-slice-callers
*/
int Unknown;
int G;
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index aebe5da2b2c..79b40ad2e32 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main h -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main h
*/
int G;
diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i
index 997d28ba405..dfd7b56cf1c 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,7 +1,7 @@
/* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+ OPT: @EVA_OPTIONS@ -deps
*/
int main (char choix) {
int x = 0, y = 0, z = 0;
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index a709a3c91d3..1c214a23023 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,3 @@
-EXECNOW: make -s tests/slicing/libSelect.cmxs tests/slicing/libAnim.cmxs
+MODULE: libSelect libAnim
+MODULE:
OPT: @EVA_OPTIONS@ -machdep x86_32
--
GitLab