diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml index 35ccfc63c83fe5ea2384d8abbe4b62aa6dbf5e44..b9f8b34078bb6422b3c976dd167135b1ca211ca5 100644 --- a/src/plugins/value/utils/summary.ml +++ b/src/plugins/value/utils/summary.ml @@ -290,15 +290,16 @@ let compute_stats () = and prog_alarms = AlarmsStats.create 131 in let do_fun kf = - if consider_function (Kernel_function.get_vi kf) then - let reachable = Value_results.is_called kf in + let reachable = Value_results.is_called kf in + let consider = consider_function (Kernel_function.get_vi kf) in + if consider then Coverage.incr prog_fun_coverage ~reachable; - if reachable then begin - let fun_stats = FunctionStats.get kf in - (* Add function stats to program stats *) + if reachable then begin + let fun_stats = FunctionStats.get kf in + AlarmsStats.add_list prog_alarms fun_stats.fun_alarm_count; + if consider then Coverage.add prog_stmt_coverage fun_stats.fun_coverage; - AlarmsStats.add_list prog_alarms fun_stats.fun_alarm_count; - end + end in Globals.Functions.iter do_fun; let alarms_statuses, assertions_statuses, preconds_statuses =