diff --git a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
index 96be458013ea25c00c86201d01d91dd023508c90..053707094794108ec1bbae31e17d63b128672dc4 100644
--- a/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
+++ b/ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
@@ -244,4 +244,207 @@ const properties_internal: State.Array<Json.key<'#property'>,propertiesData> = {
/** Status of Registered Properties */
export const properties: State.Array<Json.key<'#property'>,propertiesData> = properties_internal;
+/** The alarms are counted after being grouped by these categories */
+export enum alarmCategory {
+ /** Integer division by zero */
+ division_by_zero = 'division_by_zero',
+ /** Invalid pointer dereferencing */
+ mem_access = 'mem_access',
+ /** Array access out of bounds */
+ index_bound = 'index_bound',
+ /** Invalid shift */
+ shift = 'shift',
+ /** Integer overflow or downcast */
+ overflow = 'overflow',
+ /** Uninitialized memory read */
+ initialization = 'initialization',
+ /** Read of a dangling pointer */
+ dangling_pointer = 'dangling_pointer',
+ /** Non-finite (nan or infinite) floating-point value */
+ is_nan_or_infinite = 'is_nan_or_infinite',
+ /** Overflow in float to int conversion */
+ float_to_int = 'float_to_int',
+ /** Any other alarm */
+ other = 'other',
+}
+
+/** Loose decoder for `alarmCategory` */
+export const jAlarmCategory: Json.Loose<alarmCategory> =
+ Json.jEnum(alarmCategory);
+
+/** Safe decoder for `alarmCategory` */
+export const jAlarmCategorySafe: Json.Safe<alarmCategory> =
+ Json.jFail(Json.jEnum(alarmCategory),
+ 'plugins.eva.general.alarmCategory expected');
+
+/** Natural order for `alarmCategory` */
+export const byAlarmCategory: Compare.Order<alarmCategory> =
+ Compare.byEnum(alarmCategory);
+
+const alarmCategoryTags_internal: Server.GetRequest<null,tag[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.alarmCategoryTags',
+ input: Json.jNull,
+ output: Json.jList(jTag),
+};
+/** Registered tags for the above type. */
+export const alarmCategoryTags: Server.GetRequest<null,tag[]>= alarmCategoryTags_internal;
+
+/** Statuses count.Å“ */
+export type statusesEntry =
+ { valid: number, unknown: number, invalid: number };
+
+/** Loose decoder for `statusesEntry` */
+export const jStatusesEntry: Json.Loose<statusesEntry> =
+ Json.jObject({
+ valid: Json.jFail(Json.jNumber,'Number expected'),
+ unknown: Json.jFail(Json.jNumber,'Number expected'),
+ invalid: Json.jFail(Json.jNumber,'Number expected'),
+ });
+
+/** Safe decoder for `statusesEntry` */
+export const jStatusesEntrySafe: Json.Safe<statusesEntry> =
+ Json.jFail(jStatusesEntry,'StatusesEntry expected');
+
+/** Natural order for `statusesEntry` */
+export const byStatusesEntry: Compare.Order<statusesEntry> =
+ Compare.byFields
+ <{ valid: number, unknown: number, invalid: number }>({
+ valid: Compare.number,
+ unknown: Compare.number,
+ invalid: Compare.number,
+ });
+
+/** Statistics about an Eva analysis. */
+export type statistics =
+ { coverage:
+ { functions: { reachable: number, dead: number },
+ statements: { reachable: number, dead: number } },
+ eva_events: { errors: number, warnings: number },
+ kernel_events: { errors: number, warnings: number },
+ statuses:
+ { alarms: statusesEntry, assertions: statusesEntry,
+ preconds: statusesEntry },
+ alarms: { category: alarmCategory, count: number }[] };
+
+/** Loose decoder for `statistics` */
+export const jStatistics: Json.Loose<statistics> =
+ Json.jObject({
+ coverage: Json.jFail(
+ Json.jObject({
+ functions: Json.jFail(
+ Json.jObject({
+ reachable: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ dead: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ }),'Record expected'),
+ statements: Json.jFail(
+ Json.jObject({
+ reachable: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ dead: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ }),'Record expected'),
+ }),'Record expected'),
+ eva_events: Json.jFail(
+ Json.jObject({
+ errors: Json.jFail(Json.jNumber,'Number expected'),
+ warnings: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ kernel_events: Json.jFail(
+ Json.jObject({
+ errors: Json.jFail(Json.jNumber,'Number expected'),
+ warnings: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ statuses: Json.jFail(
+ Json.jObject({
+ alarms: jStatusesEntrySafe,
+ assertions: jStatusesEntrySafe,
+ preconds: jStatusesEntrySafe,
+ }),'Record expected'),
+ alarms: Json.jList(
+ Json.jObject({
+ category: jAlarmCategorySafe,
+ count: Json.jFail(Json.jNumber,'Number expected'),
+ })),
+ });
+
+/** Safe decoder for `statistics` */
+export const jStatisticsSafe: Json.Safe<statistics> =
+ Json.jFail(jStatistics,'Statistics expected');
+
+/** Natural order for `statistics` */
+export const byStatistics: Compare.Order<statistics> =
+ Compare.byFields
+ <{ coverage:
+ { functions: { reachable: number, dead: number },
+ statements: { reachable: number, dead: number } },
+ eva_events: { errors: number, warnings: number },
+ kernel_events: { errors: number, warnings: number },
+ statuses:
+ { alarms: statusesEntry, assertions: statusesEntry,
+ preconds: statusesEntry },
+ alarms: { category: alarmCategory, count: number }[] }>({
+ coverage: Compare.byFields
+ <{ functions: { reachable: number, dead: number },
+ statements: { reachable: number, dead: number } }>({
+ functions: Compare.byFields
+ <{ reachable: number, dead: number }>({
+ reachable: Compare.number,
+ dead: Compare.number,
+ }),
+ statements: Compare.byFields
+ <{ reachable: number, dead: number }>({
+ reachable: Compare.number,
+ dead: Compare.number,
+ }),
+ }),
+ eva_events: Compare.byFields
+ <{ errors: number, warnings: number }>({
+ errors: Compare.number,
+ warnings: Compare.number,
+ }),
+ kernel_events: Compare.byFields
+ <{ errors: number, warnings: number }>({
+ errors: Compare.number,
+ warnings: Compare.number,
+ }),
+ statuses: Compare.byFields
+ <{ alarms: statusesEntry, assertions: statusesEntry,
+ preconds: statusesEntry }>({
+ alarms: byStatusesEntry,
+ assertions: byStatusesEntry,
+ preconds: byStatusesEntry,
+ }),
+ alarms: Compare.array(
+ Compare.byFields
+ <{ category: alarmCategory, count: number }>({
+ category: byAlarmCategory,
+ count: Compare.number,
+ })),
+ });
+
+/** Signal for state [`stats`](#stats) */
+export const signalStats: Server.Signal = {
+ name: 'plugins.eva.general.signalStats',
+};
+
+const getStats_internal: Server.GetRequest<null,statistics> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getStats',
+ input: Json.jNull,
+ output: jStatistics,
+};
+/** Getter for state [`stats`](#stats) */
+export const getStats: Server.GetRequest<null,statistics>= getStats_internal;
+
+const stats_internal: State.Value<statistics> = {
+ name: 'plugins.eva.general.stats',
+ signal: signalStats,
+ getter: getStats,
+};
+/** Statistics about the last Eva analysis */
+export const stats: State.Value<statistics> = stats_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/.eslintrc.js b/ivette/src/frama-c/plugins/eva/.eslintrc.js
new file mode 100644
index 0000000000000000000000000000000000000000..50624b8675a991f2987e7a1da222c1e323eacc84
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/.eslintrc.js
@@ -0,0 +1,20 @@
+module.exports = {
+ root: true,
+ overrides: [
+ {
+ files: ['*.js', '*.jsx', '*.ts', '*.tsx'],
+ excludedFiles: 'summary.tsx',
+ extends: ["../../../../.eslintrc.js"]
+ },
+ {
+ files: ['summary.tsx'],
+ extends: [
+ 'eslint:recommended',
+ 'plugin:react/recommended',
+ 'plugin:react-hooks/recommended',
+ 'plugin:@typescript-eslint/eslint-recommended',
+ 'plugin:@typescript-eslint/recommended',
+ ]
+ }
+ ]
+};
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 9f2c3c733ab8443c010bf7f0a7f1cc1c05993a7a..495b0dde3331865486aa902ecb961e23746f1679 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -36,6 +36,7 @@ import { AutoSizer } from 'react-virtualized';
import { ProbeInfos } from './probeinfos';
import { Dimension, ValuesPanel } from './valuetable';
import { AlarmsInfos, StackInfos } from './valueinfos';
+import { } from './summary';
import './style.css';
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/summary.tsx b/ivette/src/frama-c/plugins/eva/summary.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..b1d8fd74dedd2561577f786e6919be1bb7c694af
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/summary.tsx
@@ -0,0 +1,239 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+// React & Dome
+import React from 'react';
+import * as Ivette from 'ivette';
+import { Vfill } from 'dome/layout/boxes';
+import * as States from 'frama-c/states';
+import * as Eva from 'frama-c/api/plugins/eva/general';
+
+function percent(reachable: number, total: number): string {
+ return (reachable * 100 / total).toFixed(1) + '%';
+}
+
+function FunCoverage(data: Eva.statistics): JSX.Element {
+ const {coverage: {functions: {reachable, dead}}} = data;
+ const total = reachable + dead;
+ const ratio = percent(reachable, total);
+ return total > 0 ? (
+ <>
+ <span>{reachable}</span> function{total === 1 ? '' : 's'} {' '}
+ analyzed (out of <span>{total}</span>): <span>{ratio}</span> coverage.
+ </>
+ ) :
+ <>No function to be analyzed.</>;
+}
+
+function StmtCoverage(data: Eva.statistics): JSX.Element {
+ const {coverage: {statements: {reachable, dead}}} = data;
+ const total = reachable + dead;
+ const ratio = percent(reachable, total);
+ const functions = data.coverage.functions.reachable;
+ return (functions > 0 && total > 0 ? (
+ <>
+ In {functions > 1 ? 'these functions' : 'this function'},{' '}
+ <span>{reachable}</span> statements reached
+ (out of <span>{total}</span>): <span>{ratio}</span> coverage.
+ </>
+ ) :
+ <></>
+ );
+}
+
+function CoverageTable(data: Eva.statistics): JSX.Element {
+ const {coverage: {functions, statements}} = data;
+ const functionsTotal = functions.reachable + functions.dead;
+ const statementsTotal = statements.reachable + statements.dead;
+ return (
+ <table>
+ <thead>
+ <tr>
+ <th />
+ <th>Analyzed</th>
+ <th>Total</th>
+ <th>Coverage</th>
+ </tr>
+ </thead>
+ <tbody>
+ <tr>
+ <td>Functions</td>
+ <td>{functions.reachable}</td>
+ <td>{functionsTotal}</td>
+ <td>{percent(functions.reachable, functionsTotal)}</td>
+ </tr>
+ <tr>
+ <td>Statements</td>
+ <td>{statements.reachable}</td>
+ <td>{statementsTotal}</td>
+ <td>{percent(statements.reachable, statementsTotal)}</td>
+ </tr>
+ </tbody>
+ </table>
+ );
+}
+
+function plural(count: number): string {
+ return count === 1 ? '' : 's';
+}
+
+function Errors(data: Eva.statistics): JSX.Element {
+ const {eva_events: eva, kernel_events: kernel} = data;
+ const total = eva.warnings + eva.errors + kernel.warnings + kernel.errors;
+ return (total > 0 ? (
+ <>
+ Some errors and warnings have been raised during the analysis:
+ <table>
+ <tbody>
+ <tr>
+ <td>by the Eva analyzer</td>
+ <td>{eva.errors} error{plural(eva.errors)}</td>
+ <td>{eva.warnings} warning{plural(eva.warnings)}</td>
+ </tr>
+ <tr>
+ <td>by the Frama-C kernel</td>
+ <td>{kernel.errors} error{plural(kernel.errors)}</td>
+ <td>{kernel.warnings} warning{plural(kernel.warnings)}</td>
+ </tr>
+ </tbody>
+ </table>
+ </>
+ ) :
+ <>No errors or warnings raised during the analysis.</>
+ );
+}
+
+function Alarms(data: Eva.statistics,
+ categories: Map<string, States.Tag>): JSX.Element {
+ const {alarms, statuses: {alarms: {invalid, unknown}}} = data;
+ const total = unknown + invalid;
+
+ const label = (category: Eva.alarmCategory): string | undefined =>
+ categories.get(category)?.descr;
+
+ return (
+ <>
+ <div>{total} alarms{plural(total)} generated by the analysis</div>
+ <table>
+ <tbody>
+ {alarms.map(entry => (
+ <tr key={entry.category}>
+ <td>{entry.count}</td>
+ <td>{label(entry.category)}</td>
+ </tr>
+ ))}
+ </tbody>
+ </table>
+ {invalid > 0 && (
+ <div>
+ {invalid} of them {invalid === 1 ? 'is a' : 'are'} sure
+ alarm{plural(invalid)}.
+ </div>
+ )}
+ </>
+ );
+}
+
+function Statuses(data: Eva.statistics): JSX.Element {
+ const { assertions, preconds } = data.statuses;
+ const all = (entry: Eva.statusesEntry): number =>
+ entry.valid + entry.unknown + entry.invalid;
+ const totalAssertions = all(assertions);
+ const totalPreconds = all(preconds);
+ const total = totalAssertions + totalPreconds;
+ const proven = assertions.valid + preconds.valid;
+ if (total > 0) {
+ return (
+ <>
+ <table>
+ <tbody>
+ <tr>
+ <th>Assertions</th>
+ <td>{assertions.valid} valid</td>
+ <td>{assertions.unknown} unknown</td>
+ <td>{assertions.invalid} invalid</td>
+ <td>{totalAssertions} total</td>
+ </tr>
+ <tr>
+ <th>Preconditions</th>
+ <td>{preconds.valid} valid</td>
+ <td>{preconds.unknown} unknown</td>
+ <td>{preconds.invalid} invalid</td>
+ <td>{totalPreconds} total</td>
+ </tr>
+ </tbody>
+ </table>
+ {percent(proven, total)} of the logical properties reached have been
+ proven.
+ </>
+ );
+ }
+
+ return (<>No logical properties have been reached by the analysis.</>);
+
+}
+
+export function EvaSummary(): JSX.Element {
+ const alarmCategories = States.useTags(Eva.alarmCategoryTags);
+ const data = States.useSyncValue(Eva.stats);
+
+ return (data && alarmCategories ? (
+ <>
+ <h2>Coverage</h2>
+ <ul>
+ <li>{FunCoverage(data)}</li>
+ <li>{StmtCoverage(data)}</li>
+ </ul>
+ {CoverageTable(data)}
+ <h2>Errors</h2>
+ {Errors(data)}
+ <h2>Alarms</h2>
+ {Alarms(data, alarmCategories)}
+ <h2>Statuses</h2>
+ {Statuses(data)}
+ </>
+ ) :
+ <></>
+ );
+}
+
+function EvaSummaryComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <Vfill>
+ <EvaSummary />
+ </Vfill>
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.eva_summary',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'Eva Summary',
+ title: 'Summary of the Eva analysis',
+ children: <EvaSummaryComponent />,
+});
+
+// --------------------------------------------------------------------------
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 283e6dbac434a63b4ab21abc0806b80ed26a4609..78a7ba5c09ffd6fd53904326db777374a312c940 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -206,4 +206,189 @@ let _array =
~iter:Property_status.iter
model
+
+(* ----- Analysis statistics -------------------------------------------- *)
+
+module AlarmCategory = struct
+ open Server.Data
+
+ module Tags =
+ struct
+ let dictionary = Enum.dictionary ()
+
+ (* Give a normal representation of the category *)
+ let repr =
+ let e = List.hd Cil_datatype.Exp.reprs in
+ let lv = List.hd Cil_datatype.Lval.reprs in
+ function
+ | Value_results.Division_by_zero -> Alarms.Division_by_zero e
+ | Memory_access -> Memory_access (lv, For_reading)
+ | Index_out_of_bound-> Index_out_of_bound (e, None)
+ | Invalid_shift -> Invalid_shift (e, None)
+ | Overflow -> Overflow (Signed, e, Integer.one, Lower_bound)
+ | Uninitialized -> Uninitialized lv
+ | Dangling -> Dangling lv
+ | Nan_or_infinite -> Is_nan_or_infinite (e, FFloat)
+ | Float_to_int -> Float_to_int (e, Integer.one, Lower_bound)
+ | Other -> assert false
+
+ let register alarm_category =
+ let name, descr = match alarm_category with
+ | Value_results.Other -> "other", "Any other alarm"
+ | alarm_category ->
+ let alarm = repr alarm_category in
+ Alarms.(get_short_name alarm, get_description alarm)
+ in
+ Enum.tag dictionary
+ ~name
+ ~label:(Markdown.plain name)
+ ~descr:(Markdown.plain descr)
+
+ let division_by_zero = register Division_by_zero
+ let memory_access = register Memory_access
+ let index_out_of_bound = register Index_out_of_bound
+ let invalid_shift = register Invalid_shift
+ let overflow = register Overflow
+ let uninitialized = register Uninitialized
+ let dangling = register Dangling
+ let nan_or_infinite = register Nan_or_infinite
+ let float_to_int = register Float_to_int
+ let other = register Other
+
+ let () = Enum.set_lookup dictionary
+ begin function
+ | Value_results.Division_by_zero -> division_by_zero
+ | Memory_access -> memory_access
+ | Index_out_of_bound -> index_out_of_bound
+ | Invalid_shift -> invalid_shift
+ | Overflow -> overflow
+ | Uninitialized -> uninitialized
+ | Dangling -> dangling
+ | Nan_or_infinite -> nan_or_infinite
+ | Float_to_int -> float_to_int
+ | Other -> other
+ end
+ end
+
+ let name = "alarmCategory"
+ let descr = Markdown.plain
+ "The alarms are counted after being grouped by these categories"
+ let data = Request.dictionary ~package ~name ~descr Tags.dictionary
+
+ include (val data : S with type t = Value_results.alarm_category)
+end
+
+module CoverageEntry =
+struct
+ open Value_results
+ let jtype = Package.(
+ Jrecord [
+ "reachable",Jnumber ;
+ "dead",Jnumber ;
+ ])
+ let to_json x = `Assoc [
+ "reachable", `Int x.reachable ;
+ "dead", `Int x.dead ;
+ ]
+end
+
+module Coverage =
+struct
+ open Value_results
+ let jtype = Package.(
+ Jrecord [
+ "functions",CoverageEntry.jtype ;
+ "statements",CoverageEntry.jtype ;
+ ])
+ let to_json x = `Assoc [
+ "functions", CoverageEntry.to_json x.functions ;
+ "statements", CoverageEntry.to_json x.statements ;
+ ]
+end
+
+module EventCount =
+struct
+ open Value_results
+ let jtype = Package.(
+ Jrecord [
+ "errors",Jnumber ;
+ "warnings",Jnumber ;
+ ])
+ let to_json x = `Assoc [
+ "errors", `Int x.errors ;
+ "warnings", `Int x.warnings ;
+ ]
+end
+
+module StatusesEntry =
+struct
+ open Value_results
+ let jtype =
+ Data.declare ~package
+ ~name:"statusesEntry"
+ ~descr:(Markdown.plain "Statuses count.Å“")
+ Package.(Jrecord [
+ "valid",Jnumber ;
+ "unknown",Jnumber ;
+ "invalid",Jnumber ;
+ ])
+ let to_json x = `Assoc [
+ "valid", `Int x.valid ;
+ "unknown", `Int x.unknown ;
+ "invalid", `Int x.invalid ;
+ ]
+end
+
+module Statuses =
+struct
+ open Value_results
+ let jtype = Package.(
+ Jrecord [
+ "alarms",StatusesEntry.jtype ;
+ "assertions",StatusesEntry.jtype ;
+ "preconds",StatusesEntry.jtype ;
+ ])
+ let to_json (x : statuses) = `Assoc [
+ "alarms", StatusesEntry.to_json x.alarms ;
+ "assertions", StatusesEntry.to_json x.assertions ;
+ "preconds", StatusesEntry.to_json x.preconds ;
+ ]
+end
+
+module Statistics = struct
+ open Value_results
+ type t = stats
+ let jtype =
+ Data.declare ~package
+ ~name:"statistics"
+ ~descr:(Markdown.plain "Statistics about an Eva analysis.")
+ Package.(Jrecord [
+ "coverage",Coverage.jtype ;
+ "eva_events",EventCount.jtype ;
+ "kernel_events",EventCount.jtype ;
+ "statuses",Statuses.jtype ;
+ "alarms",Jlist (Jrecord [
+ "category", AlarmCategory.jtype ;
+ "count", Jnumber ])])
+ let to_json x = `Assoc [
+ "coverage", Coverage.to_json x.coverage ;
+ "eva_events", EventCount.to_json x.eva_events ;
+ "kernel_events", EventCount.to_json x.kernel_events ;
+ "statuses", Statuses.to_json x.statuses ;
+ "alarms", `List (List.map (fun (a,c) -> `Assoc [
+ "category", AlarmCategory.to_json a ;
+ "count", `Int c ]) (AlarmsStats.bindings x.alarms))]
+end
+
+let () =
+ let signal = States.register_value ~package
+ ~name:"stats"
+ ~descr:(Markdown.plain "Statistics about the last Eva analysis")
+ ~output:(module Statistics)
+ ~get:Value_results.compute_stats
+ ()
+ in
+ Analysis.register_computed_hook (fun () -> Request.emit signal)
+
+
(**************************************************************************)
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 9ca7a64e5c07ea32af4db09682dae6ed5049fc82..1f82e0d16b7c9d143cb2919e045e57af8b7e6680 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -351,128 +351,120 @@ let merge r1 r2 =
{ main; before_states; after_states; kf_initial_states; kf_is_called;
initial_state; initial_args; alarms; statuses; kf_callers }
-(* ---------------------- Printing an analysis summary ---------------------- *)
-open Cil_types
+(* ---------------------- Stats for analysis summary ---------------------- *)
+
+type alarm_category =
+ | Division_by_zero
+ | Memory_access
+ | Index_out_of_bound
+ | Invalid_shift
+ | Overflow
+ | Uninitialized
+ | Dangling
+ | Nan_or_infinite
+ | Float_to_int
+ | Other
+
+module AlarmCategory =
+struct
+ type t = alarm_category
+
+ let of_alarm = function
+ | Alarms.Division_by_zero _ -> Division_by_zero
+ | Memory_access _ -> Memory_access
+ | Index_out_of_bound _ -> Index_out_of_bound
+ | Invalid_shift _ -> Invalid_shift
+ | Overflow _ -> Overflow
+ | Uninitialized _ -> Uninitialized
+ | Dangling _ -> Dangling
+ | Is_nan_or_infinite _
+ | Is_nan _ -> Nan_or_infinite
+ | Float_to_int _ -> Float_to_int
+ | _ -> Other
+
+ let id = function
+ | Division_by_zero -> 0
+ | Memory_access -> 1
+ | Index_out_of_bound -> 2
+ | Invalid_shift -> 4
+ | Overflow -> 5
+ | Uninitialized -> 6
+ | Dangling -> 7
+ | Nan_or_infinite -> 8
+ | Float_to_int -> 9
+ | Other -> 10
+
+ let compare c1 c2 = id c1 - id c2
+end
-let plural count = if count = 1 then "" else "s"
+module AlarmsStats =
+struct
+ include Map.Make (AlarmCategory)
+
+ let get a m = try find a m with Not_found -> 0
+ let incr a m = add a (get a m + 1) m
+end
+
+type coverage_entry =
+ { mutable reachable: int;
+ mutable dead: int; }
+
+type coverage =
+ { functions: coverage_entry;
+ statements: coverage_entry; }
+
+type event_count =
+ { mutable errors: int;
+ mutable warnings: int; }
+
+type statuses_entry =
+ { mutable valid: int;
+ mutable unknown: int;
+ mutable invalid: int; }
+
+type statuses =
+ { alarms: statuses_entry;
+ assertions: statuses_entry;
+ preconds: statuses_entry; }
+
+type stats =
+ { coverage: coverage;
+ eva_events: event_count;
+ kernel_events: event_count;
+ statuses: statuses;
+ alarms: int AlarmsStats.t; }
let consider_function vi =
not (Cil_builtins.is_builtin vi
|| Cil_builtins.is_special_builtin vi.vname
|| Cil.is_in_libc vi.vattr)
-let print_coverage fmt =
- let dead_function, reachable_function = ref 0, ref 0
- and dead_stmt, reachable_stmt = ref 0, ref 0 in
+let compute_coverage () =
+ let open Cil_types in
+ let coverage = {
+ functions = { reachable = 0; dead = 0 };
+ statements = { reachable = 0; dead = 0 };
+ }
+ and incr c = function
+ | false -> c.dead <- c.dead + 1
+ | true -> c.reachable <- c.reachable + 1
+ in
let do_stmt stmt =
- incr (if Db.Value.is_reachable_stmt stmt then reachable_stmt else dead_stmt)
+ incr coverage.statements (Db.Value.is_reachable_stmt stmt)
in
- let visit fundec =
+ let do_fun fundec =
if consider_function fundec.svar then
- if is_called (Globals.Functions.get fundec.svar)
- then (incr reachable_function; List.iter do_stmt fundec.sallstmts)
- else incr dead_function
- in
- Globals.Functions.iter_on_fundecs visit;
- 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.@;"
- !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 !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
- and kernel_warnings, kernel_errors = ref 0, ref 0 in
- let report_event event =
- let open Log in
- match event.evt_kind, event.evt_plugin with
- | Warning, "eva" when event.evt_category <> Some "alarm" -> incr eva_warnings
- | Warning, name when name = Log.kernel_label_name -> incr kernel_warnings
- | Error, "eva" when event.evt_category <> Some "alarm" -> incr eva_errors
- | Error, name when name = Log.kernel_label_name -> incr kernel_errors
- | _ -> ()
- in
- Messages.iter report_event;
- let total = !eva_errors + !eva_warnings + !kernel_errors + !kernel_warnings in
- if total = 0
- then Format.fprintf fmt "No errors or warnings raised during the analysis.@;"
- else
- let print str errors warnings =
- Format.fprintf fmt " by %-19s %3i error%s %3i warning%s@;"
- (str ^ ":") errors (plural errors) warnings (plural warnings)
- in
- Format.fprintf fmt
- "Some errors and warnings have been raised during the analysis:@;";
- print "the Eva analyzer" !eva_errors !eva_warnings;
- print "the Frama-C kernel" !kernel_errors !kernel_warnings
-
-type alarms =
- { division_by_zero: int ref;
- memory_access: int ref;
- index_out_of_bound: int ref;
- overflow: int ref;
- invalid_shift: int ref;
- uninitialized: int ref;
- dangling: int ref;
- nan_or_infinite: int ref;
- float_to_int: int ref;
- others: int ref; }
-
-type statuses = { valid: int ref; unknown: int ref; invalid: int ref; }
-
-type report =
- { alarms: statuses * alarms;
- assertions: statuses;
- preconds: statuses; }
-
-let empty_report () =
- let empty () = { valid = ref 0; unknown = ref 0; invalid = ref 0 } in
- let empty_alarms =
- { division_by_zero = ref 0;
- memory_access = ref 0;
- index_out_of_bound = ref 0;
- overflow = ref 0;
- invalid_shift = ref 0;
- uninitialized = ref 0;
- dangling = ref 0;
- nan_or_infinite = ref 0;
- float_to_int = ref 0;
- others = ref 0; }
- in
- { alarms = empty (), empty_alarms;
- assertions = empty ();
- preconds = empty (); }
-
-let report_alarm report alarm =
- let open Alarms in
- let counter = match alarm with
- | Division_by_zero _ -> report.division_by_zero
- | Memory_access _ -> report.memory_access
- | Index_out_of_bound _ -> report.index_out_of_bound
- | Invalid_shift _ -> report.invalid_shift
- | Overflow _ -> report.overflow
- | Uninitialized _ -> report.uninitialized
- | Dangling _ -> report.dangling
- | Is_nan_or_infinite _
- | Is_nan _ -> report.nan_or_infinite
- | Float_to_int _ -> report.float_to_int
- | _ -> report.others
+ let called = is_called (Globals.Functions.get fundec.svar) in
+ incr coverage.functions called;
+ if called then
+ List.iter do_stmt fundec.sallstmts
in
- incr counter
-
-let eva_emitter = Value_util.emitter
+ Globals.Functions.iter_on_fundecs do_fun;
+ coverage
let get_status ip =
+ let eva_emitter = Value_util.emitter in
let aux_status emitter status acc =
let emitter = Emitter.Usable_emitter.get emitter.Property_status.emitter in
if Emitter.equal eva_emitter emitter
@@ -481,71 +473,151 @@ let get_status ip =
in
Property_status.fold_on_statuses aux_status ip None
-let report_status acc = function
+let count_status acc = function
| None -> ()
| Some status -> match status with
- | Property_status.Dont_know -> incr acc.unknown
- | Property_status.True -> incr acc.valid
+ | Property_status.Dont_know -> acc.unknown <- acc.unknown + 1
+ | Property_status.True -> acc.valid <- acc.valid + 1
| Property_status.False_if_reachable
- | Property_status.False_and_reachable -> incr acc.invalid
-
-let make_report () =
- let report = empty_report () in
- let report_property ip =
+ | Property_status.False_and_reachable -> acc.invalid <- acc.invalid + 1
+
+let compute_statuses () =
+ let empty () = { valid = 0; unknown = 0; invalid = 0 } in
+ let statuses =
+ { alarms = empty ();
+ assertions = empty ();
+ preconds = empty ();
+ } in
+ let alarms = ref AlarmsStats.empty in
+ let incr a =
+ alarms := AlarmsStats.incr a !alarms
+ in
+ let do_property ip =
match ip with
| Property.IPCodeAnnot Property.{ ica_ca; ica_stmt; }
when Db.Value.is_reachable_stmt ica_stmt ->
begin
let status = get_status ip in
match Alarms.find ica_ca with
- | None -> report_status report.assertions status
+ | None -> count_status statuses.assertions status
| Some alarm ->
- let acc_status, acc_alarms = report.alarms in
- report_status acc_status status;
+ count_status statuses.alarms status;
match status with
| None | Some Property_status.True -> ()
- | _ -> report_alarm acc_alarms alarm
+ | _ -> incr (AlarmCategory.of_alarm alarm)
end
| Property.IPPropertyInstance {Property.ii_stmt}
when Db.Value.is_reachable_stmt ii_stmt ->
- report_status report.preconds (get_status ip)
+ count_status statuses.preconds (get_status ip)
+ | _ -> ()
+ in
+ Property_status.iter do_property;
+ statuses, !alarms
+
+let compute_stats () =
+ let statuses, alarms = compute_statuses () in
+ let stats = {
+ coverage = compute_coverage ();
+ eva_events = { errors = 0 ; warnings = 0 };
+ kernel_events = { errors = 0 ; warnings = 0 };
+ statuses;
+ alarms;
+ }
+ and incr_err entry =
+ entry.errors <- entry.errors + 1
+ and incr_warn entry =
+ entry.warnings <- entry.warnings + 1
+ in
+ let do_event event =
+ let open Log in
+ match event.evt_kind, event.evt_plugin with
+ | Warning, "eva" when event.evt_category <> Some "alarm" ->
+ incr_warn stats.eva_events
+ | Warning, name when name = Log.kernel_label_name ->
+ incr_warn stats.kernel_events
+ | Error, "eva" when event.evt_category <> Some "alarm" ->
+ incr_err stats.eva_events
+ | Error, name when name = Log.kernel_label_name ->
+ incr_warn stats.kernel_events
| _ -> ()
in
- Property_status.iter report_property;
- report
-
-let print_alarms_kind fmt kind =
- let print count str plural str' =
- if !count > 0 then
- Format.fprintf fmt " %4i %s%s%s@;"
- !count str (if !count > 1 then plural else "") str'
- in
- print kind.division_by_zero "division" "s" " by zero";
- print kind.memory_access "invalid memory access" "es" "";
- print kind.index_out_of_bound "access" "es" " out of bounds index";
- print kind.overflow "integer overflow" "s" "";
- print kind.invalid_shift "invalid shift" "s" "";
- print kind.uninitialized "access" "es" " to uninitialized left-values";
- print kind.dangling "escaping address" "es" "";
- print kind.nan_or_infinite "nan or infinite floating-point value" "s" "";
- print kind.float_to_int "illegal conversion" "s" " from floating-point to integer";
- print kind.others "other" "s" ""
-
-let print_alarms fmt report =
- let alarms, kind = report.alarms in
- let total = !(alarms.unknown) + !(alarms.invalid) in
+ Messages.iter do_event;
+ stats
+
+
+(* ---------------------- Printing an analysis summary ---------------------- *)
+
+let plural count = if count = 1 then "" else "s"
+
+let print_coverage fmt c =
+ let total_function = c.functions.dead + c.functions.reachable 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.@;"
+ c.functions.reachable (plural c.functions.reachable) total_function
+ (c.functions.reachable * 100 / total_function);
+ let total_stmt = c.statements.dead + c.statements.reachable in
+ if c.functions.reachable > 0 && total_stmt > 0 then
+ Format.fprintf fmt
+ "In %s, %i statements reached (out of %i): %i%% coverage.@;"
+ (if c.functions.reachable > 1 then "these functions" else "this function")
+ c.statements.reachable total_stmt
+ (c.statements.reachable * 100 / total_stmt)
+
+let print_events fmt stats =
+ let total =
+ stats.eva_events.warnings + stats.eva_events.errors +
+ stats.kernel_events.warnings + stats.kernel_events.errors
+ in
+ if total = 0
+ then Format.fprintf fmt "No errors or warnings raised during the analysis.@;"
+ else
+ let print str e =
+ Format.fprintf fmt " by %-19s %3i error%s %3i warning%s@;"
+ (str ^ ":") e.errors (plural e.errors) e.warnings (plural e.warnings)
+ in
+ Format.fprintf fmt
+ "Some errors and warnings have been raised during the analysis:@;";
+ print "the Eva analyzer" stats.eva_events;
+ print "the Frama-C kernel" stats.kernel_events
+
+
+let print_alarm fmt category count =
+ let str, plural, str' = match category with
+ | Division_by_zero -> "division", "s", " by zero"
+ | Memory_access -> "invalid memory access", "es", ""
+ | Index_out_of_bound -> "access", "es", " out of bounds index"
+ | Overflow -> "integer overflow", "s", ""
+ | Invalid_shift -> "invalid shift", "s", ""
+ | Uninitialized -> "access", "es", " to uninitialized left-values"
+ | Dangling -> "escaping address", "es", ""
+ | Nan_or_infinite -> "nan or infinite floating-point value", "s", ""
+ | Float_to_int -> "illegal conversion", "s", " from floating-point to integer"
+ | Other -> "other", "s", ""
+ in
+ Format.fprintf fmt " %4i %s%s%s@;"
+ count str (if count > 1 then plural else "") str'
+
+let print_alarms fmt alarms =
+ AlarmsStats.iter (print_alarm fmt) alarms
+
+let print_alarms_statuses fmt stats =
+ let alarms = stats.alarms and statuses = stats.statuses.alarms in
+ let total = statuses.unknown + statuses.invalid in
Format.fprintf fmt "%i alarm%s generated by the analysis" total (plural total);
- if total = !(kind.others)
+ if total = AlarmsStats.get Other alarms
then Format.fprintf fmt ".@;"
- else Format.fprintf fmt ":@;%a" print_alarms_kind kind;
- let invalid = !(alarms.invalid) in
+ else Format.fprintf fmt ":@;%a" print_alarms alarms;
+ let invalid = statuses.invalid in
if invalid > 0 then
Format.fprintf fmt "%i of them %s sure alarm%s (invalid status).@;"
invalid (if invalid = 1 then "is a" else "are") (plural invalid)
-let print_properties fmt report =
- let { assertions; preconds } = report in
- let total acc = !(acc.valid) + !(acc.unknown) + !(acc.invalid) in
+let print_statuses fmt statuses =
+ let { assertions; preconds } = statuses in
+ let total acc = acc.valid + acc.unknown + acc.invalid in
let total_assertions = total assertions
and total_preconds = total preconds in
let total = total_assertions + total_preconds in
@@ -557,28 +629,28 @@ let print_properties fmt report =
let print_line header status total =
Format.fprintf fmt
" %-14s %4d valid %4d unknown %4d invalid %4d total@;"
- header !(status.valid) !(status.unknown) !(status.invalid) total;
+ header status.valid status.unknown status.invalid total;
in
Format.fprintf fmt
"Evaluation of the logical properties reached by the analysis:@;";
print_line "Assertions" assertions total_assertions;
print_line "Preconditions" preconds total_preconds;
- let proven = !(assertions.valid) + !(preconds.valid) in
+ let proven = assertions.valid + preconds.valid in
let proven = proven * 100 / total in
Format.fprintf fmt
"%i%% of the logical properties reached have been proven.@;" proven
let print_summary fmt =
let bar = String.make 76 '-' in
- let report = make_report () in
+ let stats = compute_stats () in
Format.fprintf fmt "%s@;" bar;
- print_coverage fmt;
+ print_coverage fmt stats.coverage;
Format.fprintf fmt "%s@;" bar;
- print_warning fmt;
+ print_events fmt stats;
Format.fprintf fmt "%s@;" bar;
- print_alarms fmt report;
+ print_alarms_statuses fmt stats;
Format.fprintf fmt "%s@;" bar;
- print_properties fmt report;
+ print_statuses fmt stats.statuses;
Format.fprintf fmt "%s" bar
let print_summary () =
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/value_results.mli
index 512f45ebeb52538dd4963d1f659172fd9e1c56b2..dda49eb3f3b4c1318a5a59c903742909ec616854 100644
--- a/src/plugins/value/utils/value_results.mli
+++ b/src/plugins/value/utils/value_results.mli
@@ -46,6 +46,55 @@ val change_callstacks:
For technical reasons, the top of the callstack must currently
be preserved. *)
+
+(** {2 Summary } *)
+
+type alarm_category =
+ | Division_by_zero
+ | Memory_access
+ | Index_out_of_bound
+ | Invalid_shift
+ | Overflow
+ | Uninitialized
+ | Dangling
+ | Nan_or_infinite
+ | Float_to_int
+ | Other
+
+module AlarmsStats : Map.S with type key = alarm_category
+
+type coverage_entry =
+ { mutable reachable: int;
+ mutable dead: int; }
+
+type coverage =
+ { functions: coverage_entry;
+ statements: coverage_entry; }
+
+type event_count =
+ { mutable errors: int;
+ mutable warnings: int; }
+
+type statuses_entry =
+ { mutable valid: int;
+ mutable unknown: int;
+ mutable invalid: int; }
+
+type statuses =
+ { alarms: statuses_entry;
+ assertions: statuses_entry;
+ preconds: statuses_entry; }
+
+type stats =
+ { coverage: coverage;
+ eva_events: event_count;
+ kernel_events: event_count;
+ statuses: statuses;
+ alarms: int AlarmsStats.t; }
+
+(** Compute analysis statistics. *)
+val compute_stats: unit -> stats
+
(** Prints a summary of the analysis. *)
val print_summary: unit -> unit
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 8c983fd90a289be87579fd40cfe9efbde6414a90..d852f36ef101da04ad12d22bbdd37ab6577ee632 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -94,8 +94,8 @@
1 division by zero
2 invalid memory accesses
2 accesses out of bounds index
- 3 integer overflows
2 invalid shifts
+ 3 integer overflows
1 escaping address
2 nan or infinite floating-point values
2 illegal conversions from floating-point to integer
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 7bfb7aff0243d6fb76ac66ee9a5adf16a98cbed9..32a83624c64a9bbb40bae6f216db19c2f668fc41 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -117,8 +117,8 @@
1 division by zero
3 invalid memory accesses
2 accesses out of bounds index
- 3 integer overflows
2 invalid shifts
+ 3 integer overflows
1 escaping address
2 nan or infinite floating-point values
2 illegal conversions from floating-point to integer