From 0d8e028c3126df5235fead6744b943597a5d6fec Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 25 Jan 2022 10:53:16 +0100
Subject: [PATCH] [tests] prepare test configs for deletion of spurious
warnings
---
tests/journal/control.i | 2 ++
tests/journal/control2.c | 2 ++
tests/journal/intra.i | 2 ++
tests/journal/oracle/control.0.res.oracle | 4 +--
tests/journal/oracle/control.1.res.oracle | 6 ++--
tests/journal/oracle/control2.res.oracle | 10 +++---
tests/journal/oracle/control2_sav.res | 10 +++---
tests/journal/oracle/intra.res.oracle | 30 ++++++++---------
tests/misc/my_visitor.c | 2 ++
tests/saveload/basic.i | 2 ++
tests/saveload/bool.c | 2 ++
tests/saveload/callbacks.i | 2 ++
tests/saveload/deps.i | 2 ++
tests/saveload/isset.c | 2 ++
tests/saveload/oracle/basic_sav.1.res | 6 ++--
tests/saveload/oracle/basic_sav.res | 6 ++--
tests/saveload/oracle/bool_sav.res | 28 ++++++++--------
tests/saveload/oracle/callbacks.res.oracle | 32 +++++++++----------
tests/saveload/oracle/callbacks_sav.res | 16 +++++-----
tests/saveload/oracle/deps_sav.res | 4 +--
tests/saveload/oracle/isset_sav.res | 2 +-
.../oracle/segfault_datatypes_sav.res | 4 +--
tests/saveload/oracle/sparecode_sav.res | 6 ++--
tests/saveload/segfault_datatypes.i | 2 ++
tests/saveload/sparecode.i | 2 ++
25 files changed, 104 insertions(+), 82 deletions(-)
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 092afe2d239..2e38a7853a6 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 885d7f07b81..7145f20651c 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 f19b1d606e2..b7fe01ce6b4 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 f97cd8e9daf..142ca471781 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 0f89b91f804..9851832dccb 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 acf4746fb0c..02360dafcbc 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 2a9246db51c..1734f9bb537 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 1d0c56f4f1d..610bcea9ef3 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 da957b1c8e1..3fe0b7d9092 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 338816e01c2..00a166d2bc6 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 b6b40e89402..28424151adb 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 31a79ab6d68..fb98f59a3f4 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 f52f1606186..3e27bf10e2c 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 9e8eb7af862..9f0dcb12063 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 2d8d381c7cb..8e9fab39005 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 2d8d381c7cb..8e9fab39005 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 7a24197dd13..b05786274e0 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 ae9563d2b2b..0bf7aca7645 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 9e942d99e7f..294a67f3fe5 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 103d5a3540d..516b5aaa9c3 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 f2693a09a70..6c37866d487 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 3aece07549b..773e46ed9de 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 36b458ce885..7f7224a9258 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 7cba664a76f..255dc1f7524 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 b1e13d655e3..bfa764fe30d 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}"
--
GitLab