From febed78113f546a5ed08355fd0f2e0f5106828b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Apr 2019 11:19:10 +0200
Subject: [PATCH] [Eva] Updates test oracles with the analysis summary.
---
.../oracle/with_value.res.oracle | 12 ++++++
.../report/tests/report/oracle/csv.res.oracle | 40 +++++++++++++++++++
.../tests/wp_acsl/oracle/checks.0.res.oracle | 14 +++++++
...iter_over_unregistered_function.res.oracle | 13 ++++++
.../oracle/no_fp_unsound_warning.0.res.oracle | 11 +++++
.../oracle/no_fp_unsound_warning.1.res.oracle | 11 +++++
tests/idct/oracle/ieee_1180_1990.res.oracle | 18 +++++++++
tests/impact/oracle/depend5.res.oracle | 11 +++++
tests/journal/oracle/control.0.res.oracle | 12 ++++++
tests/journal/oracle/control.1.res.oracle | 26 ++++++++++++
tests/journal/oracle/control2.res.oracle | 24 +++++++++++
tests/journal/oracle/control2_sav.res | 26 ++++++++++++
tests/journal/oracle/intra.res.oracle | 16 ++++++++
tests/metrics/oracle/func_ptr.0.res.oracle | 13 ++++++
tests/metrics/oracle/func_ptr.1.res.oracle | 13 ++++++
tests/metrics/oracle/libc.0.res.oracle | 14 +++++++
tests/metrics/oracle/libc.1.res.oracle | 14 +++++++
tests/metrics/oracle/reach.res.oracle | 11 +++++
tests/metrics/oracle/unreachable.res.oracle | 22 ++++++++++
tests/misc/oracle/bts1201.res.oracle | 28 +++++++++++++
tests/misc/oracle/change_main.res.oracle | 22 ++++++++++
tests/misc/oracle/ensures.res.oracle | 11 +++++
tests/misc/oracle/well_typed_alarm.res.oracle | 11 +++++
tests/saveload/oracle/basic_sav.1.res | 15 +++++++
tests/saveload/oracle/basic_sav.res | 15 +++++++
tests/saveload/oracle/bool_sav.res | 15 +++++++
tests/saveload/oracle/callbacks_initial.res | 11 +++++
tests/saveload/oracle/deps_sav.res | 12 ++++++
.../oracle/multi_project.1.res.oracle | 14 +++++++
tests/saveload/oracle/multi_project_sav.res | 14 +++++++
.../oracle/segfault_datatypes_sav.res | 12 ++++++
tests/saveload/oracle/sparecode_sav.res | 11 +++++
.../oracle/default_assigns_bts0966.res.oracle | 13 ++++++
tests/spec/oracle/logic_def.res.oracle | 14 +++++++
tests/syntax/oracle/copy_logic.res.oracle | 15 +++++++
.../loop-case-switch-for-unroll.0.res.oracle | 11 +++++
.../loop-case-switch-for-unroll.1.res.oracle | 11 +++++
.../loop-case-switch-for-unroll.2.res.oracle | 11 +++++
.../value/numerors/oracle/numerors.res.oracle | 16 ++++++++
39 files changed, 603 insertions(+)
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 504e31673b1..2532c0705de 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 639393b8a5a..aaf1752f36f 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 a99ec33e26d..bae891952be 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 912046cbc68..f2b3a6b7386 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 f92e8ed4637..302afc81d0d 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 4f2c24befe2..69a91fb9cf5 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 701da61a7a2..a0c2c414fd9 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 8ebb3a55b25..415d327aa48 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 a04a28a513c..2ee981ccf35 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 0d4cd66ed39..55c6fcda9b2 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 65f6972933b..f73d56171f0 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 3f2f015507e..cfefb777029 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 e2f814d04a5..5e39a5c278b 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 9ad14445a92..42898601069 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 e5937b139f6..70341559591 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 3cff2f1a191..76a9cd7cd79 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 4f1b84793b0..890b92c6ed6 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 3bf756a5a54..e568528660b 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 ac7dad1c8c1..f542548237b 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 1f86ad9db0e..bf9968e480c 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 6b17595c9d5..b8d9d6fde81 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 7acf87d6161..ee0832cdeff 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 3ba7b848d76..cff9cdaaa88 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 05605960620..d2c84cb5472 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 05605960620..d2c84cb5472 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 91b80def8d2..42cfadd177d 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 7ae40acf192..25b036ba641 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 40f9aeda114..c52779de1ee 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 1cd5eaed301..1ca91d86729 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 c6cb667f227..6968a8ec6be 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 a67d19e53c3..1cf0a3182aa 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 87fe698cd5e..f1ac9d2f24d 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 7fb0bd7fa36..525ec649aff 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 068ba78e31d..a363bbc1f4a 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 30b1c2e6d09..654c5e3a503 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 3d21e2b5379..4407cbebb99 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 92842431056..ccd8dec4937 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 817e4bba618..f029ae31917 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 ed54ec83da0..b6bde3cbebb 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.
+ ----------------------------------------------------------------------------
--
GitLab