diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i index fcae6034c68e975b5cd0c0712356523269a25e33..52b560fbce0feb000e1bab6d409c7d022216c822 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 415d327aa48e2ce9f2a753cf94e0667a2ea0b345..f75abc0f8070015f2b9e02de9243b93be8905853 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 f73d56171f0db23c4055406812a7c19107de9100..5622bf1b88820c0b3fc3ce8623e7837e2b1c4c8c 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 cfefb7770292c8cb107c3032b830803c8191e095..2248303d571361f9b101d0c20dd5bd5f03961280 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 5e39a5c278bb9da6f9f575e1bfa755291fb626d9..20f13f6cd8582722bb37262113257eae826bad69 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 a23d419a768f500414b2008e8732e74b6104574a..58871cc596c7e7ec842f93dc4fd8f0964133875b 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