[Tests] using SCRIPT directives (oracle updates)

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).
 
 --------------------------------------------------------------------------------

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

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.
 

src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle

 # 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.

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

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

tests/misc/oracle/global_decl_loc.res.oracle

 [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

tests/misc/oracle/global_decl_loc2.res.oracle

 [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