diff --git a/src/plugins/report/tests/report/oracle/single.0.res.oracle b/src/plugins/report/tests/report/oracle/single.0.res.oracle
index 64f57594d7338549f7c58223a8bb7b7fc8adfddf..15553fd9a899bf3ed690f80208127b2f08387cde 100644
--- a/src/plugins/report/tests/report/oracle/single.0.res.oracle
+++ b/src/plugins/report/tests/report/oracle/single.0.res.oracle
@@ -6,7 +6,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -23,7 +23,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -39,7 +39,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -60,7 +60,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Bug ] Assertion (file tests/report/single.i, line 9)
+[ Bug ] Assertion (file tests/report/single.i, line 12)
by Test.
--------------------------------------------------------------------------------
@@ -76,7 +76,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -97,7 +97,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -113,7 +113,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test (v1).
--------------------------------------------------------------------------------
@@ -129,7 +129,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test (v2), Test (v1).
--------------------------------------------------------------------------------
diff --git a/src/plugins/report/tests/report/oracle/single.1.res.oracle b/src/plugins/report/tests/report/oracle/single.1.res.oracle
index 088835a7a6788b5f36665493ce3d57f1b512377b..4abf7a41c36e59b64a41786302d43797f49dd9ca 100644
--- a/src/plugins/report/tests/report/oracle/single.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/single.1.res.oracle
@@ -6,7 +6,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test.
--------------------------------------------------------------------------------
@@ -22,7 +22,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/report/single.i, line 9)
+[ Valid ] Assertion (file tests/report/single.i, line 12)
by Test.
--------------------------------------------------------------------------------
@@ -38,9 +38,9 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -55,9 +55,9 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -72,9 +72,9 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -89,9 +89,9 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
diff --git a/src/plugins/report/tests/report/oracle/single.2.res.oracle b/src/plugins/report/tests/report/oracle/single.2.res.oracle
index 08bdf3a349cd32576721e2ecfb66f20b0ee98378..2c350195d7e7a8a8232803e0e9839f307cc1cab0 100644
--- a/src/plugins/report/tests/report/oracle/single.2.res.oracle
+++ b/src/plugins/report/tests/report/oracle/single.2.res.oracle
@@ -11,7 +11,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/report/single.i, line 9)
+[ - ] Assertion (file tests/report/single.i, line 12)
tried with Test2, Test1.
--------------------------------------------------------------------------------
@@ -27,7 +27,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/report/single.i, line 9)
+[ Valid ] Assertion (file tests/report/single.i, line 12)
by Test1.
--------------------------------------------------------------------------------
@@ -43,7 +43,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/report/single.i, line 9)
+[ Valid ] Assertion (file tests/report/single.i, line 12)
by Test1.
by Test2.
@@ -62,9 +62,9 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test2, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -79,7 +79,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Bug ] Assertion (file tests/report/single.i, line 9)
+[ Bug ] Assertion (file tests/report/single.i, line 12)
by Test2.
--------------------------------------------------------------------------------
@@ -97,11 +97,11 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Alarm ] Assertion (file tests/report/single.i, line 9)
+[ Alarm ] Assertion (file tests/report/single.i, line 12)
By Test1, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
By Test2, with pending:
- - Unreachable program point (file tests/report/single.i, line 9)
+ - Unreachable program point (file tests/report/single.i, line 12)
--------------------------------------------------------------------------------
--- Status Report Summary
@@ -117,7 +117,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Bug ] Assertion (file tests/report/single.i, line 9)
+[ Bug ] Assertion (file tests/report/single.i, line 12)
by Test2.
--------------------------------------------------------------------------------
@@ -133,7 +133,7 @@
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Bug ] Assertion (file tests/report/single.i, line 9)
+[ Bug ] Assertion (file tests/report/single.i, line 12)
by Test1.
by Test2.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
index 0becba4e3779f4a17ec4a22b65cbde6ffa263a4b..cc0edb5e06ef6934f7c8820b9abf3247a751a011 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
@@ -1,17 +1,17 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/unsupported_builtin.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_acsl/unsupported_builtin.i:10: Warning:
+[kernel] tests/wp_acsl/unsupported_builtin.i:11: Warning:
No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/unsupported_builtin.i:7: Warning:
+[wp] tests/wp_acsl/unsupported_builtin.i:8: Warning:
Builtin unimplemented_builtin not defined
------------------------------------------------------------
Function main
------------------------------------------------------------
-Goal Assertion (file tests/wp_acsl/unsupported_builtin.i, line 12):
-tests/wp_acsl/unsupported_builtin.i:7: warning from wp:
+Goal Assertion (file tests/wp_acsl/unsupported_builtin.i, line 13):
+tests/wp_acsl/unsupported_builtin.i:8: warning from wp:
- Warning: Ignored Hypothesis
Reason: Builtin unimplemented_builtin not defined
Prove: true.
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index efd77d2456cfca6a462c6f6af540db2334a34f5b..3342bdbd1e8d0a630e3ed5f4dbef78429c01f86a 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] tests/journal/control.i:18: starting to merge loop iterations
-[eva:alarm] tests/journal/control.i:21: Warning:
+[eva] tests/journal/control.i:22: starting to merge loop iterations
+[eva:alarm] tests/journal/control.i:25: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 663abd350fa5fdc998e8857a64b6cdc201d4e121..eb59d625aff0307835c439c998ca70fcc440235c 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] tests/journal/control.i:18: starting to merge loop iterations
-[eva:alarm] tests/journal/control.i:21: Warning:
+[eva] tests/journal/control.i:22: starting to merge loop iterations
+[eva:alarm] tests/journal/control.i:25: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
@@ -44,7 +44,7 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva:alarm] tests/journal/control.i:21: Warning:
+[eva:alarm] tests/journal/control.i:25: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[from] Computing for function f
diff --git a/tests/misc/oracle/global_decl_loc.res.oracle b/tests/misc/oracle/global_decl_loc.res.oracle
index ebeec539157719888ba079dcd5f302761b592f79..5a2c144cfb4ee9dd8a5030ce97a9d2ba6ca238dd 100644
--- a/tests/misc/oracle/global_decl_loc.res.oracle
+++ b/tests/misc/oracle/global_decl_loc.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:7
diff --git a/tests/misc/oracle/global_decl_loc2.res.oracle b/tests/misc/oracle/global_decl_loc2.res.oracle
index 454d932e2db64309978664a32e711b64f34a109a..c44f803bb273b3f3321fe0565cf2de8dbd5de9e5 100644
--- a/tests/misc/oracle/global_decl_loc2.res.oracle
+++ b/tests/misc/oracle/global_decl_loc2.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:7