diff --git a/tests/journal/control.i b/tests/journal/control.i
index 092afe2d239cccf9ed270389b444989500316f10..2e38a7853a672a6ac5001098049f2d071b2810c6 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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..7145f20651cc624cbd09b9baccc6aaca0b4a5d18 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,4 +1,6 @@
/* run.config
+
+
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..b7fe01ce6b42e701a6f422262136a4a062916be6 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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..142ca471781766acb0b16dc9370aaffbdbb429d5 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 ======
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 0f89b91f804351f04acb5d47bfc56735386ec5b8..9851832dccb6776c76e6f4c9574148d59299487a 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 ======
@@ -43,7 +43,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
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index acf4746fb0c54e7a06c20e5f47a5a29fc7244bd7..02360dafcbcd947c5433d8da5a563e80a378bd8f 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:
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..610bcea9ef3c27183ded438e0ef6d75918c58ba8 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
diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c
index da957b1c8e130b2f5faa33e3c6a0daa54a305a62..3fe0b7d9092d44cecb3f6ff1648da75505f0fee6 100644
--- a/tests/misc/my_visitor.c
+++ b/tests/misc/my_visitor.c
@@ -1,4 +1,6 @@
/* run.config
+
+
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/saveload/basic.i b/tests/saveload/basic.i
index 338816e01c2355f5716f7ed4b3144d56da296b78..00a166d2bc6a0603137df5bdad47850a091b6793 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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..28424151adbbe62e3414ccda9195b2e8135e43f8 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,4 +1,6 @@
/* run.config
+
+
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..fb98f59a3f45e5a8ab26edcb26775996dc2a65ec 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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..3e27bf10e2c7e731f1f1229a87066c275a0185f6 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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..9f0dcb120637d84ad4d74de0ea49d0667de8370f 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,4 +1,6 @@
/* run.config
+
+
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_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_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..0bf7aca76453ffff5cf74739bde1118eac196bbf 100644
--- a/tests/saveload/oracle/callbacks.res.oracle
+++ b/tests/saveload/oracle/callbacks.res.oracle
@@ -6,9 +6,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 +18,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 +34,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 +61,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 +73,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 +89,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_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_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_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_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..255dc1f7524e884b8e2530caba64511f385ec796 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,4 +1,6 @@
/* run.config*
+
+
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..bfa764fe30d810fe6bd68569c909c866b52dbaaa 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,4 +1,6 @@
/* run.config
+
+
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}"