From d4f4058ec7dc21966574328c815dd9eaf3bc22ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 2 Aug 2019 14:19:29 +0200
Subject: [PATCH] [Eva] Updates test oracles.
---
tests/impact/depend5.i | 2 +-
tests/impact/oracle/depend5.res.oracle | 24 ++++++++++---------
tests/journal/oracle/control2.res.oracle | 11 ++++-----
tests/journal/oracle/control2_sav.res | 11 ++++-----
tests/journal/oracle/intra.res.oracle | 2 +-
.../syntax/oracle/Refresh_visitor.res.oracle | 4 ++--
6 files changed, 25 insertions(+), 29 deletions(-)
diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i
index fcae6034c68..52b560fbce0 100644
--- a/tests/impact/depend5.i
+++ b/tests/impact/depend5.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-calldeps -then -impact-pragma g"
+ STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-pragma g"
*/
int a, b, c, d, e;
diff --git a/tests/impact/oracle/depend5.res.oracle b/tests/impact/oracle/depend5.res.oracle
index 415d327aa48..f75abc0f807 100644
--- a/tests/impact/oracle/depend5.res.oracle
+++ b/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
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index f73d56171f0..5622bf1b888 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/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 ======
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index cfefb777029..2248303d571 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/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 ======
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 5e39a5c278b..20f13f6cd85 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/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.
diff --git a/tests/syntax/oracle/Refresh_visitor.res.oracle b/tests/syntax/oracle/Refresh_visitor.res.oracle
index a23d419a768..58871cc596c 100644
--- a/tests/syntax/oracle/Refresh_visitor.res.oracle
+++ b/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
--
GitLab