From 37f9be961123e9644acd711de32d8ce2bd4adcac Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 13 Oct 2021 12:11:42 +0200
Subject: [PATCH] [Tests] using SCRIPT directives (oracle updates)
---
.../tests/report/oracle/single.0.res.oracle | 16 +++++++-------
.../tests/report/oracle/single.1.res.oracle | 20 ++++++++---------
.../tests/report/oracle/single.2.res.oracle | 22 +++++++++----------
.../oracle/unsupported_builtin.res.oracle | 8 +++----
tests/journal/oracle/control.0.res.oracle | 4 ++--
tests/journal/oracle/control.1.res.oracle | 6 ++---
tests/misc/oracle/global_decl_loc.res.oracle | 2 +-
tests/misc/oracle/global_decl_loc2.res.oracle | 2 +-
8 files changed, 40 insertions(+), 40 deletions(-)
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 64f57594d73..15553fd9a89 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 088835a7a67..4abf7a41c36 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 08bdf3a349c..2c350195d7e 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 0becba4e377..cc0edb5e06e 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 efd77d2456c..3342bdbd1e8 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 663abd350fa..eb59d625aff 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 ebeec539157..5a2c144cfb4 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 454d932e2db..c44f803bb27 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
--
GitLab