From 671710afd27761332152b23cbab9e4b316020273 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 25 Jan 2022 22:46:22 +0100
Subject: [PATCH] [tests] avoid warnings about unused files with option -load
---
tests/journal/control.i | 4 ++--
tests/journal/control2.c | 4 ++--
tests/journal/intra.i | 4 ++--
tests/journal/oracle/control.0.res.oracle | 1 -
tests/journal/oracle/control.1.res.oracle | 5 +----
tests/journal/oracle/control.2.res.oracle | 1 -
tests/journal/oracle/control2.res.oracle | 1 -
tests/journal/oracle/intra.res.oracle | 1 -
tests/misc/my_visitor.c | 4 ++--
tests/misc/oracle/my_visitor.0.res.oracle | 1 -
tests/misc/oracle/my_visitor.1.res.oracle | 1 -
tests/saveload/basic.i | 4 ++--
tests/saveload/bool.c | 4 ++--
tests/saveload/callbacks.i | 4 ++--
tests/saveload/deps.i | 4 ++--
tests/saveload/isset.c | 4 ++--
tests/saveload/oracle/basic.0.res.oracle | 1 -
tests/saveload/oracle/basic.1.res.oracle | 1 -
tests/saveload/oracle/basic.2.res.oracle | 1 -
tests/saveload/oracle/basic.3.res.oracle | 1 -
tests/saveload/oracle/basic.4.res.oracle | 1 -
tests/saveload/oracle/bool.0.res.oracle | 1 -
tests/saveload/oracle/bool.1.res.oracle | 1 -
tests/saveload/oracle/callbacks.res.oracle | 1 -
tests/saveload/oracle/deps.0.res.oracle | 1 -
tests/saveload/oracle/deps.1.res.oracle | 1 -
tests/saveload/oracle/deps.2.res.oracle | 1 -
tests/saveload/oracle/deps.3.res.oracle | 1 -
tests/saveload/oracle/deps.4.res.oracle | 1 -
tests/saveload/oracle/isset.0.res.oracle | 1 -
tests/saveload/oracle/isset.1.res.oracle | 1 -
tests/saveload/oracle/isset.2.res.oracle | 1 -
tests/saveload/oracle/isset.3.res.oracle | 1 -
tests/saveload/oracle/segfault_datatypes.res.oracle | 1 -
tests/saveload/oracle/sparecode.res.oracle | 1 -
tests/saveload/segfault_datatypes.i | 4 ++--
tests/saveload/sparecode.i | 4 ++--
37 files changed, 23 insertions(+), 51 deletions(-)
delete mode 100644 tests/saveload/oracle/basic.2.res.oracle
delete mode 100644 tests/saveload/oracle/bool.1.res.oracle
delete mode 100644 tests/saveload/oracle/deps.0.res.oracle
delete mode 100644 tests/saveload/oracle/deps.3.res.oracle
delete mode 100644 tests/saveload/oracle/isset.0.res.oracle
delete mode 100644 tests/saveload/oracle/isset.1.res.oracle
delete mode 100644 tests/saveload/oracle/isset.2.res.oracle
delete mode 100644 tests/saveload/oracle/isset.3.res.oracle
delete mode 100644 tests/saveload/oracle/sparecode.res.oracle
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 2e38a7853a6..ec7902161dd 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
COMMENT: do not compare generated journals since they depend on current time
PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 7145f20651c..9570c6dd3af 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
SCRIPT: @PTEST_RESULT@/control_journal2.ml
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index b7fe01ce6b4..5ae163e21ff 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: @EVA_PLUGINS@ sparecode
MODULE: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index 142ca471781..8191206632c 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -29,7 +29,6 @@
----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 9851832dccb..ae023e8b822 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -29,7 +29,6 @@
----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
@@ -57,9 +56,7 @@
1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 1 warning
+ No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 integer overflow
diff --git a/tests/journal/oracle/control.2.res.oracle b/tests/journal/oracle/control.2.res.oracle
index fb87aaecc1b..2c9d316b3d6 100644
--- a/tests/journal/oracle/control.2.res.oracle
+++ b/tests/journal/oracle/control.2.res.oracle
@@ -1,7 +1,6 @@
1
2
3
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
1
2
3
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index 02360dafcbc..97fb53bb8f6 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -63,7 +63,6 @@
----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 610bcea9ef3..1cd15712237 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -114,4 +114,3 @@
[pdg] done for function stop
[sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c
index 3fe0b7d9092..ffb4b64f503 100644
--- a/tests/misc/my_visitor.c
+++ b/tests/misc/my_visitor.c
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN:
MODULE: @PTEST_NAME@
EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@_sav.res 2> @PTEST_RESULT@/@PTEST_NAME@_sav.err
diff --git a/tests/misc/oracle/my_visitor.0.res.oracle b/tests/misc/oracle/my_visitor.0.res.oracle
index 757a20ca369..99cdff68fd1 100644
--- a/tests/misc/oracle/my_visitor.0.res.oracle
+++ b/tests/misc/oracle/my_visitor.0.res.oracle
@@ -1,4 +1,3 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */
int f(void)
{
diff --git a/tests/misc/oracle/my_visitor.1.res.oracle b/tests/misc/oracle/my_visitor.1.res.oracle
index 14717c12726..cb5171adca0 100644
--- a/tests/misc/oracle/my_visitor.1.res.oracle
+++ b/tests/misc/oracle/my_visitor.1.res.oracle
@@ -4,7 +4,6 @@
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */
int f(void)
{
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index 00a166d2bc6..bde889f55cf 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
MODULE: @PTEST_NAME@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
MODULE:
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index 28424151adb..0761e1802e7 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@"
diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i
index fb98f59a3f4..0d972cf7c43 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ @PTEST_FILE@ -out -calldeps -eva-show-progress -main main1 -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3"
*/
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index 3e27bf10e2c..789392c738d 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
MODULE: deps_A
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps "
diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c
index 9f0dcb12063..67cbc12b5c2 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_NAME@.sav @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-quiet -load %{dep:@PTEST_NAME@.sav}"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
diff --git a/tests/saveload/oracle/basic.0.res.oracle b/tests/saveload/oracle/basic.0.res.oracle
index 919ad3e4907..0fe986b70a1 100644
--- a/tests/saveload/oracle/basic.0.res.oracle
+++ b/tests/saveload/oracle/basic.0.res.oracle
@@ -1,2 +1 @@
[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/basic.1.res.oracle b/tests/saveload/oracle/basic.1.res.oracle
index 2cf7ada6689..00d6006f606 100644
--- a/tests/saveload/oracle/basic.1.res.oracle
+++ b/tests/saveload/oracle/basic.1.res.oracle
@@ -1,4 +1,3 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/saveload/oracle/basic.2.res.oracle b/tests/saveload/oracle/basic.2.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/basic.2.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/basic.3.res.oracle b/tests/saveload/oracle/basic.3.res.oracle
index 16968dd0a24..05d31773bf3 100644
--- a/tests/saveload/oracle/basic.3.res.oracle
+++ b/tests/saveload/oracle/basic.3.res.oracle
@@ -1,2 +1 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
unknown (tried by Test)
diff --git a/tests/saveload/oracle/basic.4.res.oracle b/tests/saveload/oracle/basic.4.res.oracle
index 047acff3e8d..7452402948f 100644
--- a/tests/saveload/oracle/basic.4.res.oracle
+++ b/tests/saveload/oracle/basic.4.res.oracle
@@ -1,2 +1 @@
[kernel] Warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/bool.0.res.oracle b/tests/saveload/oracle/bool.0.res.oracle
index f2e70960028..d193e342d69 100644
--- a/tests/saveload/oracle/bool.0.res.oracle
+++ b/tests/saveload/oracle/bool.0.res.oracle
@@ -1,4 +1,3 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] Computing for function f
[from] Done for function f
[from] Computing for function main
diff --git a/tests/saveload/oracle/bool.1.res.oracle b/tests/saveload/oracle/bool.1.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/bool.1.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/callbacks.res.oracle b/tests/saveload/oracle/callbacks.res.oracle
index 0bf7aca7645..60b806b01fc 100644
--- a/tests/saveload/oracle/callbacks.res.oracle
+++ b/tests/saveload/oracle/callbacks.res.oracle
@@ -1,4 +1,3 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[eva] Analyzing a complete application starting at main2
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/saveload/oracle/deps.0.res.oracle b/tests/saveload/oracle/deps.0.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/deps.0.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/deps.1.res.oracle b/tests/saveload/oracle/deps.1.res.oracle
index 525368b9140..86d7a2aa4ea 100644
--- a/tests/saveload/oracle/deps.1.res.oracle
+++ b/tests/saveload/oracle/deps.1.res.oracle
@@ -1,2 +1 @@
[kernel] Warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/deps.2.res.oracle b/tests/saveload/oracle/deps.2.res.oracle
index 525368b9140..86d7a2aa4ea 100644
--- a/tests/saveload/oracle/deps.2.res.oracle
+++ b/tests/saveload/oracle/deps.2.res.oracle
@@ -1,2 +1 @@
[kernel] Warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/deps.3.res.oracle b/tests/saveload/oracle/deps.3.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/deps.3.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/deps.4.res.oracle b/tests/saveload/oracle/deps.4.res.oracle
index d1126cce5b4..0ace314a020 100644
--- a/tests/saveload/oracle/deps.4.res.oracle
+++ b/tests/saveload/oracle/deps.4.res.oracle
@@ -1,3 +1,2 @@
[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
[kernel] Warning: 1 state in memory reset to their default value. It is inconsistent in this Frama_C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.0.res.oracle b/tests/saveload/oracle/isset.0.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/isset.0.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.1.res.oracle b/tests/saveload/oracle/isset.1.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/isset.1.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.2.res.oracle b/tests/saveload/oracle/isset.2.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/isset.2.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.3.res.oracle b/tests/saveload/oracle/isset.3.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/isset.3.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/segfault_datatypes.res.oracle b/tests/saveload/oracle/segfault_datatypes.res.oracle
index 919ad3e4907..0fe986b70a1 100644
--- a/tests/saveload/oracle/segfault_datatypes.res.oracle
+++ b/tests/saveload/oracle/segfault_datatypes.res.oracle
@@ -1,2 +1 @@
[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/sparecode.res.oracle b/tests/saveload/oracle/sparecode.res.oracle
deleted file mode 100644
index c1a75f49e23..00000000000
--- a/tests/saveload/oracle/sparecode.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i
index 255dc1f7524..f82aa25d341 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,6 +1,6 @@
/* run.config*
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
MODULE: segfault_datatypes_A
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
MODULE: segfault_datatypes_B
diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i
index bfa764fe30d..ffa780633e0 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,6 +1,6 @@
/* run.config
-
-
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: @EVA_PLUGINS@ slicing
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save @PTEST_NAME@.sav @PTEST_FILE@ -then-on 'Slicing export' -print > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
--
GitLab