diff --git a/tests/journal/control.i b/tests/journal/control.i index 2e38a7853a672a6ac5001098049f2d071b2810c6..ec7902161dda42107bb8d9219dca2ccd293a1079 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 7145f20651cc624cbd09b9baccc6aaca0b4a5d18..9570c6dd3afb3e59c787a9f04594244b196b4e0c 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 b7fe01ce6b42e701a6f422262136a4a062916be6..5ae163e21ff0267076ad57e04d8ddcfc17e1bc2e 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 142ca471781766acb0b16dc9370aaffbdbb429d5..8191206632c5a2badf8b201659e3bc09e88640bc 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 9851832dccb6776c76e6f4c9574148d59299487a..ae023e8b8226ac8ac7a2e86a190dc09f5e2bcd72 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 fb87aaecc1b1525a11fa7308b14d5825ee587f66..2c9d316b3d61cb2542d43b9dcd9eea66d30c10b0 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 02360dafcbcd947c5433d8da5a563e80a378bd8f..97fb53bb8f67b370c1e94911f5b7ef2df89199fc 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 610bcea9ef3c27183ded438e0ef6d75918c58ba8..1cd1571223722dac18125880403465facf99258e 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 3fe0b7d9092d44cecb3f6ff1648da75505f0fee6..ffb4b64f50373a83c58ea1efbeead58e23eee857 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 757a20ca369650eea0ce2c3162081003a9e5dc0d..99cdff68fd11aa9c4e57c0818df7f5a2584787f3 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 14717c12726eef25759c4b1f52744367b6b3fe94..cb5171adca05ef60341ce5813896eed563af564e 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 00a166d2bc6a0603137df5bdad47850a091b6793..bde889f55cfc6d8ecfe71eb05717619cd3067fac 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 28424151adbbe62e3414ccda9195b2e8135e43f8..0761e1802e7b7a271b73e76e97294db78f8ec878 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 fb98f59a3f45e5a8ab26edcb26775996dc2a65ec..0d972cf7c43012e3b243be20b5924529606fd2ce 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 3e27bf10e2c7e731f1f1229a87066c275a0185f6..789392c738d76ac3426b0c1a52b386df8dacedab 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 9f0dcb120637d84ad4d74de0ea49d0667de8370f..67cbc12b5c2ce7a8a3008651ec0fc755487d212c 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 919ad3e4907c1f8e2bf010459d184911758aec0d..0fe986b70a1ed12971d4f09a2d440bb47f152d5f 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 2cf7ada66893ceb8fffd9b80ab2095c00320d0ee..00d6006f60617db5b874f2f3e311887a8ae9347a 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 16968dd0a24898734984c5fc918d12e7491fdd88..05d31773bf3f042e9f9b748cc546aaca05ad6872 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 047acff3e8d77ced0f676b1de446cdbbe0c91952..7452402948f0fad8d57c67cc0b5465f130d5c22a 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 f2e7096002831c02bbf21281a4c13821581bb843..d193e342d69221b4cb1adb9cae3f0f96141e6d86 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 0bf7aca76453ffff5cf74739bde1118eac196bbf..60b806b01fc1701f826f5a5ec33e94ebbe870ef4 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 525368b91402446b298d0242a20cdb75dbd4b268..86d7a2aa4ea6852ffe77c514b82169f16a040c6d 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 525368b91402446b298d0242a20cdb75dbd4b268..86d7a2aa4ea6852ffe77c514b82169f16a040c6d 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 d1126cce5b44973d2f40b213658d3d4be094f7e3..0ace314a020f9c99ef7b61fbdaab5789416dcfd4 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 919ad3e4907c1f8e2bf010459d184911758aec0d..0fe986b70a1ed12971d4f09a2d440bb47f152d5f 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 c1a75f49e233a3557ccc3efb28c191b714eaa1d5..0000000000000000000000000000000000000000 --- 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 255dc1f7524e884b8e2530caba64511f385ec796..f82aa25d3410704ed3a717f9081d97288d5a5569 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 bfa764fe30d810fe6bd68569c909c866b52dbaaa..ffa780633e0759e832e1e61242c69103dcd8f3a8 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}"