diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 4ec633c711ce24d107fbb2ec27359d5bf788f63a..4363193a1b51f6a8de4275dde0e0a23aa1f4434e 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -368,30 +368,32 @@ let consider_function vi =
|| Cil.hasAttribute "fc_stdlib_generated" vi.vattr)
let print_coverage fmt =
- let ignored, analyzed = ref 0, ref 0
- and dead, reachable = ref 0, ref 0 in
- let is_reachable = Db.Value.is_reachable_stmt in
- let do_stmt stmt = incr (if is_reachable stmt then reachable else dead) in
+ let dead_function, reachable_function = ref 0, ref 0
+ and dead_stmt, reachable_stmt = ref 0, ref 0 in
+ let do_stmt stmt =
+ incr (if Db.Value.is_reachable_stmt stmt then reachable_stmt else dead_stmt)
+ in
let visit fundec =
if consider_function fundec.svar then
if is_called (Globals.Functions.get fundec.svar)
- then (incr analyzed; List.iter do_stmt fundec.sallstmts)
- else incr ignored
+ then (incr reachable_function; List.iter do_stmt fundec.sallstmts)
+ else incr dead_function
in
Globals.Functions.iter_on_fundecs visit;
- let all = !dead + !analyzed in
- if all = 0
+ let total_function = !dead_function + !reachable_function in
+ if total_function = 0
then Format.fprintf fmt "No function to be analyzed.@;"
else
Format.fprintf fmt
"%i function%s analyzed (out of %i): %i%% coverage.@;"
- !analyzed (plural !analyzed) all (!analyzed * 100 / all);
- let total = !dead + !reachable in
- if !analyzed > 0 && total > 0 then
+ !reachable_function (plural !reachable_function) total_function
+ (!reachable_function * 100 / total_function);
+ let total_stmt = !dead_stmt + !reachable_stmt in
+ if !reachable_function > 0 && total_stmt > 0 then
Format.fprintf fmt
"In %s, %i statements reached (out of %i): %i%% coverage.@;"
- (if !analyzed > 1 then "these functions" else "this function")
- !reachable total (!reachable * 100 / total)
+ (if !reachable_function > 1 then "these functions" else "this function")
+ !reachable_stmt total_stmt (!reachable_stmt * 100 / total_stmt)
let print_warning fmt =
let eva_warnings, eva_errors = ref 0, ref 0
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 f2b3a6b73869d6056238fbd7bb1d8b664c3957b1..2efdf3909b39756e6eb8ab9986733941c1167363 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
@@ -11,7 +11,7 @@
assertion 'Eva,initialization' got final status invalid.
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 3): 33% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 1 statements reached (out of 3): 33% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index ace1c0568b9fc422d31f7bfa9b341f94f18c509d..56319e5d1845473862f9cb775b4515dc3ab93f09 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -973,7 +973,7 @@
S___fc_stdout[0..1] ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 6 functions analyzed (out of 44): 13% coverage.
+ 6 functions analyzed (out of 6): 100% coverage.
In these functions, 588 statements reached (out of 626): 93% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index 2ee981ccf351c5624f462d99bd30b24696a4e799..efd77d2456cfca6a462c6f6af540db2334a34f5b 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -18,7 +18,7 @@
i ∈ {4}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 55c6fcda9b26c40ee167dcf8563665b5dd72ab26..663abd350fa5fdc998e8857a64b6cdc201d4e121 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -18,7 +18,7 @@
i ∈ {4}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
@@ -56,7 +56,7 @@
i ∈ {4}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index f73d56171f0db23c4055406812a7c19107de9100..04f5cc28cae629f77dab9116a4785e1910491f0e 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -17,7 +17,7 @@
i ∈ {4}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index cfefb7770292c8cb107c3032b830803c8191e095..234e16239cc482d48773b401746dffd334303ca7 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -17,7 +17,7 @@
i ∈ {4}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 5e39a5c278bb9da6f9f575e1bfa755291fb626d9..9032dd6f7aef8be7a8e414890d3e99b037adf17d 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -58,7 +58,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 8 functions analyzed (out of 9): 88% coverage.
+ 8 functions analyzed (out of 10): 80% coverage.
In these functions, 58 statements reached (out of 59): 98% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
diff --git a/tests/metrics/oracle/func_ptr.0.res.oracle b/tests/metrics/oracle/func_ptr.0.res.oracle
index 428986010691df4429d28efc6da6ca2e449b53bb..0a380c923213a518b44cc5ab6df690031a0bcdcb 100644
--- a/tests/metrics/oracle/func_ptr.0.res.oracle
+++ b/tests/metrics/oracle/func_ptr.0.res.oracle
@@ -48,7 +48,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 8): 12% coverage.
+ 1 function analyzed (out of 4): 25% coverage.
In this function, 6 statements reached (out of 13): 46% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
diff --git a/tests/metrics/oracle/func_ptr.1.res.oracle b/tests/metrics/oracle/func_ptr.1.res.oracle
index 703415595918a67d1441bee0b6d26d1cef1dddd4..b44df54a2fe98e9eaaf8914d44887efdcafcf7d7 100644
--- a/tests/metrics/oracle/func_ptr.1.res.oracle
+++ b/tests/metrics/oracle/func_ptr.1.res.oracle
@@ -48,7 +48,7 @@
[eva] done for function foobar
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
+ 2 functions analyzed (out of 4): 50% coverage.
In these functions, 5 statements reached (out of 5): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index 76a9cd7cd795af18278d1e949a4e6407dcbec6a9..c3bb5a741d5ae3a77120a0d2459ee3498e48cef0 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -40,7 +40,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 4 functions analyzed (out of 4): 100% coverage.
+ 4 functions analyzed (out of 5): 80% coverage.
In these functions, 10 statements reached (out of 10): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 8c8f0e6b9987c0efcc1d96fb117a3d40096d755c..eca3c4a7d227c3204cc015581c99570d60fa0430 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -73,7 +73,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 4 functions analyzed (out of 4): 100% coverage.
+ 4 functions analyzed (out of 5): 80% coverage.
In these functions, 10 statements reached (out of 10): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/metrics/oracle/reach.res.oracle b/tests/metrics/oracle/reach.res.oracle
index e568528660bde94fa24656908310b1b9822a4dd9..76558191ccef8ba929bce7f1571de2c98c5c21f7 100644
--- a/tests/metrics/oracle/reach.res.oracle
+++ b/tests/metrics/oracle/reach.res.oracle
@@ -85,7 +85,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 6): 16% coverage.
+ 1 function analyzed (out of 3): 33% coverage.
In this function, 7 statements reached (out of 12): 58% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/metrics/oracle/unreachable.res.oracle b/tests/metrics/oracle/unreachable.res.oracle
index f542548237b0d0a7f7567f3951bbb2da54de561c..38770a200d191a2cfe6964fe6a343e78ba57eef8 100644
--- a/tests/metrics/oracle/unreachable.res.oracle
+++ b/tests/metrics/oracle/unreachable.res.oracle
@@ -37,7 +37,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 5): 20% coverage.
+ 1 function analyzed (out of 2): 50% coverage.
In this function, 6 statements reached (out of 10): 60% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
@@ -69,7 +69,7 @@
[eva] done for function foo
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
+ 1 function analyzed (out of 2): 50% coverage.
In this function, 2 statements reached (out of 2): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index bf9968e480cc7fb94343c74c0e71eb5a44bef38d..b15cb77c71ad3712d598439a18afb2b5be94afb6 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -8,7 +8,7 @@
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
+ 1 function analyzed (out of 2): 50% coverage.
In this function, 2 statements reached (out of 2): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
@@ -28,7 +28,7 @@
[eva] done for function main2
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
+ 1 function analyzed (out of 2): 50% coverage.
In this function, 1 statements reached (out of 1): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/saveload/oracle/callbacks_initial.res b/tests/saveload/oracle/callbacks_initial.res
index 25b036ba64125f63b83322c481bbdb8145af540e..ca27cc9df7cc3081e5c5ad7bbd1f98d0b479dbef 100644
--- a/tests/saveload/oracle/callbacks_initial.res
+++ b/tests/saveload/oracle/callbacks_initial.res
@@ -35,7 +35,7 @@
[eva] done for function main1
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 4 functions analyzed (out of 4): 100% coverage.
+ 4 functions analyzed (out of 6): 66% coverage.
In these functions, 9 statements reached (out of 9): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
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 4407cbebb995be38963c081af07126d4ee7385ce..bc309572e3c93311052a35b023b615d0bb7335a5 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
@@ -114,7 +114,7 @@
gen_nondet_i ∈ {31}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 5): 40% coverage.
+ 2 functions analyzed (out of 2): 100% coverage.
In these functions, 45 statements reached (out of 48): 93% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
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 ccd8dec4937e12ce19a03bca5e7be6379d4cb91c..92c05ca5ff89cdd99b6e91c527dbe54d925fe132 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
@@ -114,7 +114,7 @@
gen_nondet_i ∈ {31}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 52): 3% coverage.
+ 2 functions analyzed (out of 2): 100% coverage.
In these functions, 75 statements reached (out of 125): 60% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
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 f029ae319170bc1e849e524390a368aca68a6c87..93eb615f7f19c1b9e96c932e2fe84d4c6de0451d 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
@@ -114,7 +114,7 @@
gen_nondet_i ∈ {31}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 166): 1% coverage.
+ 2 functions analyzed (out of 2): 100% coverage.
In these functions, 74 statements reached (out of 238): 31% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index 18d328c7689fe090af56982f7196f186335068d2..fe68cdf367b9ebc43d0a69b2de88ec79fd1a6378 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -12,7 +12,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- No function to be analyzed.
+ 0 functions analyzed (out of 4): 0% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
diff --git a/tests/value/oracle/summary.1.res.oracle b/tests/value/oracle/summary.1.res.oracle
index 05e3490c3ef8a52ea6ac273e8d1acadc8a85b390..c3d37ddacc8540eb714fae0b9b041752aa5a0383 100644
--- a/tests/value/oracle/summary.1.res.oracle
+++ b/tests/value/oracle/summary.1.res.oracle
@@ -12,7 +12,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
+ 1 function analyzed (out of 4): 25% coverage.
In this function, 1 statements reached (out of 1): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.2.res.oracle b/tests/value/oracle/summary.2.res.oracle
index 7326ccc855202f51023362d23a736ca553142729..642453d63930e4727c5d6ac5f842e6f7657f2cce 100644
--- a/tests/value/oracle/summary.2.res.oracle
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -15,7 +15,7 @@
NON TERMINATING FUNCTION
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 2): 50% coverage.
+ 1 function analyzed (out of 4): 25% coverage.
In this function, 1 statements reached (out of 2): 50% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 58a58f35480ae093a3f912184836bb2e09ad129b..800aa84f7f444f248e282ca4458e5872cd1cea8b 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -73,7 +73,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
+ 2 functions analyzed (out of 4): 50% coverage.
In these functions, 32 statements reached (out of 32): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis: