diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index d118911f38427d443261b7f717c85b494417e987..021f6e1c9723758db197d34f5068fc63a5a09227 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -71,6 +71,20 @@ let str_global_replace regex repl s =
let res = Str.global_replace regex repl s in
Mutex.unlock str_mutex; res
+(* The match may start after [pos] (instead of [str_string_match]) *)
+let str_string_contains regexp s pos =
+ Mutex.lock str_mutex;
+ let res = try
+ ignore (Str.search_forward regexp s pos) ;
+ true
+ with Not_found -> false
+ in
+ Mutex.unlock str_mutex; res
+
+let str_string_contains_option opt =
+ let re = Str.regexp ("\\( \\|^\\)"^ opt ^ "\\( \\|=\\|$\\)") in
+ str_string_contains re
+
let str_string_match regex s n =
Mutex.lock str_mutex;
let res = Str.string_match regex s n in
@@ -344,7 +358,7 @@ let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
let macro_default_options = ref "-journal-disable -check -no-autoload-plugins"
let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
-let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
+let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
let default_toplevel = ref "@frama-c@"
(* Those variables are read from a ptests_config file *)
@@ -771,7 +785,11 @@ struct
let has_frama_c_exe = ref false in
if !verbosity >= 4 then lock_printf "%% Expand: %s@." s;
if !verbosity >= 5 then print_macros macros;
+ let nb_loops = ref 0 in
let rec aux s =
+ if !nb_loops > 100 then
+ fail "Possible infinite recursion in macro expands"
+ else incr nb_loops ;
let expand_macro = function
| Str.Text s -> s
| Str.Delim s ->
@@ -812,14 +830,9 @@ struct
let expand_directive =
let deprecated_opts = "(-load-module|-load-script)" in
- let re = Str.regexp "\\(-load-module\\|-load-script\\)" in
+ let contains_deprecated_opts = str_string_contains_option "\\(-load-module\\|-load-script\\)" in
fun ~file macros s ->
- Mutex.lock str_mutex;
- let contains =
- try ignore (Str.search_forward re s 0); true
- with Not_found -> false
- in
- Mutex.unlock str_mutex;
+ let contains = contains_deprecated_opts s 0 in
if contains then lock_eprintf "%s: DEPRECATED direct use of %s option: %s@.Please use PLUGIN, MODULE, SCRIPT or LIBS directive instead of the deprecated option.@." file deprecated_opts s;
expand macros s
@@ -1576,23 +1589,21 @@ end = struct
let process_macros s = Macros.expand macros s in
let toplevel =
let toplevel = log_default_filter cmd.toplevel in
- let in_toplevel,toplevel= Macros.does_expand macros toplevel in
- if not cmd.execnow then begin
- let has_ptest_file, options =
- if in_toplevel.has_ptest_opt then in_toplevel.has_ptest_file, []
- else
- let in_option,options= Macros.does_expand macros cmd.options in
- (in_option.has_ptest_file || in_toplevel.has_ptest_file),
- (if in_toplevel.has_frama_c_exe then
- [ process_macros "@PTEST_PRE_OPTIONS@" ;
- options ;
- process_macros "@PTEST_POST_OPTIONS@" ;
- ]
- else [ options ])
+ let in_toplevel,toplevel = Macros.does_expand macros toplevel in
+ if cmd.execnow || in_toplevel.has_ptest_opt then toplevel
+ else begin
+ let has_ptest_file,options =
+ let in_option,options = Macros.does_expand macros cmd.options in
+ (in_option.has_ptest_file || in_toplevel.has_ptest_file),
+ (if in_toplevel.has_frama_c_exe then
+ [ process_macros "@PTEST_PRE_OPTIONS@" ;
+ options ;
+ process_macros "@PTEST_POST_OPTIONS@" ;
+ ]
+ else [ options ])
in
String.concat " " (toplevel::(if has_ptest_file then options else ptest_file::options))
end
- else toplevel
in
let toplevel = get_ptest_toplevel cmd (dune_feature_cmd toplevel) in
{ cmd with
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index 656a6b9bc1ee85ae90e3f525027d76edad9d7baf..c53452aa6966c517b9b960fc3dad049dabec7538 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,22 +1,26 @@
/* run.config
COMMENT: run.config is intentionally not-*
-PLUGIN:
+ PLUGIN:
EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_RESULT@/absorb.sav @PTEST_FILE@ > @PTEST_RESULT@/absorb_sav.res 2> @PTEST_RESULT@/absorb_sav.err
-PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load %{dep:@PTEST_RESULT@/absorb.sav} -eva @EVA_CONFIG@ -float-hex -save @PTEST_RESULT@/absorb.sav2 > @PTEST_RESULT@/absorb_sav2.res 2> @PTEST_RESULT@/absorb_sav2.err
+ COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose.
+ CMD: @frama-c@ @PTEST_OPTIONS@
OPT: -load %{dep:@PTEST_RESULT@/absorb.sav2} -deps -out -input
*/
/* run.config*
DONTRUN:
*/
#include "__fc_builtin.h"
+
float x = 1.0, y = 0.0, z, t, min_f, min_fl, den;
+
void main() {
long long b = Frama_C_interval(-2000000001, 2000000001);
b = b * b;
z = y + 1e-286;
while (y != x)
- {
+ {
y = x ; x+=1E-286;
}
t = b;
diff --git a/tests/float/oracle/absorb.res.oracle b/tests/float/oracle/absorb.res.oracle
index e65974a16042b3455328846be038095c5823a861..1b5788d6e983af2f8621e1a5b3818f191b9e2b39 100644
--- a/tests/float/oracle/absorb.res.oracle
+++ b/tests/float/oracle/absorb.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 main
[from] Computing for function Frama_C_interval <-main
[from] Done for function Frama_C_interval
diff --git a/tests/float/oracle/absorb_sav.res b/tests/float/oracle/absorb_sav.res
index a618fee603c74d4ec344f842264c96a1263f1094..280a79a32b2a298c2da2a13e2f5a05d8d007b572 100644
--- a/tests/float/oracle/absorb_sav.res
+++ b/tests/float/oracle/absorb_sav.res
@@ -1,4 +1,4 @@
[kernel] Parsing absorb.c (with preprocessing)
-[kernel:parser:decimal-float] absorb.c:17: Warning:
+[kernel:parser:decimal-float] absorb.c:21: Warning:
Floating-point constant 1e-286 is not represented exactly. Will use 0x1.e74404f3daadbp-951.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/tests/float/oracle/absorb_sav2.res b/tests/float/oracle/absorb_sav2.res
index 0e6e5f6ef81892ec580bfcb78555dbae39034e45..b34d714dc2c19196b811c578a6f23f2753032f77 100644
--- a/tests/float/oracle/absorb_sav2.res
+++ b/tests/float/oracle/absorb_sav2.res
@@ -10,12 +10,12 @@
min_fl ∈ {0}
den ∈ {0}
[eva] computing for function Frama_C_interval <- main.
- Called from absorb.c:15.
+ Called from absorb.c:19.
[eva] using specification for function Frama_C_interval
-[eva] absorb.c:15:
+[eva] absorb.c:19:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] absorb.c:18: starting to merge loop iterations
+[eva] absorb.c:22: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 092afe2d239cccf9ed270389b444989500316f10..ec7902161dda42107bb8d9219dca2ccd293a1079 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,4 +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 885d7f07b81496997a68cdd8dc6f8473b7dbd5b8..9570c6dd3afb3e59c787a9f04594244b196b4e0c 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,4 +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 f19b1d606e2881b0abda42cc04213ea7cd16dc23..5ae163e21ff0267076ad57e04d8ddcfc17e1bc2e 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,4 +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 f97cd8e9dafd9a3774d5e3a1003d90f598feded1..8191206632c5a2badf8b201659e3bc09e88640bc 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control.i:22: starting to merge loop iterations
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva] control.i:24: starting to merge loop iterations
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -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 0f89b91f804351f04acb5d47bfc56735386ec5b8..ae023e8b8226ac8ac7a2e86a190dc09f5e2bcd72 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control.i:22: starting to merge loop iterations
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva] control.i:24: starting to merge loop iterations
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -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:
@@ -43,7 +42,7 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva:alarm] control.i:25: Warning: signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[from] Computing for function f
[from] Done for 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 acf4746fb0c54e7a06c20e5f47a5a29fc7244bd7..97fb53bb8f67b370c1e94911f5b7ef2df89199fc 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning:
+[eva] control2.c:14: starting to merge loop iterations
+[eva:alarm] control2.c:17: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -37,12 +37,12 @@
y ∈ [--..--]
c ∈ [--..--]
d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:15: Warning:
signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
[eva:alarm] control2.c:15: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control2.c:17: Warning:
+ signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
@@ -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/control2_sav.res b/tests/journal/oracle/control2_sav.res
index 2a9246db51c537dbcb841ca4f96aa7170df83043..1734f9bb5372539b42ca6899a554625e521d5272 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning:
+[eva] control2.c:14: starting to merge loop iterations
+[eva:alarm] control2.c:17: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -38,12 +38,12 @@
y ∈ [--..--]
c ∈ [--..--]
d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:15: Warning:
signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
[eva:alarm] control2.c:15: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control2.c:17: Warning:
+ signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 1d0c56f4f1dfc363f663efd08c22315be831b308..1cd1571223722dac18125880403465facf99258e 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -8,49 +8,49 @@
X10 ∈ {0}
Y10 ∈ {0}
[eva] computing for function param <- main.
- Called from intra.i:81.
+ Called from intra.i:83.
[eva] Recording results for param
[eva] Done for function param
[eva] computing for function tmp <- main.
- Called from intra.i:82.
-[eva] intra.i:20: assertion got status valid.
+ Called from intra.i:84.
[eva] intra.i:22: assertion got status valid.
+[eva] intra.i:24: assertion got status valid.
[eva] Recording results for tmp
[eva] Done for function tmp
[eva] computing for function spare_called_fct <- main.
- Called from intra.i:83.
+ Called from intra.i:85.
[eva] Recording results for spare_called_fct
[eva] Done for function spare_called_fct
[eva] computing for function call_two_outputs <- main.
- Called from intra.i:84.
+ Called from intra.i:86.
[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:48.
+ Called from intra.i:50.
[eva] Recording results for two_outputs
[eva] Done for function two_outputs
[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:52.
+ Called from intra.i:54.
[eva] Recording results for two_outputs
[eva] Done for function two_outputs
[eva] Recording results for call_two_outputs
[eva] Done for function call_two_outputs
[eva] computing for function loop <- main.
- Called from intra.i:85.
-[eva] intra.i:63: assertion got status valid.
-[eva] intra.i:64: loop invariant got status valid.
-[eva] intra.i:66: starting to merge loop iterations
+ Called from intra.i:87.
+[eva] intra.i:65: assertion got status valid.
+[eva] intra.i:66: loop invariant got status valid.
+[eva] intra.i:68: starting to merge loop iterations
[eva] Recording results for loop
[eva] Done for function loop
[eva] computing for function assign <- main.
- Called from intra.i:86.
+ Called from intra.i:88.
[eva] Recording results for assign
[eva] Done for function assign
[eva] computing for function assign <- main.
- Called from intra.i:87.
+ Called from intra.i:89.
[eva] Recording results for assign
[eva] Done for function assign
[eva] computing for function stop <- main.
- Called from intra.i:90.
-[kernel:annot:missing-spec] intra.i:90: Warning:
+ Called from intra.i:92.
+[kernel:annot:missing-spec] intra.i:92: Warning:
Neither code nor specification for function stop, generating default assigns from the prototype
[eva] using specification for function stop
[eva] Done for function stop
@@ -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 da957b1c8e130b2f5faa33e3c6a0daa54a305a62..ffb4b64f50373a83c58ea1efbeead58e23eee857 100644
--- a/tests/misc/my_visitor.c
+++ b/tests/misc/my_visitor.c
@@ -1,4 +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 338816e01c2355f5716f7ed4b3144d56da296b78..bde889f55cfc6d8ecfe71eb05717619cd3067fac 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,4 +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 b6b40e894029de1144330278dc6275e90de09ef8..0761e1802e7b7a271b73e76e97294db78f8ec878 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,4 +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 31a79ab6d68372e612132f48bfbb8286b85ea3f5..0d972cf7c43012e3b243be20b5924529606fd2ce 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,4 +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 f52f160618655e9f5b6a1fde609b2fbeee9e9940..789392c738d76ac3426b0c1a52b386df8dacedab 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,4 +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 9e8eb7af8624a4f22ff7a1b48287f5bf3575dd04..67cbc12b5c2ce7a8a3008651ec0fc755487d212c 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,4 +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/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index 2d8d381c7cbfedc39e3f5d60bcde3cd09134cc17..8e9fab3900539a0111c80c9798d86efeb94bd94a 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -4,9 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] basic.i:18: assertion got status valid.
-[eva] basic.i:19: starting to merge loop iterations
-[eva:alarm] basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] basic.i:20: assertion got status valid.
+[eva] basic.i:21: starting to merge loop iterations
+[eva:alarm] basic.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index 2d8d381c7cbfedc39e3f5d60bcde3cd09134cc17..8e9fab3900539a0111c80c9798d86efeb94bd94a 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -4,9 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] basic.i:18: assertion got status valid.
-[eva] basic.i:19: starting to merge loop iterations
-[eva:alarm] basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] basic.i:20: assertion got status valid.
+[eva] basic.i:21: starting to merge loop iterations
+[eva:alarm] basic.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
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/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 7a24197dd13a11b3d32faf881abf47700079f65b..b05786274e09835b0456d757bbf858d4da3ef511 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -6,36 +6,36 @@
x ∈ {0}
y ∈ {0}
[eva] computing for function f <- main.
- Called from bool.c:25.
-[eva] bool.c:17: assertion got status valid.
-[eva] bool.c:18: starting to merge loop iterations
-[eva:alarm] bool.c:18: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+ Called from bool.c:27.
+[eva] bool.c:19: assertion got status valid.
+[eva] bool.c:20: starting to merge loop iterations
+[eva:alarm] bool.c:20: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function printf_va_1 <- main.
- Called from bool.c:27.
+ Called from bool.c:29.
[eva] using specification for function printf_va_1
-[eva] bool.c:27: function printf_va_1: precondition got status valid.
+[eva] bool.c:29: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function printf_va_2 <- main.
- Called from bool.c:29.
+ Called from bool.c:31.
[eva] using specification for function printf_va_2
-[eva] bool.c:29: function printf_va_2: precondition got status valid.
+[eva] bool.c:31: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
- Called from bool.c:31.
+ Called from bool.c:33.
[eva] using specification for function printf_va_3
-[eva] bool.c:31: function printf_va_3: precondition got status valid.
+[eva] bool.c:33: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function printf_va_4 <- main.
- Called from bool.c:33.
+ Called from bool.c:35.
[eva] using specification for function printf_va_4
-[eva] bool.c:33: function printf_va_4: precondition got status valid.
+[eva] bool.c:35: function printf_va_4: precondition got status valid.
[eva] Done for function printf_va_4
[eva] computing for function printf_va_5 <- main.
- Called from bool.c:35.
+ Called from bool.c:37.
[eva] using specification for function printf_va_5
-[eva] bool.c:35: function printf_va_5: precondition got status valid.
+[eva] bool.c:37: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/saveload/oracle/callbacks.res.oracle b/tests/saveload/oracle/callbacks.res.oracle
index ae9563d2b2b8ce582d84ca2bef1b6bd3dd9006f3..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
@@ -6,9 +5,9 @@
x ∈ {0}
y ∈ {0}
[eva] computing for function g1 <- main2.
- Called from callbacks.i:30.
+ Called from callbacks.i:32.
[eva] computing for function f <- g1 <- main2.
- Called from callbacks.i:16.
+ Called from callbacks.i:18.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -18,9 +17,9 @@
[from] Done for function g1
[eva] Done for function g1
[eva] computing for function g2 <- main2.
- Called from callbacks.i:31.
+ Called from callbacks.i:33.
[eva] computing for function f <- g2 <- main2.
- Called from callbacks.i:21.
+ Called from callbacks.i:23.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -34,13 +33,13 @@
[from] Done for function main2
[eva] done for function main2
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
y FROM p
-[from] call to g1 at callbacks.i:30 (by main2):
+[from] call to g1 at callbacks.i:32 (by main2):
x FROM \nothing
-[from] call to g2 at callbacks.i:31 (by main2):
+[from] call to g2 at callbacks.i:33 (by main2):
y FROM \nothing
[from] entry point:
x FROM \nothing
@@ -61,9 +60,9 @@
x ∈ {0}
y ∈ {0}
[eva] computing for function g1 <- main3.
- Called from callbacks.i:35.
+ Called from callbacks.i:37.
[eva] computing for function f <- g1 <- main3.
- Called from callbacks.i:16.
+ Called from callbacks.i:18.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -73,9 +72,9 @@
[from] Done for function g1
[eva] Done for function g1
[eva] computing for function g2 <- main3.
- Called from callbacks.i:36.
+ Called from callbacks.i:38.
[eva] computing for function f <- g2 <- main3.
- Called from callbacks.i:21.
+ Called from callbacks.i:23.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -89,13 +88,13 @@
[from] Done for function main3
[eva] done for function main3
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
y FROM p
-[from] call to g1 at callbacks.i:35 (by main3):
+[from] call to g1 at callbacks.i:37 (by main3):
x FROM \nothing
-[from] call to g2 at callbacks.i:36 (by main3):
+[from] call to g2 at callbacks.i:38 (by main3):
y FROM \nothing
[from] entry point:
x FROM \nothing
diff --git a/tests/saveload/oracle/callbacks_sav.res b/tests/saveload/oracle/callbacks_sav.res
index 9e942d99e7f83b4e5f7643cffc474c9c39d2e506..294a67f3fe59243bedc5da3aebccce7995d75f20 100644
--- a/tests/saveload/oracle/callbacks_sav.res
+++ b/tests/saveload/oracle/callbacks_sav.res
@@ -6,9 +6,9 @@
x ∈ {0}
y ∈ {0}
[eva] computing for function g1 <- main1.
- Called from callbacks.i:25.
+ Called from callbacks.i:27.
[eva] computing for function f <- g1 <- main1.
- Called from callbacks.i:16.
+ Called from callbacks.i:18.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -18,9 +18,9 @@
[from] Done for function g1
[eva] Done for function g1
[eva] computing for function g2 <- main1.
- Called from callbacks.i:26.
+ Called from callbacks.i:28.
[eva] computing for function f <- g2 <- main1.
- Called from callbacks.i:21.
+ Called from callbacks.i:23.
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
@@ -45,13 +45,13 @@
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to f at callbacks.i:16 (by g1):
+[from] call to f at callbacks.i:18 (by g1):
x FROM p
-[from] call to f at callbacks.i:21 (by g2):
+[from] call to f at callbacks.i:23 (by g2):
y FROM p
-[from] call to g1 at callbacks.i:25 (by main1):
+[from] call to g1 at callbacks.i:27 (by main1):
x FROM \nothing
-[from] call to g2 at callbacks.i:26 (by main1):
+[from] call to g2 at callbacks.i:28 (by main1):
y FROM \nothing
[from] entry point:
x FROM \nothing
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/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 103d5a3540df28ec7894e9cec410ffc4e6c8097e..516b5aaa9c355dd58ac0dba9a1de29d2dfa1fdc3 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] deps.i:19: starting to merge loop iterations
-[eva:alarm] deps.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva] deps.i:21: starting to merge loop iterations
+[eva:alarm] deps.i:21: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
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/isset_sav.res b/tests/saveload/oracle/isset_sav.res
index f2693a09a703f2ac60abde786ce875d8b5aaf428..6c37866d4873f65d073c1ddd5e8e2809474c9090 100644
--- a/tests/saveload/oracle/isset_sav.res
+++ b/tests/saveload/oracle/isset_sav.res
@@ -1 +1 @@
-[eva:alarm] isset.c:13: Warning: signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] isset.c:15: Warning: signed overflow. assert -2147483648 ≤ i - 1;
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/segfault_datatypes_sav.res b/tests/saveload/oracle/segfault_datatypes_sav.res
index 3aece07549bce1d601a9775123b3ace2d2ebade7..773e46ed9de6a9b8d046630df082ddc385da9d94 100644
--- a/tests/saveload/oracle/segfault_datatypes_sav.res
+++ b/tests/saveload/oracle/segfault_datatypes_sav.res
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] segfault_datatypes.i:12: starting to merge loop iterations
-[eva:alarm] segfault_datatypes.i:12: Warning:
+[eva] segfault_datatypes.i:14: starting to merge loop iterations
+[eva:alarm] segfault_datatypes.i:14: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
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/oracle/sparecode_sav.res b/tests/saveload/oracle/sparecode_sav.res
index 36b458ce885011f637ab5b5355569f1ac10771fb..7f7224a92580a85386ee8d10c43884311124310e 100644
--- a/tests/saveload/oracle/sparecode_sav.res
+++ b/tests/saveload/oracle/sparecode_sav.res
@@ -6,15 +6,15 @@
[eva:initial-state] Values of globals at initialization
G ∈ {0}
[eva] computing for function f <- main.
- Called from sparecode.i:16.
+ Called from sparecode.i:18.
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function f <- main.
- Called from sparecode.i:17.
+ Called from sparecode.i:19.
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function f <- main.
- Called from sparecode.i:18.
+ Called from sparecode.i:20.
[eva] Recording results for f
[eva] Done for function f
[eva] Recording results for main
diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i
index 7cba664a76f74269d272e7d24bbcaa2aa6a8e42c..f82aa25d3410704ed3a717f9081d97288d5a5569 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,4 +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 b1e13d655e34e8f47b96597e5c40b2fe6fc7a241..ffa780633e0759e832e1e61242c69103dcd8f3a8 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,4 +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}"