diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
index 504e31673b11bfc0d47a0708faa9b08494ca9d5c..2532c0705debdae0c04bd3b145d657e2f7699ac2 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
@@ -412,6 +412,18 @@
i ∈ {-154}
[eva:final-states] Values at end of function main:
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 46 functions analyzed (out of 46): 100% coverage.
+ In these functions, 329 statements reached (out of 329): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 22 alarms generated by the analysis:
+ 22 integer overflows
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[loop] Functions with loops whose bounds we could not find:
g1
g2
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index 639393b8a5af4fca82b1c0e8bdd05cbf4a74a955..aaf1752f36f4d2a5614f9f35f6bd27d7e986d277 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -67,6 +67,26 @@
r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 23 statements reached (out of 23): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 7 alarms generated by the analysis:
+ 2 accesses out of bounds index
+ 2 integer overflows
+ 2 accesses to uninitialized left-values
+ 1 nan or infinite floating-point value
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 4 unknown 1 invalid 7 total
+ 28% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[report] Dumping properties in 'tests/report/result/csv.csv'
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -152,3 +172,23 @@
r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 23 statements reached (out of 23): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 7 alarms generated by the analysis:
+ 2 accesses out of bounds index
+ 2 integer overflows
+ 2 accesses to uninitialized left-values
+ 1 nan or infinite floating-point value
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 4 unknown 1 invalid 7 total
+ 28% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
index a99ec33e26d36787a9fc88e173e145acb5ac2b4a..bae891952be7ca996280d35951a229bd1336993e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -42,6 +42,20 @@ Prove: true.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 4 unknown 0 invalid 4 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Global Properties
diff --git a/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle b/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
index 912046cbc683279ca4b87d64509e674f76e1ac4b..f2b3a6b73869d6056238fbd7bb1d8b664c3957b1 100644
--- a/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
+++ b/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
@@ -9,6 +9,19 @@
[eva] done for function main
[eva] tests/callgraph/issue_55_iter_over_unregistered_function.i:12:
assertion 'Eva,initialization' got final status invalid.
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 3): 33% coverage.
+ In this function, 1 statements reached (out of 3): 33% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ 1 of them is a sure alarm (invalid status).
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[inout] InOut (internal) for function main:
Operational inputs:
q
diff --git a/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle b/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
index f92e8ed4637457992e96534d767763525ad2623b..302afc81d0db9b556b86b10ca214cc82f795ee26 100644
--- a/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
+++ b/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
@@ -5,5 +5,16 @@
[eva:initial-state] Values of globals at initialization
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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.
+ ----------------------------------------------------------------------------
[inout] Out (internal) for function main:
\nothing
diff --git a/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle b/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
index 4f2c24befe204e6d5d21b74ab9455631cc1c0e17..69a91fb9cf5e48c751f375293aaea9e2cd52ce47 100644
--- a/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
+++ b/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
@@ -5,6 +5,17 @@
[eva:initial-state] Values of globals at initialization
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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.
+ ----------------------------------------------------------------------------
[cg] Warning: using callgraph while option -cg-function-pointers is unset, result may be unsound
[inout] Out (internal) for function main:
\nothing
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 701da61a7a281513ca4425510286d513f568e803..a0c2c414fd9f4785327dea18761f3ff05f3f9fa8 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -971,6 +971,24 @@
idct_mc2[0..7][0..7] ∈ [-8192..8192]
__retres ∈ {0; 1}
S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 6 functions analyzed (out of 44): 13% coverage.
+ In these functions, 588 statements reached (out of 626): 93% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 42 warnings
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 72 alarms generated by the analysis:
+ 64 accesses to uninitialized left-values
+ 8 illegal conversions from floating-point to integer
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 11 valid 0 unknown 0 invalid 11 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[from] Computing for function IEEE_1180_1990_rand
[from] Done for function IEEE_1180_1990_rand
[from] Computing for function IEEE_1180_1990_mkbk
diff --git a/tests/impact/oracle/depend5.res.oracle b/tests/impact/oracle/depend5.res.oracle
index 8ebb3a55b259b013d269dc286549ddc1a47a1fdc..415d327aa48e2ce9f2a753cf94e0667a2ea0b345 100644
--- a/tests/impact/oracle/depend5.res.oracle
+++ b/tests/impact/oracle/depend5.res.oracle
@@ -17,6 +17,17 @@
[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/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index a04a28a513c7a7a17daa9e0a36f3b9daa84f2e59..2ee981ccf351c5624f462d99bd30b24696a4e799 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -16,6 +16,18 @@
[eva:final-states] Values at end of function f:
x ∈ [0..2147483647]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 4): 25% coverage.
+ In this function, 9 statements reached (out of 12): 75% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 0d4cd66ed390271e928405b836d12f8bdb684395..55c6fcda9b26c40ee167dcf8563665b5dd72ab26 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -16,6 +16,18 @@
[eva:final-states] Values at end of function f:
x ∈ [0..2147483647]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 4): 25% coverage.
+ In this function, 9 statements reached (out of 12): 75% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
@@ -42,6 +54,20 @@
[eva:final-states] Values at end of function f:
x ∈ [0..2147483647]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 4): 25% coverage.
+ In this function, 9 statements reached (out of 12): 75% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] entry point:
x FROM x (and SELF)
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index 65f6972933b6d55079a46623f905c5dd4781c67d..f73d56171f0db23c4055406812a7c19107de9100 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -15,6 +15,18 @@
[eva:final-states] Values at end of function f:
x ∈ [0..2147483647]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 4): 25% coverage.
+ In this function, 9 statements reached (out of 12): 75% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[eva] Analyzing an incomplete application starting at f
@@ -37,6 +49,18 @@
x ∈ [--..--]
y ∈ [--..--]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 3 alarms generated by the analysis:
+ 3 integer overflows
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index 3f2f015507ecaba23d749a4b1a96195a1b714ff6..cfefb7770292c8cb107c3032b830803c8191e095 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -15,6 +15,18 @@
[eva:final-states] Values at end of function f:
x ∈ [0..2147483647]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 4): 25% coverage.
+ In this function, 9 statements reached (out of 12): 75% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
@@ -38,6 +50,20 @@
x ∈ [--..--]
y ∈ [--..--]
i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 3 alarms generated by the analysis:
+ 3 integer overflows
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function f
[from] Done for function f
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index e2f814d04a544f8528f553003c53056efcf76aaa..5e39a5c278bb9da6f9f575e1bfa755291fb626d9 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -56,6 +56,22 @@
[eva] Done for function stop
[eva] Recording results for main
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 8 functions analyzed (out of 9): 88% coverage.
+ In these functions, 58 statements reached (out of 59): 98% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 6 valid 0 unknown 0 invalid 6 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[pdg] computing for function main
[from] Computing for function param
[from] Done for function param
diff --git a/tests/metrics/oracle/func_ptr.0.res.oracle b/tests/metrics/oracle/func_ptr.0.res.oracle
index 9ad14445a9209e71ea101cea19402366ef688035..428986010691df4429d28efc6da6ca2e449b53bb 100644
--- a/tests/metrics/oracle/func_ptr.0.res.oracle
+++ b/tests/metrics/oracle/func_ptr.0.res.oracle
@@ -46,6 +46,19 @@
bar ∈ {0}
bar_extern ∈ {0}
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 8): 12% coverage.
+ In this function, 6 statements reached (out of 13): 46% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 3 (out of 5)
diff --git a/tests/metrics/oracle/func_ptr.1.res.oracle b/tests/metrics/oracle/func_ptr.1.res.oracle
index e5937b139f68d51c065640b27c4fa32d8d6982b6..703415595918a67d1441bee0b6d26d1cef1dddd4 100644
--- a/tests/metrics/oracle/func_ptr.1.res.oracle
+++ b/tests/metrics/oracle/func_ptr.1.res.oracle
@@ -46,6 +46,19 @@
bar ∈ {0}
bar_extern ∈ {0}
[eva] done for function foobar
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 5)
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index 3cff2f1a191389113a805b4da2240e279a026555..76a9cd7cd795af18278d1e949a4e6407dcbec6a9 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -38,6 +38,20 @@
[eva] using specification for function isalpha
[eva] using specification for function isblank
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 0 unknown 0 invalid 2 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 4 (out of 5)
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 4f1b84793b0cdddb3255ee72a288a2185f1122be..890b92c6ed6f4576aded31faf97765ab72a9cf68 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -56,6 +56,20 @@
[eva] using specification for function isalpha
[eva] using specification for function isblank
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 0 unknown 0 invalid 2 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 7 (out of 76)
diff --git a/tests/metrics/oracle/reach.res.oracle b/tests/metrics/oracle/reach.res.oracle
index 3bf756a5a54dd8ce98852cfbd896521f5e130ca5..e568528660bde94fa24656908310b1b9822a4dd9 100644
--- a/tests/metrics/oracle/reach.res.oracle
+++ b/tests/metrics/oracle/reach.res.oracle
@@ -83,6 +83,17 @@
t[0] ∈ {{ &baz }}
[1] ∈ {0}
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 6): 16% coverage.
+ In this function, 7 statements reached (out of 12): 58% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 3 (out of 3)
diff --git a/tests/metrics/oracle/unreachable.res.oracle b/tests/metrics/oracle/unreachable.res.oracle
index ac7dad1c8c1d4676a07e7ceefbb6a82e01282460..f542548237b0d0a7f7567f3951bbb2da54de561c 100644
--- a/tests/metrics/oracle/unreachable.res.oracle
+++ b/tests/metrics/oracle/unreachable.res.oracle
@@ -35,6 +35,17 @@
[eva:initial-state] Values of globals at initialization
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 5): 20% coverage.
+ In this function, 6 statements reached (out of 10): 60% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 2)
@@ -56,6 +67,17 @@
[eva:initial-state] Values of globals at initialization
[eva] done for function foo
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 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.
+ ----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 2)
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index 1f86ad9db0ec5a63a16f794d0d3aff8ccf38e9bc..bf9968e480cc7fb94343c74c0e71eb5a44bef38d 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -6,12 +6,40 @@
[eva] tests/misc/bts1201.i:5: assertion got status valid.
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main2
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] done for function main2
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
void main(void)
{
diff --git a/tests/misc/oracle/change_main.res.oracle b/tests/misc/oracle/change_main.res.oracle
index 6b17595c9d5a78fb1d6dbf5ac62bb7de4d92dbeb..b8d9d6fde811d0da2effd143924adadba3783044 100644
--- a/tests/misc/oracle/change_main.res.oracle
+++ b/tests/misc/oracle/change_main.res.oracle
@@ -8,6 +8,17 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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.
+ ----------------------------------------------------------------------------
[eva] Analyzing a complete application starting at g
[eva] Computing initial state
[eva] Initial state computed
@@ -17,3 +28,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function g:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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.
+ ----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index 7acf87d61616ae7b517495ee6013e35bbdeaf2a7..ee0832cdeffc1cc003c4ae54db0a7947af527c57 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -7,6 +7,17 @@
[eva:alarm] tests/misc/ensures.i:5: Warning:
function main: postcondition got status invalid.
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 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.
+ ----------------------------------------------------------------------------
[kernel] main: behavior default!
**NOT** VALID according to Frama-C kernel (under hypotheses)
[kernel] main: behavior default! **NOT** VALID according to Eva (under hypotheses)
diff --git a/tests/misc/oracle/well_typed_alarm.res.oracle b/tests/misc/oracle/well_typed_alarm.res.oracle
index 3ba7b848d7601547c3df402938180028ebd6fe61..cff9cdaaa88971d0ae07d576c88835d8e353efe0 100644
--- a/tests/misc/oracle/well_typed_alarm.res.oracle
+++ b/tests/misc/oracle/well_typed_alarm.res.oracle
@@ -7,6 +7,17 @@
[eva:alarm] tests/misc/well_typed_alarm.i:11: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 10 statements reached (out of 10): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
int main(int c)
{
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index 056059606204259f47c4619d6aa71f6dd14adaa0..d2c84cb5472a81605ccd30aad3736fefb3012431 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -15,6 +15,21 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index 056059606204259f47c4619d6aa71f6dd14adaa0..d2c84cb5472a81605ccd30aad3736fefb3012431 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -15,6 +15,21 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 91b80def8d2d6316bebfd69690759d3c1442a3d0..42cfadd177d9795b61e0ab5ef909a7f2ab78dc5c 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -54,3 +54,18 @@
x ∈ {1}
y ∈ {2}
S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 24 statements reached (out of 24): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 5 valid 0 unknown 0 invalid 5 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/saveload/oracle/callbacks_initial.res b/tests/saveload/oracle/callbacks_initial.res
index 7ae40acf1929984ee3ad46dcc680ee34749f64a8..25b036ba64125f63b83322c481bbdb8145af540e 100644
--- a/tests/saveload/oracle/callbacks_initial.res
+++ b/tests/saveload/oracle/callbacks_initial.res
@@ -33,6 +33,17 @@
[from] Computing for function main1
[from] Done for function main1
[eva] done for function main1
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 9 statements reached (out of 9): 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/saveload/callbacks.i:16 (by g1):
x FROM p
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 40f9aeda11453a63ab6d1a1c2a1b0b9083ec2cbe..c52779de1ee27f18ae17e8ab60348d97820dbefe 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -14,6 +14,18 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 11 statements reached (out of 11): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/multi_project.1.res.oracle b/tests/saveload/oracle/multi_project.1.res.oracle
index 1cd5eaed301e7605d863fc6f45aa6e8ca1326a5a..1ca91d867296f076e2a0a71a83f86eddebc8b32a 100644
--- a/tests/saveload/oracle/multi_project.1.res.oracle
+++ b/tests/saveload/oracle/multi_project.1.res.oracle
@@ -18,6 +18,20 @@
x ∈ {2}
y ∈ {4}
__retres ∈ {8}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 7 statements reached (out of 7): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
[kernel] Checking "foo"
[kernel] Checking "foobar"
[kernel] Checking "default"
diff --git a/tests/saveload/oracle/multi_project_sav.res b/tests/saveload/oracle/multi_project_sav.res
index c6cb667f22790752799c6073a046dd5a4f4d07a2..6968a8ec6bec3d45c4bafa4c62f29beab29467df 100644
--- a/tests/saveload/oracle/multi_project_sav.res
+++ b/tests/saveload/oracle/multi_project_sav.res
@@ -12,6 +12,20 @@
[eva] tests/saveload/multi_project.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 7 statements reached (out of 7): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
int f(int x)
{
diff --git a/tests/saveload/oracle/segfault_datatypes_sav.res b/tests/saveload/oracle/segfault_datatypes_sav.res
index a67d19e53c35d8b2b99e4d14186c88dd929a4f51..1cf0a3182aa799855b6b8135f9bfc4bcc08f6746 100644
--- a/tests/saveload/oracle/segfault_datatypes_sav.res
+++ b/tests/saveload/oracle/segfault_datatypes_sav.res
@@ -14,6 +14,18 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 11 statements reached (out of 11): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/sparecode_sav.res b/tests/saveload/oracle/sparecode_sav.res
index 87fe698cd5e96a4e76080db43d43fb7c6b43d9f1..f1ac9d2f24dc8133113b67db5feb21a631f000bc 100644
--- a/tests/saveload/oracle/sparecode_sav.res
+++ b/tests/saveload/oracle/sparecode_sav.res
@@ -19,6 +19,17 @@
[eva] Done for function f
[eva] Recording results for main
[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 9 statements reached (out of 9): 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.
+ ----------------------------------------------------------------------------
[slicing] initializing slicing ...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function main
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 7fb0bd7fa3693bab1e859ba911eec5c6cbd8f579..525ec649affa3ac23429cd1408acd16667082f02 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -16,6 +16,19 @@
[1] ∈ {1}
[2..3] ∈ {0}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 7 statements reached (out of 7): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
enum states {
Init = 0,
diff --git a/tests/spec/oracle/logic_def.res.oracle b/tests/spec/oracle/logic_def.res.oracle
index 068ba78e31da714037077c5f602d3cb9fb8b6b1e..a363bbc1f4af37ee378a86e65f0e6c8f3e4b4134 100644
--- a/tests/spec/oracle/logic_def.res.oracle
+++ b/tests/spec/oracle/logic_def.res.oracle
@@ -10,6 +10,20 @@
[eva:final-states] Values at end of function main:
x ∈ {42}
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
/*@ logic ℤ foo(int x) = x + 2;
*/
diff --git a/tests/syntax/oracle/copy_logic.res.oracle b/tests/syntax/oracle/copy_logic.res.oracle
index 30b1c2e6d09c3740020ab25e56bddbea1a9d455d..654c5e3a503a0e2bb24d6a9d131b3ac87b6f57ad 100644
--- a/tests/syntax/oracle/copy_logic.res.oracle
+++ b/tests/syntax/oracle/copy_logic.res.oracle
@@ -19,6 +19,21 @@
[eva:final-states] Values at end of function main:
y ∈ [-2147483606..2147483647]
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 6 statements reached (out of 6): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 2 unknown 0 invalid 2 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
/*@ predicate p(int x) ;
*/
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
index 3d21e2b53792ea9a3ed56da9ff3f57ac6e8046dc..4407cbebb995be38963c081af07126d4ee7385ce 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
@@ -112,6 +112,17 @@
x ∈ {32}
n ∈ {0}
gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 5): 40% coverage.
+ In these functions, 45 statements reached (out of 48): 93% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
int gen_nondet(int line);
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
index 9284243105698190efe952fd6994c375a159a1f3..ccd8dec4937e12ce19a03bca5e7be6379d4cb91c 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
@@ -112,6 +112,17 @@
x ∈ {32}
n ∈ {0}
gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 52): 3% coverage.
+ In these functions, 75 statements reached (out of 125): 60% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
int gen_nondet(int line);
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
index 817e4bba61835baf1760948d7bd0dd08d16de0f0..f029ae319170bc1e849e524390a368aca68a6c87 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
@@ -112,6 +112,17 @@
x ∈ {32}
n ∈ {0}
gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 166): 1% coverage.
+ In these functions, 74 statements reached (out of 238): 31% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
/* Generated by Frama-C */
int gen_nondet(int line);
diff --git a/tests/value/numerors/oracle/numerors.res.oracle b/tests/value/numerors/oracle/numerors.res.oracle
index ed54ec83da044cbae19d8b23fe57d391f51ae626..b6bde3cbebb23d7897c74e3661ee2ec094742a7a 100644
--- a/tests/value/numerors/oracle/numerors.res.oracle
+++ b/tests/value/numerors/oracle/numerors.res.oracle
@@ -292,3 +292,19 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 29 functions analyzed (out of 29): 100% coverage.
+ In these functions, 257 statements reached (out of 257): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 3 warnings
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 146 valid 0 unknown 0 invalid 146 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------