diff --git a/Makefile b/Makefile
index 69e9b86684f6cde8b04d6a6f5b12987de89a81e7..a5f8daa3d76f371459e0586a27400b34d9037aee 100644
--- a/Makefile
+++ b/Makefile
@@ -882,6 +882,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/warn domains/cvalue/locals_scoping \
domains/cvalue/cvalue_offsetmap \
utils/value_results \
+ utils/summary \
domains/cvalue/builtins domains/cvalue/builtins_malloc \
domains/cvalue/builtins_string domains/cvalue/builtins_misc \
domains/cvalue/builtins_memory domains/cvalue/builtins_print_c \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 81ea66623889de33690c7d2cfd92aa261053deb6..95e9f72a6f9d21e5558b33525c9cf242887155e0 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1477,6 +1477,8 @@ src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/summary.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/summary.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.ml: CEA_LGPL_OR_PROPRIETARY
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..e0d31cec7827634693a791baebce957b4312ab3e 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
@@ -54,15 +54,53 @@ import { jTagSafe } from 'frama-c/api/kernel/data';
//@ts-ignore
import { tag } from 'frama-c/api/kernel/data';
-const isComputed_internal: Server.GetRequest<null,boolean> = {
+/** State of the computation of Eva Analysis. */
+export type computationStateType = "not_computed" | "computing" | "computed";
+
+/** Loose decoder for `computationStateType` */
+export const jComputationStateType: Json.Loose<computationStateType> =
+ Json.jUnion<"not_computed" | "computing" | "computed">(
+ Json.jTag("not_computed"),
+ Json.jTag("computing"),
+ Json.jTag("computed"),
+ );
+
+/** Safe decoder for `computationStateType` */
+export const jComputationStateTypeSafe: Json.Safe<computationStateType> =
+ Json.jFail(jComputationStateType,'ComputationStateType expected');
+
+/** Natural order for `computationStateType` */
+export const byComputationStateType: Compare.Order<computationStateType> =
+ Compare.structural;
+
+/** Signal for state [`computationState`](#computationstate) */
+export const signalComputationState: Server.Signal = {
+ name: 'plugins.eva.general.signalComputationState',
+};
+
+const getComputationState_internal: Server.GetRequest<
+ null,
+ computationStateType
+ > = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.general.isComputed',
+ name: 'plugins.eva.general.getComputationState',
input: Json.jNull,
- output: Json.jBoolean,
+ output: jComputationStateType,
signals: [],
};
-/** True if the Eva analysis has been done */
-export const isComputed: Server.GetRequest<null,boolean>= isComputed_internal;
+/** Getter for state [`computationState`](#computationstate) */
+export const getComputationState: Server.GetRequest<
+ null,
+ computationStateType
+ >= getComputationState_internal;
+
+const computationState_internal: State.Value<computationStateType> = {
+ name: 'plugins.eva.general.computationState',
+ signal: signalComputationState,
+ getter: getComputationState,
+};
+/** The current computation state of the analysis. */
+export const computationState: State.Value<computationStateType> = computationState_internal;
const getCallers_internal: Server.GetRequest<
Json.key<'#fct'>,
@@ -244,4 +282,302 @@ 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),
+ signals: [],
+};
+/** 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,
+ });
+
+/** Alarm count for each alarm category. */
+export type alarmEntry = { category: alarmCategory, count: number };
+
+/** Loose decoder for `alarmEntry` */
+export const jAlarmEntry: Json.Loose<alarmEntry> =
+ Json.jObject({
+ category: jAlarmCategorySafe,
+ count: Json.jFail(Json.jNumber,'Number expected'),
+ });
+
+/** Safe decoder for `alarmEntry` */
+export const jAlarmEntrySafe: Json.Safe<alarmEntry> =
+ Json.jFail(jAlarmEntry,'AlarmEntry expected');
+
+/** Natural order for `alarmEntry` */
+export const byAlarmEntry: Compare.Order<alarmEntry> =
+ Compare.byFields
+ <{ category: alarmCategory, count: number }>({
+ category: byAlarmCategory,
+ count: Compare.number,
+ });
+
+/** Statistics about an Eva analysis. */
+export type programStatsType =
+ { progFunCoverage: { reachable: number, dead: number },
+ progStmtCoverage: { reachable: number, dead: number },
+ progAlarms: alarmEntry[],
+ evaEvents: { errors: number, warnings: number },
+ kernelEvents: { errors: number, warnings: number },
+ alarmsStatuses: statusesEntry, assertionsStatuses: statusesEntry,
+ precondsStatuses: statusesEntry };
+
+/** Loose decoder for `programStatsType` */
+export const jProgramStatsType: Json.Loose<programStatsType> =
+ Json.jObject({
+ progFunCoverage: Json.jFail(
+ Json.jObject({
+ reachable: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ dead: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ progStmtCoverage: Json.jFail(
+ Json.jObject({
+ reachable: Json.jFail(Json.jNumber,
+ 'Number expected'),
+ dead: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ progAlarms: Json.jList(jAlarmEntry),
+ evaEvents: Json.jFail(
+ Json.jObject({
+ errors: Json.jFail(Json.jNumber,'Number expected'),
+ warnings: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ kernelEvents: Json.jFail(
+ Json.jObject({
+ errors: Json.jFail(Json.jNumber,'Number expected'),
+ warnings: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ alarmsStatuses: jStatusesEntrySafe,
+ assertionsStatuses: jStatusesEntrySafe,
+ precondsStatuses: jStatusesEntrySafe,
+ });
+
+/** Safe decoder for `programStatsType` */
+export const jProgramStatsTypeSafe: Json.Safe<programStatsType> =
+ Json.jFail(jProgramStatsType,'ProgramStatsType expected');
+
+/** Natural order for `programStatsType` */
+export const byProgramStatsType: Compare.Order<programStatsType> =
+ Compare.byFields
+ <{ progFunCoverage: { reachable: number, dead: number },
+ progStmtCoverage: { reachable: number, dead: number },
+ progAlarms: alarmEntry[],
+ evaEvents: { errors: number, warnings: number },
+ kernelEvents: { errors: number, warnings: number },
+ alarmsStatuses: statusesEntry, assertionsStatuses: statusesEntry,
+ precondsStatuses: statusesEntry }>({
+ progFunCoverage: Compare.byFields
+ <{ reachable: number, dead: number }>({
+ reachable: Compare.number,
+ dead: Compare.number,
+ }),
+ progStmtCoverage: Compare.byFields
+ <{ reachable: number, dead: number }>({
+ reachable: Compare.number,
+ dead: Compare.number,
+ }),
+ progAlarms: Compare.array(byAlarmEntry),
+ evaEvents: Compare.byFields
+ <{ errors: number, warnings: number }>({
+ errors: Compare.number,
+ warnings: Compare.number,
+ }),
+ kernelEvents: Compare.byFields
+ <{ errors: number, warnings: number }>({
+ errors: Compare.number,
+ warnings: Compare.number,
+ }),
+ alarmsStatuses: byStatusesEntry,
+ assertionsStatuses: byStatusesEntry,
+ precondsStatuses: byStatusesEntry,
+ });
+
+/** Signal for state [`programStats`](#programstats) */
+export const signalProgramStats: Server.Signal = {
+ name: 'plugins.eva.general.signalProgramStats',
+};
+
+const getProgramStats_internal: Server.GetRequest<null,programStatsType> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getProgramStats',
+ input: Json.jNull,
+ output: jProgramStatsType,
+ signals: [],
+};
+/** Getter for state [`programStats`](#programstats) */
+export const getProgramStats: Server.GetRequest<null,programStatsType>= getProgramStats_internal;
+
+const programStats_internal: State.Value<programStatsType> = {
+ name: 'plugins.eva.general.programStats',
+ signal: signalProgramStats,
+ getter: getProgramStats,
+};
+/** Statistics about the last Eva analysis for the whole program */
+export const programStats: State.Value<programStatsType> = programStats_internal;
+
+/** Data for array rows [`functionStats`](#functionstats) */
+export interface functionStatsData {
+ /** Entry identifier. */
+ key: Json.key<'#fundec'>;
+ /** Coverage of the Eva analysis */
+ coverage: { reachable: number, dead: number };
+ /** Alarms raised by the Eva analysis by category */
+ alarmCount: alarmEntry[];
+ /** Alarms statuses emitted by the Eva analysis */
+ alarmStatuses: statusesEntry;
+}
+
+/** Loose decoder for `functionStatsData` */
+export const jFunctionStatsData: Json.Loose<functionStatsData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey<'#fundec'>('#fundec'),'#fundec expected'),
+ coverage: Json.jFail(
+ Json.jObject({
+ reachable: Json.jFail(Json.jNumber,'Number expected'),
+ dead: Json.jFail(Json.jNumber,'Number expected'),
+ }),'Record expected'),
+ alarmCount: Json.jList(jAlarmEntry),
+ alarmStatuses: jStatusesEntrySafe,
+ });
+
+/** Safe decoder for `functionStatsData` */
+export const jFunctionStatsDataSafe: Json.Safe<functionStatsData> =
+ Json.jFail(jFunctionStatsData,'FunctionStatsData expected');
+
+/** Natural order for `functionStatsData` */
+export const byFunctionStatsData: Compare.Order<functionStatsData> =
+ Compare.byFields
+ <{ key: Json.key<'#fundec'>,
+ coverage: { reachable: number, dead: number },
+ alarmCount: alarmEntry[], alarmStatuses: statusesEntry }>({
+ key: Compare.string,
+ coverage: Compare.byFields
+ <{ reachable: number, dead: number }>({
+ reachable: Compare.number,
+ dead: Compare.number,
+ }),
+ alarmCount: Compare.array(byAlarmEntry),
+ alarmStatuses: byStatusesEntry,
+ });
+
+/** Signal for array [`functionStats`](#functionstats) */
+export const signalFunctionStats: Server.Signal = {
+ name: 'plugins.eva.general.signalFunctionStats',
+};
+
+const reloadFunctionStats_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.reloadFunctionStats',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Force full reload for array [`functionStats`](#functionstats) */
+export const reloadFunctionStats: Server.GetRequest<null,null>= reloadFunctionStats_internal;
+
+const fetchFunctionStats_internal: Server.GetRequest<
+ number,
+ { pending: number, updated: functionStatsData[],
+ removed: Json.key<'#fundec'>[], reload: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.fetchFunctionStats',
+ input: Json.jNumber,
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jFunctionStatsData),
+ removed: Json.jList(Json.jKey<'#fundec'>('#fundec')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
+ signals: [],
+};
+/** Data fetcher for array [`functionStats`](#functionstats) */
+export const fetchFunctionStats: Server.GetRequest<
+ number,
+ { pending: number, updated: functionStatsData[],
+ removed: Json.key<'#fundec'>[], reload: boolean }
+ >= fetchFunctionStats_internal;
+
+const functionStats_internal: State.Array<
+ Json.key<'#fundec'>,
+ functionStatsData
+ > = {
+ name: 'plugins.eva.general.functionStats',
+ getkey: ((d:functionStatsData) => d.key),
+ signal: signalFunctionStats,
+ fetch: fetchFunctionStats,
+ reload: reloadFunctionStats,
+ order: byFunctionStatsData,
+};
+/** Statistics about the last Eva analysis for each function */
+export const functionStats: State.Array<
+ Json.key<'#fundec'>,
+ functionStatsData
+ > = functionStats_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index 7705b8ee8164ece05300b1d18e364bbb333391c0..6c94aedd8590d7a3f1b80d699a6f1fadaa192c48 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -33,7 +33,7 @@ import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
import { functions, functionsData } from 'frama-c/api/kernel/ast';
-import { isComputed } from 'frama-c/api/plugins/eva/general';
+import { computationState } from 'frama-c/api/plugins/eva/general';
// --------------------------------------------------------------------------
// --- Global Search Hints
@@ -115,7 +115,7 @@ export default () => {
useFlipSettings('ivette.globals.evaonly', false);
const multipleSelection = selection?.multiple;
const multipleSelectionActive = multipleSelection?.allSelections.length > 0;
- const evaComputed = States.useRequest(isComputed, null);
+ const evaComputed = States.useSyncValue(computationState) === 'computed';
function isSelected(fct: functionsData) {
return multipleSelection?.allSelections.some(
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..bbcaf416ec8c4a32b31bd81ece002e2965f8b0ab
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/.eslintrc.js
@@ -0,0 +1,26 @@
+module.exports = {
+ root: true,
+ overrides: [
+ {
+ files: ['*.js', '*.jsx', '*.ts', '*.tsx'],
+ excludedFiles: 'Summary.tsx|Coverage.tsx|CoverageMeter.tsx',
+ extends: ["../../../../.eslintrc.js"]
+ },
+ {
+ files: ['Summary.tsx','Coverage.tsx'],
+ extends: [
+ 'eslint:recommended',
+ 'plugin:react/recommended',
+ 'plugin:react-hooks/recommended',
+ 'plugin:@typescript-eslint/eslint-recommended',
+ 'plugin:@typescript-eslint/recommended',
+ ],
+ rules: {
+ "@typescript-eslint/explicit-function-return-type": [
+ "error",
+ { allowExpressions: true }
+ ]
+ }
+ }
+ ]
+};
diff --git a/ivette/src/frama-c/plugins/eva/Coverage.tsx b/ivette/src/frama-c/plugins/eva/Coverage.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..e07e8b7a4298985fc098afe56d2c45a86ef41c35
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/Coverage.tsx
@@ -0,0 +1,195 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import React from 'react';
+import * as Json from 'dome/data/json';
+import { Table, Column } from 'dome/table/views';
+import { CompactModel } from 'dome/table/arrays';
+import * as Arrays from 'dome/table/arrays';
+import * as Compare from 'dome/data/compare';
+import * as Ivette from 'ivette';
+import * as States from 'frama-c/states';
+
+import * as Eva from 'frama-c/api/plugins/eva/general';
+import CoverageMeter, { percent } from './CoverageMeter';
+
+type key = Json.key<'#fct'>;
+type stats = Eva.functionStatsData;
+
+// --- Coverage Table ---
+
+const ordering: Arrays.ByColumns<stats> = {
+ fct: Compare.byFields({ key: Compare.string }),
+ alarms: Compare.byFields({
+ alarmStatuses: Compare.lift(
+ (x) => x.unknown + x.invalid,
+ Compare.number,
+ ),
+ }),
+ sureAlarms: Compare.byFields(
+ { alarmStatuses: Compare.byFields({ invalid: Compare.number }) },
+ ),
+ deadStatements: Compare.byFields({
+ coverage: Compare.byFields(
+ { dead: Compare.number },
+ ),
+ }),
+ reachableStatements: Compare.byFields({
+ coverage: Compare.byFields(
+ { reachable: Compare.number },
+ ),
+ }),
+ totalStatements: Compare.byFields(
+ { coverage: Compare.lift((x) => x.reachable + x.dead, Compare.number) },
+ ),
+ coverage: Compare.byFields(
+ {
+ coverage: Compare.lift(
+ (x) => x.reachable / (x.reachable + x.dead),
+ Compare.number,
+ ),
+ },
+ ),
+};
+
+class Model extends CompactModel<key, stats> {
+ constructor() {
+ super(Eva.functionStats.getkey);
+ this.setColumnOrder(ordering);
+ this.setSorting({ sortBy: 'coverage', sortDirection: 'ASC' });
+ }
+}
+
+export function CoverageTable(): JSX.Element {
+ const data = States.useSyncArray(Eva.functionStats).getArray();
+ const [selection, updateSelection] = States.useSelection();
+
+ const model = React.useMemo(() => new Model(), []);
+ React.useEffect(() => model.replaceAllDataWith(data), [model, data]);
+
+ const onSelection = ({ key }: stats): void => {
+ updateSelection({ location: { fct: key } });
+ };
+
+ return (
+ <Table
+ model={model}
+ sorting={model}
+ selection={selection?.current?.fct}
+ onSelection={onSelection}
+ settings="ivette.coverage.table"
+ >
+ <Column
+ id="fct"
+ label="Function"
+ align="left"
+ width={200}
+ fill
+ getter={({ key }: stats) => key}
+ />
+ <Column
+ id="alarms"
+ label="Alarms"
+ title="Number of alarms emitted by the Eva analysis"
+ align="center"
+ width={80}
+ getter={({ alarmStatuses }: stats) => (
+ alarmStatuses.invalid + alarmStatuses.unknown
+ )}
+ />
+ <Column
+ id="sureAlarms"
+ label="Sure alarms"
+ title="Number of sure alarms emitted by the Eva analysis"
+ align="center"
+ width={80}
+ getter={({ alarmStatuses }: stats) => alarmStatuses.invalid}
+ />
+ <Column
+ id="deadStatements"
+ label="Dead"
+ title="Number of statements unreachable to the Eva analysis"
+ align="center"
+ visible={false}
+ width={80}
+ getter={({ coverage }: stats) => coverage.dead}
+ />
+ <Column
+ id="reachableStatements"
+ label="Reachable"
+ title="Number of statements reached by the Eva analysis"
+ align="center"
+ visible={false}
+ width={80}
+ getter={({ coverage }: stats) => coverage.reachable}
+ />
+ <Column
+ id="totalStatements"
+ label="Total"
+ title="Total number of statements"
+ align="center"
+ visible={false}
+ width={80}
+ getter={({ coverage }: stats) => coverage.dead + coverage.reachable}
+ />
+ <Column
+ id="coverage"
+ label="Coverage"
+ title="Coverage of the Eva analysis"
+ align="center"
+ width={80}
+ getter={({ coverage }: stats) => coverage}
+ render={(coverage) => <>{percent(coverage)}</>}
+ />
+ <Column
+ id="coverage-meter"
+ label=""
+ align="center"
+ width={80}
+ getter={({ coverage }: stats) => coverage}
+ render={(coverage) => (<CoverageMeter coverage={coverage} />)}
+ />
+ </Table>
+ );
+}
+
+// --- Coverage Component ---
+
+export default function CoverageComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <CoverageTable />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.eva_coverage',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'Eva Coverage',
+ title: 'Detailed coverage of the Eva analysis',
+ children: <CoverageComponent />,
+});
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx b/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..39537a19e5caa644252dad7992792ca5405b203c
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx
@@ -0,0 +1,48 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import React from 'react';
+
+export interface Coverage {
+ reachable: number;
+ dead: number;
+}
+
+export function percent(coverage: Coverage): string {
+ const q = coverage.reachable / (coverage.reachable + coverage.dead);
+ return `${(q * 100).toFixed(1)}%`;
+}
+
+export default function (props: {coverage: Coverage}) {
+ const { reachable, dead } = props.coverage;
+ const total = reachable + dead;
+
+ return (
+ <meter
+ min={0}
+ max={total}
+ low={0.8 * total}
+ optimum={total}
+ value={reachable}
+ />
+ );
+}
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..0a48090a333743f2cb7e381f6ac695e34648d8ef
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/Summary.tsx
@@ -0,0 +1,259 @@
+/* ************************************************************************ */
+/* */
+/* 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 * as States from 'frama-c/states';
+import * as Eva from 'frama-c/api/plugins/eva/general';
+
+import { LED } from 'dome/controls/buttons';
+
+import CoverageMeter, { percent } from './CoverageMeter';
+
+import './summary.css';
+
+function CoverageTable(data: Eva.programStatsType): JSX.Element {
+ const { progFunCoverage: functions, progStmtCoverage: statements } = data;
+ const functionsTotal = functions.reachable + functions.dead;
+ const statementsTotal = statements.reachable + statements.dead;
+ return (
+ <table className="coverage-table">
+ <thead>
+ <tr>
+ <th aria-label="Category" />
+ <th>Analyzed</th>
+ <th>Total</th>
+ <th>Coverage</th>
+ <th aria-label="Coverage Meter" />
+ </tr>
+ </thead>
+ <tbody>
+ <tr>
+ <th>Functions</th>
+ <td>{functions.reachable}</td>
+ <td>{functionsTotal}</td>
+ <td>{percent(functions)}</td>
+ <td>
+ <CoverageMeter coverage={functions} />
+ </td>
+ </tr>
+ <tr>
+ <th>Statements</th>
+ <td>{statements.reachable}</td>
+ <td>{statementsTotal}</td>
+ <td>{percent(statements)}</td>
+ <td>
+ <CoverageMeter coverage={statements} />
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ );
+}
+
+function plural(count: number): string {
+ return count === 1 ? '' : 's';
+}
+
+function Errors(data: Eva.programStatsType): JSX.Element {
+ const { evaEvents: eva, kernelEvents: 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 className="errors-table">
+ <thead>
+ <tr>
+ <th aria-label="Plugin" />
+ <th>Errors</th>
+ <th>Warnings</th>
+ </tr>
+ </thead>
+ <tbody>
+ <tr>
+ <th>Eva analyzer</th>
+ <td>{eva.errors}</td>
+ <td>{eva.warnings}</td>
+ </tr>
+ <tr>
+ <th>Frama-C kernel</th>
+ <td>{kernel.errors}</td>
+ <td>{kernel.warnings}</td>
+ </tr>
+ </tbody>
+ </table>
+ </>
+ ) :
+ <>No errors or warnings raised during the analysis.</>
+ );
+}
+
+function Alarms(data: Eva.programStatsType,
+ categories: Map<string, States.Tag>): JSX.Element {
+ const { progAlarms, alarmsStatuses: { invalid, unknown } } = data;
+ const total = unknown + invalid;
+
+ const label = (category: Eva.alarmCategory): string | undefined => (
+ categories.get(category)?.descr
+ );
+
+ function order(e1: Eva.alarmEntry, e2: Eva.alarmEntry): number {
+ const { other } = Eva.alarmCategory;
+ const d = e2.count - e1.count;
+ if (e1.category === other && e2.category === other)
+ return d;
+ if (e1.category === other)
+ return 1;
+ if (e2.category === other)
+ return -1;
+ return d || Eva.byAlarmCategory(e1.category, e2.category);
+ }
+
+ return (
+ <>
+ <span>{total}</span> alarm{plural(total)} generated by the analysis :
+ <table className="alarms-table">
+ <tbody>
+ {progAlarms.sort(order).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.programStatsType): JSX.Element {
+ const { assertionsStatuses: assertions, precondsStatuses: preconds } = data;
+ const all = (entry: Eva.statusesEntry): number => (
+ entry.valid + entry.unknown + entry.invalid
+ );
+ const totalAssertions = all(assertions);
+ const totalPreconds = all(preconds);
+ const total = totalAssertions + totalPreconds;
+ if (total > 0) {
+ return (
+ <>
+ <table className="statuses-table">
+ <thead>
+ <tr>
+ <th aria-label="Kind" />
+ <th>Valid</th>
+ <th>Unknown</th>
+ <th>Invalid</th>
+ <th>Total</th>
+ </tr>
+ </thead>
+ <tbody>
+ <tr>
+ <th>Assertions</th>
+ <td>{assertions.valid}</td>
+ <td>{assertions.unknown}</td>
+ <td>{assertions.invalid}</td>
+ <td>{totalAssertions}</td>
+ </tr>
+ <tr>
+ <th>Preconditions</th>
+ <td>{preconds.valid}</td>
+ <td>{preconds.unknown}</td>
+ <td>{preconds.invalid}</td>
+ <td>{totalPreconds}</td>
+ </tr>
+ </tbody>
+ </table>
+ </>
+ );
+ }
+
+ 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.programStats);
+ const state = States.useSyncValue(Eva.computationState);
+
+ if (state === 'not_computed')
+ return (
+ <div className="eva-summary-status">
+ No Eva analysis has been run yet.
+ </div>
+ );
+
+ if (state === 'computing')
+ return (
+ <div className="eva-summary-status">
+ <LED status="active" blink />
+ Eva analysis in progress…
+ </div>
+ );
+
+ if (state === 'computed' && data && alarmCategories)
+ return (
+ <div className="eva-summary-box">
+ <div className="eva-summary">
+ <h1>Analysis Summary</h1>
+ <h2>Coverage</h2>
+ {CoverageTable(data)}
+ <h2>Errors</h2>
+ {Errors(data)}
+ <h2>Alarms</h2>
+ {Alarms(data, alarmCategories)}
+ <h2>Statuses</h2>
+ {Statuses(data)}
+ </div>
+ </div>
+ );
+
+ return (<></>);
+}
+
+function EvaSummaryComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <EvaSummary />
+ </>
+ );
+}
+
+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/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 9f2c3c733ab8443c010bf7f0a7f1cc1c05993a7a..1d862289c35dc1f6a34b170c85f4fd23e2894a5c 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -36,6 +36,8 @@ import { AutoSizer } from 'react-virtualized';
import { ProbeInfos } from './probeinfos';
import { Dimension, ValuesPanel } from './valuetable';
import { AlarmsInfos, StackInfos } from './valueinfos';
+import { } from './Summary';
+import { } from './Coverage';
import './style.css';
// --------------------------------------------------------------------------
@@ -90,6 +92,16 @@ Ivette.registerComponent({
children: <ValuesComponent />,
});
+Ivette.registerView({
+ id: 'summary',
+ rank: 1,
+ label: 'Eva Summary',
+ layout: [
+ ['frama-c.plugins.eva_summary', 'frama-c.plugins.eva_coverage'],
+ 'frama-c.messages',
+ ],
+});
+
Ivette.registerView({
id: 'values',
rank: 1,
diff --git a/ivette/src/frama-c/plugins/eva/summary.css b/ivette/src/frama-c/plugins/eva/summary.css
new file mode 100644
index 0000000000000000000000000000000000000000..41de1d074404dafbeb6a92b09769ffeed566c2dc
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/summary.css
@@ -0,0 +1,100 @@
+.eva-summary-status {
+ margin: auto;
+}
+
+.eva-summary-status .dome-xButton-led {
+ display: inline-block;
+ vertical-align: baseline;
+}
+
+.eva-summary-box {
+ background-color: white;
+ height: 100%;
+ width: 100%;
+ display: flex;
+ flex-direction: column;
+ flex-wrap: wrap;
+ align-items: center;
+ justify-content: center;
+ overflow: auto;
+}
+
+.eva-summary {
+ min-height: 0px;
+ user-select: text;
+}
+
+.eva-summary * {
+ user-select: auto;
+}
+
+.eva-summary span {
+ font-weight: bold;
+}
+
+.eva-summary h1 {
+ margin: 4px;
+}
+
+.eva-summary h2 {
+ margin: 20px 4px 8px;
+}
+
+.eva-summary table {
+ border-collapse: collapse;
+ width: auto;
+ margin: 6px;
+}
+
+.eva-summary thead th {
+ border-bottom: 1px solid black;
+ padding: 2px 8px;
+}
+
+.eva-summary tbody th {
+ text-align: left;
+ font-weight: normal;
+}
+
+.eva-summary tbody td {
+ text-align: center;
+}
+
+.eva-summary .coverage-table td {
+ position: relative;
+}
+
+.eva-summary .coverage-table td * {
+ z-index: 1;
+}
+
+.eva-summary .coverage-table .progress {
+ position: absolute;
+ z-index: 0;
+}
+
+.eva-summary .alarms-table tr:nth-child(2n) {
+ background-color: #eee;
+}
+
+.eva-summary .alarms-table td:nth-child(1) {
+ text-align: right;
+}
+
+.eva-summary .alarms-table td:nth-child(2) {
+ text-align: left;
+}
+
+.eva-summary .statuses-table tr :nth-child(5) {
+ background-color: #ddd;
+}
+
+.eva-summary td {
+ padding: 2px 6px;
+}
+
+
+.eva-summary thead tr td {
+ border-bottom: 1px solid black;
+}
+
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index bd94ad5e2bfd7874bb4f732a53e09629c823d2e3..f242dde7e2b1e5c815a8f9ab1166db6a1e7adad4 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -119,7 +119,7 @@ module Ref
include Info
val default: unit -> Data.t
end)
- : Ref with type data = Data.t
+ : Ref with type data = Data.t and type Datatype.t = Data.t ref
(** Output signature of [Option_ref]. Note that [get] will raise [Not_found]
if the stored data is [None]. Use [get_option] if you want to have
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index 36f7c9648b859d37d957e47a97582ffb50813080..9cbac7e0bd89681ea0bf5c1fbfbecd6ff16fa7b3 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
@@ -30,8 +30,8 @@
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
5 alarms generated by the analysis:
- 1 invalid memory access
3 integer overflows
+ 1 invalid memory access
1 access to uninitialized left-values
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index 6136cebc45ed92fb5908b315bfd4e1c9ac6d7b2c..8d646242f63b276a80e5b1aecbe4798c58561b3d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -26,8 +26,8 @@
[eva] ====== VALUES COMPUTED ======
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 5 functions analyzed (out of 5): 100% coverage.
- In these functions, 27 statements reached (out of 27): 100% coverage.
+ 3 functions analyzed (out of 5): 60% coverage.
+ In these functions, 23 statements reached (out of 23): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 7ce9dd03cc6ed5e4235edfdc1d544b0471ae871b..d130f00bdd88864d88d5c8d2e04a0efd66d398e8 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -375,6 +375,19 @@ struct
with Not_found -> Data.failure "Undefined function '%s'" key
end
+module Fundec =
+struct
+ type t = fundec
+ let jtype = Pkg.Jkey "fundec"
+ let to_json fundec =
+ `String fundec.svar.vname
+ let of_json js =
+ let key = Js.to_string js in
+ try Kernel_function.get_definition (Globals.Functions.find_by_name key)
+ with Not_found | Kernel_function.No_Definition ->
+ Data.failure "Undefined function definition '%s'" key
+end
+
module KfMarker = struct
type record
let record : record Record.signature = Record.signature ()
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index d85697dec6786bf566dabe44780959aa27ab7572..e0cc3e7007dc8c3d38cfca3c0c23c4c01ee23279 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -30,6 +30,7 @@ open Cil_types
module Position : Data.S with type t = Filepath.position
module Kf : Data.S with type t = kernel_function
+module Fundec : Data.S with type t = fundec
module Ki : Data.S with type t = kinstr
module Stmt : Data.S with type t = stmt
module Lval : Data.S with type t = kinstr * lval
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index 08317ce24c1dedfc8c886a18d943acd41ca9c62c..bf2edda269cc7b43711570e2ed71afceea3d1ded 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -37,7 +37,7 @@ let install signal hook = function
in Request.on_signal signal install
let install_emit signal add_hook =
- install signal (fun () -> Request.emit signal) add_hook
+ install signal (fun _ -> Request.emit signal) add_hook
(* -------------------------------------------------------------------------- *)
(* --- Values --- *)
@@ -45,7 +45,7 @@ let install_emit signal add_hook =
let register_value (type a) ~package ~name ~descr
~(output : a Request.output) ~get
- ?(add_hook : unit callback option) ()
+ ?(add_hook : 'b callback option) ()
=
let open Markdown in
let href = link ~name () in
@@ -68,7 +68,7 @@ let register_value (type a) ~package ~name ~descr
let register_state (type a) ~package ~name ~descr
~(data : a data) ~get ~set
- ?(add_hook : unit callback option) () =
+ ?(add_hook : 'b callback option) () =
let open Markdown in
let module D = (val data) in
let href = link ~name () in
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
index 1285874ffe93828ccebc0362f28d4abb65ad5cd1..2ae32160c807bcd45e27f225aeeb153c29b923ba 100644
--- a/src/plugins/server/states.mli
+++ b/src/plugins/server/states.mli
@@ -44,7 +44,7 @@ val register_value :
descr:Markdown.text ->
output:'a Request.output ->
get:(unit -> 'a) ->
- ?add_hook:(unit callback) ->
+ ?add_hook:('b callback) ->
unit -> Request.signal
(** Register a (projectified) state and generates the associated signal and
@@ -67,7 +67,7 @@ val register_state :
data:'a Data.data ->
get:(unit -> 'a) ->
set:('a -> unit) ->
- ?add_hook:(unit callback) ->
+ ?add_hook:('b callback) ->
unit -> Request.signal
type 'a model (** Columns array model *)
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 283e6dbac434a63b4ab21abc0806b80ed26a4609..1b226d8e8d271a6d3b5a718d3b81e5c33d6c96e8 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -31,11 +31,30 @@ let package =
~readme:"eva.md"
()
-let () = Request.register ~package
- ~kind:`GET ~name:"isComputed"
- ~descr:(Markdown.plain "True if the Eva analysis has been done")
- ~input:(module Data.Junit) ~output:(module Data.Jbool)
- Db.Value.is_computed
+module ComputationState = struct
+ type t = Analysis.computation_state
+ let jtype =
+ Data.declare ~package
+ ~name:"computationStateType"
+ ~descr:(Markdown.plain "State of the computation of Eva Analysis.")
+ Package.(Junion [
+ Jtag "not_computed" ;
+ Jtag "computing" ;
+ Jtag "computed"])
+ let to_json = function
+ | Analysis.NotComputed -> `String "not_computed"
+ | Computing -> `String "computing"
+ | Computed -> `String "computed"
+end
+
+let _computation_signal =
+ States.register_value ~package
+ ~name:"computationState"
+ ~descr:(Markdown.plain "The current computation state of the analysis.")
+ ~output:(module ComputationState)
+ ~get:Analysis.current_computation_state
+ ~add_hook:Analysis.register_computation_hook
+ ()
let is_computed kf =
Db.Value.is_computed () &&
@@ -206,4 +225,214 @@ 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
+ | Summary.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
+ | Summary.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
+ | Summary.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 = Summary.alarm_category)
+end
+
+module Coverage =
+struct
+ open Summary
+ type t = coverage
+ let jtype = Package.(
+ Jrecord [
+ "reachable",Jnumber ;
+ "dead",Jnumber ;
+ ])
+ let to_json x = `Assoc [
+ "reachable", `Int x.reachable ;
+ "dead", `Int x.dead ;
+ ]
+end
+
+module Events =
+struct
+ open Summary
+ let jtype = Package.(
+ Jrecord [
+ "errors",Jnumber ;
+ "warnings",Jnumber ;
+ ])
+ let to_json x = `Assoc [
+ "errors", `Int x.errors ;
+ "warnings", `Int x.warnings ;
+ ]
+end
+
+module Statuses =
+struct
+ open Summary
+ type t = statuses
+ 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 AlarmEntry =
+struct
+ let jtype =
+ Data.declare ~package
+ ~name:"alarmEntry"
+ ~descr:(Markdown.plain "Alarm count for each alarm category.")
+ Package.(Jrecord [
+ "category", AlarmCategory.jtype ;
+ "count", Jnumber ])
+ let to_json (a,c) = `Assoc [
+ "category", AlarmCategory.to_json a ;
+ "count", `Int c ]
+end
+
+module Alarms =
+struct
+ type t = (AlarmCategory.t * int) list
+ let jtype = Package.Jlist AlarmEntry.jtype
+ let to_json x = `List (List.map AlarmEntry.to_json x)
+end
+
+module Statistics = struct
+ open Summary
+ type t = program_stats
+ let jtype =
+ Data.declare ~package
+ ~name:"programStatsType"
+ ~descr:(Markdown.plain "Statistics about an Eva analysis.")
+ Package.(Jrecord [
+ "progFunCoverage",Coverage.jtype ;
+ "progStmtCoverage",Coverage.jtype ;
+ "progAlarms", Alarms.jtype ;
+ "evaEvents",Events.jtype ;
+ "kernelEvents",Events.jtype ;
+ "alarmsStatuses",Statuses.jtype ;
+ "assertionsStatuses",Statuses.jtype ;
+ "precondsStatuses",Statuses.jtype ])
+ let to_json x = `Assoc [
+ "progFunCoverage", Coverage.to_json x.prog_fun_coverage ;
+ "progStmtCoverage", Coverage.to_json x.prog_stmt_coverage ;
+ "progAlarms", Alarms.to_json x.prog_alarms ;
+ "evaEvents", Events.to_json x.eva_events ;
+ "kernelEvents", Events.to_json x.kernel_events ;
+ "alarmsStatuses", Statuses.to_json x.alarms_statuses ;
+ "assertionsStatuses", Statuses.to_json x.assertions_statuses ;
+ "precondsStatuses", Statuses.to_json x.preconds_statuses ]
+end
+
+let _computed_signal =
+ States.register_value ~package
+ ~name:"programStats"
+ ~descr:(Markdown.plain
+ "Statistics about the last Eva analysis for the whole program")
+ ~output:(module Statistics)
+ ~get:Summary.compute_stats
+ ~add_hook:(Analysis.register_computation_hook ~on:Computed)
+ ()
+
+let _array =
+ let open Summary in
+ let model = States.model () in
+
+ States.column model ~name:"coverage"
+ ~descr:(Markdown.plain "Coverage of the Eva analysis")
+ ~data:(module Coverage)
+ ~get:(fun (_kf,stats) -> stats.fun_coverage);
+
+ States.column model ~name:"alarmCount"
+ ~descr:(Markdown.plain "Alarms raised by the Eva analysis by category")
+ ~data:(module Alarms)
+ ~get:(fun (_kf,stats) -> stats.fun_alarm_count);
+
+ States.column model ~name:"alarmStatuses"
+ ~descr:(Markdown.plain "Alarms statuses emitted by the Eva analysis")
+ ~data:(module Statuses)
+ ~get:(fun (_kf,stats) -> stats.fun_alarm_statuses);
+
+ States.register_array
+ ~package
+ ~name:"functionStats"
+ ~descr:(Markdown.plain
+ "Statistics about the last Eva analysis for each function")
+ ~key:(fun (fundec,_stats) -> fundec.svar.vname)
+ ~keyType:Kernel_ast.Fundec.jtype
+ ~iter:(fun f -> FunctionStats.iter (fun fundec s -> f (fundec,s)))
+ ~add_update_hook:FunctionStats.register_hook
+ model
+
+
(**************************************************************************)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 5255b073cb68c0b0ef716e2e3c8dfc86c5e07516..1aae152c818918c1ab13ee8d0ebaa22514a15857 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -60,7 +60,8 @@ type domain = {
let signal = Request.signal ~package ~name:"changed"
~descr:(Md.plain "Emitted when EVA results has changed")
-let () = Analysis.register_computed_hook (fun () -> Request.emit signal)
+let () = Analysis.register_computation_hook ~on:Computed
+ (fun _ -> Request.emit signal)
(* -------------------------------------------------------------------------- *)
(* --- Marker Utilities --- *)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 278bc97910dc0f96eb7e802376af28b857875e4d..7fde8c2e3ddfee761223d62b4148c34b596a9994 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -114,6 +114,35 @@ module Default =
: Analyzer)
+(* Current state of the analysis *)
+type computation_state = NotComputed | Computing | Computed
+
+module ComputationState =
+struct
+ let to_string = function
+ | NotComputed -> "NotComputed"
+ | Computing -> "Computing"
+ | Computed -> "Computed"
+
+ module Prototype =
+ struct
+ include Datatype.Serializable_undefined
+ type t = computation_state
+ let name = "Eva.Analysis.ComputationState"
+ let pretty fmt s = Format.pp_print_string fmt (to_string s)
+ let reprs = [ NotComputed ; Computing ; Computed ]
+ let dependencies = [ Db.Value.self ]
+ let default () = NotComputed
+ end
+
+ module Datatype' = Datatype.Make (Prototype)
+ module Hook = Hook.Build (Prototype)
+ include (State_builder.Ref (Datatype') (Prototype))
+
+ let set s = set s; Hook.apply s
+ let () = add_hook_on_update (fun r -> Hook.apply !r)
+end
+
(* Reference to the current configuration (built by Abstractions.configure from
the parameters of Eva regarding the abstractions used in the analysis) and
the current Analyzer module. *)
@@ -127,22 +156,27 @@ let current_analyzer () = (module (val (snd !ref_analyzer)): S)
Useful for the GUI parts that depend on it. *)
module Analyzer_Hook = Hook.Build (struct type t = (module S) end)
-(* Set of hooks called whenever the current Analyzer is computed.
- Useful for the GUI parts that depend on it. *)
-module Computed_Hook = Hook.Build (struct type t = unit end)
-
(* Register a new hook. *)
let register_hook = Analyzer_Hook.extend
-(* Register a new computed hook. *)
-let register_computed_hook = Computed_Hook.extend
-
(* Sets the current Analyzer module for a given configuration.
Calls the hooks above. *)
let set_current_analyzer config (analyzer: (module Analyzer)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
+(* Get the current computation state. *)
+let current_computation_state () =
+ ComputationState.get ()
+
+(* Register a hook on current computation state *)
+let register_computation_hook ?on f =
+ let f' = match on with
+ | None -> f
+ | Some s -> fun s' -> if s = s' then f s
+ in
+ ComputationState.Hook.extend f'
+
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
let _, lib_entry = Globals.entry_point () in
@@ -177,9 +211,10 @@ let force_compute () =
Eva_audit.check_configuration (Kernel.AuditCheck.get ());
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
+ ComputationState.set Computing; (* The new analyzer can be accesed through hooks *)
let module Analyzer = (val snd !ref_analyzer) in
Analyzer.compute_from_entry_point ~lib_entry kf ;
- Computed_Hook.apply ()
+ ComputationState.set Computed
(* Resets the Analyzer when the current project is changed. *)
let () =
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 732d307bd553273534ddd69ed306215b42a5a19e..2a6e647e5fc99a01f8172413e7cfa25721fb7b86 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -70,9 +70,18 @@ val register_hook: ((module S) -> unit) -> unit
is changed. This happens when a new analysis is run with different
abstractions than before, or when the current project is changed. *)
-val register_computed_hook: (unit -> unit) -> unit
-(** Registers a hook that will be called each time the [current] analyzer
- has been computed. *)
+type computation_state = NotComputed | Computing | Computed
+(** Computation state of the analysis. *)
+
+val current_computation_state : unit -> computation_state
+(** Get the current computation state of the analysis, updated by
+ [force_compute] and states updates. *)
+
+val register_computation_hook: ?on:computation_state ->
+ (computation_state -> unit) -> unit
+(** Registers a hook that will be called each time the analysis starts or
+ finishes. If [on] is given, the hook will only be called when the
+ analysis switches to this specific state. *)
val force_compute : unit -> unit
(** Perform a full analysis, starting from the [main] function. *)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index a932d0eebdcf98c0dc1a21575316dd7a9cb5208b..5d0cf41b0baab78657e85110dd86b5c3bd2cae33 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -201,9 +201,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Library_functions.warn_unsupported_spec vi.vorig_name;
Spec.compute_using_specification ~warn:true call_kinstr call spec state,
Eval.Cacheable
- | `Def _fundec ->
+ | `Def fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
- Computer.compute kf call_kinstr state
+ let result = Computer.compute kf call_kinstr state in
+ Summary.FunctionStats.recompute fundec;
+ result
in
if pp then
Value_parameters.feedback
@@ -349,7 +351,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
Abstract.Dom.post_analysis final_state;
- Value_results.print_summary ();
+ Summary.print_summary ();
restore_signals ()
in
let cleanup () =
diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1429c0262b314bff082b941cf0e2fe9d495a1245
--- /dev/null
+++ b/src/plugins/value/utils/summary.ml
@@ -0,0 +1,432 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Types *)
+
+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
+ let equal c1 c2 = id c1 = id c2
+ let hash c = id c
+end
+
+type coverage =
+ { mutable reachable: int;
+ mutable dead: int; }
+
+type statuses =
+ { mutable valid: int;
+ mutable unknown: int;
+ mutable invalid: int; }
+
+type events =
+ { mutable errors: int;
+ mutable warnings: int; }
+
+type alarms = (alarm_category * int) list (* Alarm count for each category *)
+
+type fun_stats =
+ { fun_coverage: coverage;
+ fun_alarm_count: alarms;
+ fun_alarm_statuses: statuses; }
+
+type program_stats =
+ { prog_fun_coverage: coverage;
+ prog_stmt_coverage: coverage;
+ prog_alarms: alarms;
+ eva_events: events;
+ kernel_events: events;
+ alarms_statuses: statuses;
+ assertions_statuses: statuses;
+ preconds_statuses: statuses; }
+
+module AlarmsStats =
+struct
+ include Hashtbl.Make (AlarmCategory)
+
+ let get t a = try find t a with Not_found -> 0
+ let add t a c = replace t a (get t a + c)
+ let incr t a = add t a 1
+ let to_list t = fold (fun a c l -> (a,c) :: l) t []
+ let add_list t l = List.iter (fun (a,c) -> add t a c) l
+end
+
+
+(* --- Datatypes --- *)
+
+module Coverage = struct
+ let make () =
+ { reachable = 0;
+ dead = 0; }
+ let total c = c.reachable + c.dead
+ let incr c ~reachable = match reachable with
+ | false -> c.dead <- c.dead + 1
+ | true -> c.reachable <- c.reachable + 1
+ let add c1 c2 =
+ c1.reachable <- c1.reachable + c2.reachable;
+ c1.dead <- c1.dead + c2.dead
+end
+
+module Statuses = struct
+ let make () =
+ { valid = 0;
+ unknown = 0;
+ invalid = 0; }
+ let total c = c.valid + c.unknown + c.invalid
+ let incr c = function
+ | Property_status.Dont_know -> c.unknown <- c.unknown + 1
+ | Property_status.True -> c.valid <- c.valid + 1
+ | Property_status.False_if_reachable
+ | Property_status.False_and_reachable -> c.invalid <- c.invalid + 1
+end
+
+module Events = struct
+ let make () =
+ { errors = 0;
+ warnings = 0; }
+ let total c = c.errors + c.warnings
+end
+
+(* --- Function stats computation --- *)
+
+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
+ then Some status
+ else acc
+ in
+ Property_status.fold_on_statuses aux_status ip None
+
+let compute_fun_stats fundec =
+ let alarms = AlarmsStats.create 13
+ and coverage = Coverage.make ()
+ and statuses = Statuses.make ()
+ in
+ let kf = Globals.Functions.get fundec.Cil_types.svar in
+ let do_status alarm ip =
+ match get_status ip with
+ | None -> ()
+ | Some status ->
+ Statuses.incr statuses status;
+ match status with
+ | Property_status.True -> ()
+ | _ -> AlarmsStats.incr alarms (AlarmCategory.of_alarm alarm)
+ in
+ let do_annot stmt _emitter annotation =
+ match Alarms.find annotation with
+ | None -> ()
+ | Some alarm ->
+ let l = Property.ip_of_code_annot kf stmt annotation in
+ List.iter (do_status alarm) l
+ in
+ let do_stmt stmt =
+ let reachable = Db.Value.is_reachable_stmt stmt in
+ Coverage.incr coverage ~reachable;
+ Annotations.iter_code_annot (do_annot stmt) stmt
+ in
+ List.iter do_stmt fundec.Cil_types.sallstmts;
+ { fun_coverage = coverage;
+ fun_alarm_count = AlarmsStats.to_list alarms;
+ fun_alarm_statuses = statuses; }
+
+
+module FunctionStats_Type = Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ type t = fun_stats
+ let name = "Eva.Summary.FunctionStats_Type"
+ let reprs = [{
+ fun_coverage = Coverage.make ();
+ fun_alarm_count = [];
+ fun_alarm_statuses = Statuses.make ();
+ }]
+ end)
+
+module FunctionStats = struct
+ include State_builder.Hashtbl
+ (Cil_datatype.Fundec.Hashtbl)
+ (FunctionStats_Type)
+ (struct
+ let name = "Eva.Summary.FunctionStats"
+ let dependencies = [ Db.Value.self ]
+ let size = 17
+ end)
+
+ module Hook = Hook.Build (struct
+ type t = Cil_types.fundec * fun_stats
+ end)
+
+ let compute kf =
+ let stats = compute_fun_stats kf in
+ Hook.apply (kf,stats);
+ stats
+ let get kf =
+ try Some (find kf)
+ with Not_found -> None
+ let recompute kf = replace kf (compute kf)
+ let register_hook = Hook.extend
+end
+
+
+(* --- Program stats computation --- *)
+
+let consider_function vi =
+ vi.Cil_types.vdefined &&
+ not (Cil_builtins.is_builtin vi
+ || Cil_builtins.is_special_builtin vi.vname
+ || Cil.is_in_libc vi.vattr)
+
+let compute_events () =
+ let eva = Events.make () and kernel = Events.make () in
+ let 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 eva
+ | Warning, name when name = Log.kernel_label_name ->
+ incr_warn kernel
+ | Error, "eva" when event.evt_category <> Some "alarm" ->
+ incr_err eva
+ | Error, name when name = Log.kernel_label_name ->
+ incr_warn kernel
+ | _ -> ()
+ in
+ Messages.iter do_event;
+ eva, kernel
+
+let compute_statuses () =
+ let alarms = Statuses.make ()
+ and assertions = Statuses.make ()
+ and preconds = Statuses.make ()
+ in
+ let do_property ip =
+ let incr stmt statuses =
+ if Db.Value.is_reachable_stmt stmt then
+ match get_status ip with
+ | None -> ()
+ | Some status -> Statuses.incr statuses status
+ in
+ match ip with
+ | Property.IPCodeAnnot Property.{ica_ca; ica_stmt} ->
+ begin
+ match Alarms.find ica_ca with
+ | None -> incr ica_stmt assertions
+ | Some _alarm -> incr ica_stmt alarms
+ end
+ | Property.IPPropertyInstance {Property.ii_stmt} ->
+ incr ii_stmt preconds
+ | _ -> ()
+ in
+ Property_status.iter do_property;
+ alarms, assertions, preconds
+
+let compute_stats () =
+ let prog_fun_coverage = Coverage.make ()
+ and prog_stmt_coverage = Coverage.make ()
+ and prog_alarms = AlarmsStats.create 131
+ in
+ let do_fun fundec =
+ let consider = consider_function fundec.Cil_types.svar in
+ match FunctionStats.get fundec with
+ | Some fun_stats ->
+ AlarmsStats.add_list prog_alarms fun_stats.fun_alarm_count;
+ if consider then
+ begin
+ Coverage.incr prog_fun_coverage ~reachable:true;
+ Coverage.add prog_stmt_coverage fun_stats.fun_coverage;
+ end
+ | None ->
+ if consider then Coverage.incr prog_fun_coverage ~reachable:false;
+ in
+ Globals.Functions.iter_on_fundecs do_fun;
+ let alarms_statuses, assertions_statuses, preconds_statuses =
+ compute_statuses ()
+ and eva_events, kernel_events = compute_events () in
+ { prog_fun_coverage;
+ prog_stmt_coverage;
+ prog_alarms=AlarmsStats.to_list prog_alarms;
+ eva_events;
+ kernel_events;
+ alarms_statuses;
+ assertions_statuses;
+ preconds_statuses; }
+
+
+(* --- Printing --- *)
+
+let plural count = if count = 1 then "" else "s"
+
+let print_coverage fmt {prog_fun_coverage=funs; prog_stmt_coverage=stmts} =
+ let funs_total = Coverage.total funs
+ and stmts_total = Coverage.total stmts in
+ if funs_total = 0
+ then Format.fprintf fmt "No function to be analyzed.@;"
+ else
+ Format.fprintf fmt
+ "%i function%s analyzed (out of %i): %i%% coverage.@;"
+ funs.reachable (plural funs.reachable) funs_total
+ (funs.reachable * 100 / funs_total);
+ if funs_total > 0 && stmts_total > 0 then
+ Format.fprintf fmt
+ "In %s, %i statements reached (out of %i): %i%% coverage.@;"
+ (if funs.reachable > 1 then "these functions" else "this function")
+ stmts.reachable stmts_total
+ (stmts.reachable * 100 / stmts_total)
+
+let print_events fmt stats =
+ if Events.total stats.eva_events + Events.total stats.kernel_events = 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 {prog_alarms; alarms_statuses} =
+ let total = Statuses.total alarms_statuses in
+ Format.fprintf fmt "%i alarm%s generated by the analysis" total (plural total);
+ match prog_alarms with
+ | [] | [Other,_] ->
+ Format.fprintf fmt ".@;"
+ | _many_alarms_categories ->
+ let order x1 x2 =
+ match x1, x2 with
+ | (Other,c1), (Other,c2) -> c2 - c1
+ | (Other,_), _ -> 1 (* "Other" at the end *)
+ | _, (Other,_) -> -1
+ | (a1,c1), (a2,c2) ->
+ (* Descending count order *)
+ let d = c2 - c1 in
+ if d <> 0 then d else AlarmCategory.compare a1 a2
+ in
+ Format.fprintf fmt ":@;";
+ List.iter (print_alarm fmt) (List.sort order prog_alarms);
+ let invalid = alarms_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_statuses fmt {assertions_statuses; preconds_statuses} =
+ let total_assertions = Statuses.total assertions_statuses
+ and total_preconds = Statuses.total preconds_statuses in
+ let total = total_assertions + total_preconds in
+ if total = 0
+ then
+ Format.fprintf fmt
+ "No logical properties have been reached by the analysis.@;"
+ else
+ 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;
+ in
+ Format.fprintf fmt
+ "Evaluation of the logical properties reached by the analysis:@;";
+ print_line "Assertions" assertions_statuses total_assertions;
+ print_line "Preconditions" preconds_statuses total_preconds;
+ let proven = assertions_statuses.valid + preconds_statuses.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 stats = compute_stats () in
+ Format.fprintf fmt "%s@;" bar;
+ print_coverage fmt stats;
+ Format.fprintf fmt "%s@;" bar;
+ print_events fmt stats;
+ Format.fprintf fmt "%s@;" bar;
+ print_alarms fmt stats;
+ Format.fprintf fmt "%s@;" bar;
+ print_statuses fmt stats;
+ Format.fprintf fmt "%s" bar
+
+let print_summary () =
+ let dkey = Value_parameters.dkey_summary in
+ let header fmt = Format.fprintf fmt " ====== ANALYSIS SUMMARY ======" in
+ Value_parameters.printf ~header ~dkey ~level:1 " @[<v>%t@]" print_summary
diff --git a/src/plugins/value/utils/summary.mli b/src/plugins/value/utils/summary.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a0e912834d72d655bd40c7b91dd9cca6a8b763cf
--- /dev/null
+++ b/src/plugins/value/utils/summary.mli
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** {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
+
+type coverage =
+ { mutable reachable: int;
+ mutable dead: int; }
+
+type statuses =
+ { mutable valid: int;
+ mutable unknown: int;
+ mutable invalid: int; }
+
+type events =
+ { mutable errors: int;
+ mutable warnings: int; }
+
+type alarms = (alarm_category * int) list (* Alarm count for each category *)
+
+type fun_stats =
+ { fun_coverage: coverage;
+ fun_alarm_count: alarms;
+ fun_alarm_statuses: statuses; }
+
+type program_stats =
+ { prog_fun_coverage: coverage;
+ prog_stmt_coverage: coverage;
+ prog_alarms: alarms;
+ eva_events: events;
+ kernel_events: events;
+ alarms_statuses: statuses;
+ assertions_statuses: statuses;
+ preconds_statuses: statuses; }
+
+module FunctionStats : sig
+ (** Get the current analysis statistics for a function *)
+ val get: Cil_types.fundec -> fun_stats option
+
+ (** Iterate on every function statistics *)
+ val iter: (Cil_types.fundec -> fun_stats -> unit) -> unit
+
+ (** Trigger the recomputation of function stats *)
+ val recompute: Cil_types.fundec -> unit
+
+ (** Set a hook on function statistics computation *)
+ val register_hook: (Cil_types.fundec * fun_stats -> unit) -> unit
+end
+
+(** Compute analysis statistics. *)
+val compute_stats: unit -> program_stats
+
+(** Prints a summary of the analysis. *)
+val print_summary: unit -> unit
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 9ca7a64e5c07ea32af4db09682dae6ed5049fc82..d8dfd0c0fd3dda6aa95f9695d5df5a2829b5de77 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -351,240 +351,6 @@ 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
-
-let plural count = if count = 1 then "" else "s"
-
-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 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 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
- in
- incr counter
-
-let eva_emitter = Value_util.emitter
-
-let get_status ip =
- let aux_status emitter status acc =
- let emitter = Emitter.Usable_emitter.get emitter.Property_status.emitter in
- if Emitter.equal eva_emitter emitter
- then Some status
- else acc
- in
- Property_status.fold_on_statuses aux_status ip None
-
-let report_status acc = function
- | None -> ()
- | Some status -> match status with
- | Property_status.Dont_know -> incr acc.unknown
- | Property_status.True -> incr acc.valid
- | 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 =
- 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
- | Some alarm ->
- let acc_status, acc_alarms = report.alarms in
- report_status acc_status status;
- match status with
- | None | Some Property_status.True -> ()
- | _ -> report_alarm acc_alarms alarm
- end
- | Property.IPPropertyInstance {Property.ii_stmt}
- when Db.Value.is_reachable_stmt ii_stmt ->
- report_status report.preconds (get_status ip)
- | _ -> ()
- 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
- Format.fprintf fmt "%i alarm%s generated by the analysis" total (plural total);
- if total = !(kind.others)
- then Format.fprintf fmt ".@;"
- else Format.fprintf fmt ":@;%a" print_alarms_kind kind;
- let invalid = !(alarms.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 total_assertions = total assertions
- and total_preconds = total preconds in
- let total = total_assertions + total_preconds in
- if total = 0
- then
- Format.fprintf fmt
- "No logical properties have been reached by the analysis.@;"
- else
- 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;
- 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 = 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
- Format.fprintf fmt "%s@;" bar;
- print_coverage fmt;
- Format.fprintf fmt "%s@;" bar;
- print_warning fmt;
- Format.fprintf fmt "%s@;" bar;
- print_alarms fmt report;
- Format.fprintf fmt "%s@;" bar;
- print_properties fmt report;
- Format.fprintf fmt "%s" bar
-
-let print_summary () =
- let dkey = Value_parameters.dkey_summary in
- let header fmt = Format.fprintf fmt " ====== ANALYSIS SUMMARY ======" in
- Value_parameters.printf ~header ~dkey ~level:1 " @[<v>%t@]" print_summary
(*
Local Variables:
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/value_results.mli
index 512f45ebeb52538dd4963d1f659172fd9e1c56b2..9592d1e753f5eda07466e46e263863f903648115 100644
--- a/src/plugins/value/utils/value_results.mli
+++ b/src/plugins/value/utils/value_results.mli
@@ -26,6 +26,7 @@
open Cil_types
+val is_called: kernel_function -> bool
val mark_kf_as_called: kernel_function -> unit
val add_kf_caller: caller:kernel_function * stmt -> kernel_function -> unit
@@ -46,9 +47,6 @@ val change_callstacks:
For technical reasons, the top of the callstack must currently
be preserved. *)
-(** Prints a summary of the analysis. *)
-val print_summary: unit -> unit
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index f93e7228b403b708b01b4386186ab29d200d1a5a..4fc947aed52f0310962541382bab507065ba34a8 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -30,8 +30,8 @@
__retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 25 statements reached (out of 28): 89% coverage.
+ 2 functions analyzed (out of 3): 66% coverage.
+ In these functions, 25 statements reached (out of 25): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 8c983fd90a289be87579fd40cfe9efbde6414a90..4a16459c438b0638d3dd1a9422243ea203352ec3 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -91,14 +91,14 @@
by the Frama-C kernel: 0 errors 2 warnings
----------------------------------------------------------------------------
17 alarms generated by the analysis:
- 1 division by zero
+ 3 integer overflows
2 invalid memory accesses
2 accesses out of bounds index
- 3 integer overflows
2 invalid shifts
- 1 escaping address
2 nan or infinite floating-point values
2 illegal conversions from floating-point to integer
+ 1 division by zero
+ 1 escaping address
2 others
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 7bfb7aff0243d6fb76ac66ee9a5adf16a98cbed9..df409d8f59baf69c3c876cc5f95c465c3cbdf979 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -114,14 +114,14 @@
by the Frama-C kernel: 0 errors 2 warnings
----------------------------------------------------------------------------
18 alarms generated by the analysis:
- 1 division by zero
3 invalid memory accesses
- 2 accesses out of bounds index
3 integer overflows
+ 2 accesses out of bounds index
2 invalid shifts
- 1 escaping address
2 nan or infinite floating-point values
2 illegal conversions from floating-point to integer
+ 1 division by zero
+ 1 escaping address
2 others
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis: