[Eva] Updates test oracles.

tests/impact/depend5.i

 /* run.config
-   STDOPT: #"-calldeps -then -impact-pragma g"
+   STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-pragma g"
    */
 
 int a, b, c, d, e;

tests/impact/oracle/depend5.res.oracle

@@ -8,26 +8,28 @@
   c ∈ {0}
   d ∈ {0}
   e ∈ {0}
+[eva] computing for function f <- main.
+  Called from tests/impact/depend5.i:23.
+[eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
+[eva] Done for function f
+[eva] computing for function g <- main.
+  Called from tests/impact/depend5.i:25.
+[eva] computing for function f <- g <- main.
+  Called from tests/impact/depend5.i:18.
+[eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g
 [from] Computing for function g
 [from] Done for function g
+[eva] Done for function g
+[eva] Recording results for main
 [from] Computing for function main
 [from] Done for function main
 [eva] done for function main
-[eva:summary] ====== ANALYSIS SUMMARY ======
-  ----------------------------------------------------------------------------
-  3 functions analyzed (out of 3): 100% coverage.
-  In these functions, 13 statements reached (out of 13): 100% coverage.
-  ----------------------------------------------------------------------------
-  No errors or warnings raised during the analysis.
-  ----------------------------------------------------------------------------
-  0 alarms generated by the analysis.
-  ----------------------------------------------------------------------------
-  No logical properties have been reached by the analysis.
-  ----------------------------------------------------------------------------
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
 [from] call to f at tests/impact/depend5.i:18 (by g):
   b FROM a; e

tests/journal/oracle/control2.res.oracle

@@ -7,13 +7,11 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] tests/journal/control2.c:12: starting to merge loop iterations
-[eva:alarm] tests/journal/control2.c:15: Warning: 
-  signed overflow. assert x + 1 ≤ 2147483647;
+[eva:loop-unroll] tests/journal/control2.c:12: Automatic loop unrolling.
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  x ∈ [0..2147483647]
+  x ∈ {4}
   i ∈ {4}
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
@@ -22,8 +20,7 @@
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
-  1 alarm generated by the analysis:
-       1 integer overflow
+  0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
@@ -46,7 +43,7 @@
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  x ∈ [--..--]
+  x ∈ [-2147483644..2147483647]
   y ∈ [--..--]
   i ∈ {4}
 [eva:summary] ====== ANALYSIS SUMMARY ======

tests/journal/oracle/control2_sav.res

@@ -7,13 +7,11 @@
   y ∈ {0}
   c ∈ {0}
   d ∈ {0}
-[eva] tests/journal/control2.c:12: starting to merge loop iterations
-[eva:alarm] tests/journal/control2.c:15: Warning: 
-  signed overflow. assert x + 1 ≤ 2147483647;
+[eva:loop-unroll] tests/journal/control2.c:12: Automatic loop unrolling.
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  x ∈ [0..2147483647]
+  x ∈ {4}
   i ∈ {4}
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
@@ -22,8 +20,7 @@
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
-  1 alarm generated by the analysis:
-       1 integer overflow
+  0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
@@ -47,7 +44,7 @@
 [eva] done for function f
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  x ∈ [--..--]
+  x ∈ [-2147483644..2147483647]
   y ∈ [--..--]
   i ∈ {4}
 [eva:summary] ====== ANALYSIS SUMMARY ======

tests/journal/oracle/intra.res.oracle

@@ -36,8 +36,8 @@
 [eva] computing for function loop <- main.
   Called from tests/journal/intra.i:85.
 [eva] tests/journal/intra.i:63: assertion got status valid.
+[eva:loop-unroll] tests/journal/intra.i:66: Automatic loop unrolling.
 [eva] tests/journal/intra.i:64: loop invariant got status valid.
-[eva] tests/journal/intra.i:66: starting to merge loop iterations
 [eva] Recording results for loop
 [eva] Done for function loop
 [eva] computing for function assign <- main.

tests/syntax/oracle/Refresh_visitor.res.oracle

@@ -7,12 +7,12 @@ Start
   
 [eva:alarm] tests/syntax/Refresh_visitor.i:17: Warning: 
   assertion got status unknown.
+[eva:loop-unroll] tests/syntax/Refresh_visitor.i:26: Automatic loop unrolling.
 [eva] tests/syntax/Refresh_visitor.i:23: loop invariant got status valid.
 [eva] tests/syntax/Refresh_visitor.i:24: loop invariant got status valid.
+[eva:loop-unroll] tests/syntax/Refresh_visitor.i:32: Automatic loop unrolling.
 [eva] tests/syntax/Refresh_visitor.i:29: loop invariant got status valid.
 [eva] tests/syntax/Refresh_visitor.i:30: loop invariant got status valid.
-[eva] tests/syntax/Refresh_visitor.i:32: starting to merge loop iterations
-[eva] tests/syntax/Refresh_visitor.i:26: starting to merge loop iterations
 [eva:alarm] tests/syntax/Refresh_visitor.i:14: Warning: 
   function main: postcondition got status unknown.
 [eva] Recording results for main