diff --git a/Makefile b/Makefile
index abe001d1968d1b5f6f6d7fc925d3ef641eb3bc8d..9af6317689253cc9dbda1c8f09bc45b47fbbd540 100644
--- a/Makefile
+++ b/Makefile
@@ -784,7 +784,7 @@ PLUGIN_NAME:=Metrics
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/metrics
PLUGIN_CMO:= metrics_parameters css_html metrics_base metrics_acsl \
- metrics_cabs metrics_cilast metrics_coverage \
+ metrics_cabs metrics_cilast metrics_coverage metrics_pivot \
register
PLUGIN_GUI_CMO:= metrics_gui register_gui
PLUGIN_DEPENDENCIES:=Eva
diff --git a/configure.in b/configure.in
index 54d56f2f332a02e82021d094e5031ac2a9be11d3..faaf96d4eca57a97b791b6d0c7ceeb19c930740c 100644
--- a/configure.in
+++ b/configure.in
@@ -783,6 +783,7 @@ plugin_require(inout,callgraph)
#########
check_plugin(metrics,src/plugins/metrics,[support for metrics analysis],yes)
+plugin_require(metrics,server)
plugin_require(metrics,eva)
plugin_use(metrics,gui)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 0e4ca8c9bb2c2a828b8de118b3d1431e3a5fde9d..0d0c951d48b04dbdbd428528415e6281ccd9258c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1009,6 +1009,8 @@ src/plugins/metrics/metrics_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/metrics/metrics_pivot.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/metrics/metrics_pivot.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/ivette/Makefile.distrib b/ivette/Makefile.distrib
index b6773e8d65d31dead54e2e1d96a427e3edee939d..02f7a024dc5194201d7e70a2f91dccd5494d7ee7 100644
--- a/ivette/Makefile.distrib
+++ b/ivette/Makefile.distrib
@@ -147,6 +147,7 @@ DISTRIB_FILES += ivette/src/frama-c/api/generated/kernel/services/index.ts
DISTRIB_FILES += ivette/src/frama-c/api/generated/plugins/dive/index.ts
DISTRIB_FILES += ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
DISTRIB_FILES += ivette/src/frama-c/api/generated/plugins/eva/values/index.ts
+DISTRIB_FILES += ivette/src/frama-c/api/generated/plugins/pivot/general/index.ts
DISTRIB_FILES += ivette/src/frama-c/api/generated/plugins/studia/studia/index.ts
DISTRIB_FILES += ivette/src/frama-c/api/generator.ml
DISTRIB_FILES += ivette/src/frama-c/client.ts
@@ -159,6 +160,7 @@ DISTRIB_FILES += ivette/src/frama-c/kernel/Globals.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/History.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/Locations.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/Messages.tsx
+DISTRIB_FILES += ivette/src/frama-c/kernel/PivotTable.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/Properties.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/SourceCode.tsx
DISTRIB_FILES += ivette/src/frama-c/kernel/Status.tsx
@@ -189,6 +191,7 @@ DISTRIB_FILES += ivette/src/frama-c/plugins/eva/style.css
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/summary.css
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valueinfos.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valuetable.tsx
+DISTRIB_FILES += ivette/src/frama-c/react-pivottable.d.ts
DISTRIB_FILES += ivette/src/frama-c/server.ts
DISTRIB_FILES += ivette/src/frama-c/states.ts
DISTRIB_FILES += ivette/src/frama-c/utils.ts
diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt
index c89734b28035fc538a00d3b922ea4237fefe1aea..b41ae593231fac45596038d840bcc09628aefa98 100644
--- a/ivette/headers/header_spec.txt
+++ b/ivette/headers/header_spec.txt
@@ -147,6 +147,7 @@ src/frama-c/api/generated/kernel/services/index.ts: CEA_LGPL
src/frama-c/api/generated/plugins/dive/index.ts: CEA_LGPL
src/frama-c/api/generated/plugins/eva/general/index.ts: CEA_LGPL
src/frama-c/api/generated/plugins/eva/values/index.ts: CEA_LGPL
+src/frama-c/api/generated/plugins/pivot/general/index.ts: CEA_LGPL
src/frama-c/api/generated/plugins/studia/studia/index.ts: CEA_LGPL
src/frama-c/api/generator.ml: .ignore
src/frama-c/client.ts: CEA_LGPL
@@ -159,6 +160,7 @@ src/frama-c/kernel/Globals.tsx: CEA_LGPL
src/frama-c/kernel/History.tsx: CEA_LGPL
src/frama-c/kernel/Locations.tsx: CEA_LGPL
src/frama-c/kernel/Messages.tsx: CEA_LGPL
+src/frama-c/kernel/PivotTable.tsx: CEA_LGPL
src/frama-c/kernel/Properties.tsx: CEA_LGPL
src/frama-c/kernel/SourceCode.tsx: CEA_LGPL
src/frama-c/kernel/Status.tsx: CEA_LGPL
@@ -189,6 +191,7 @@ src/frama-c/plugins/eva/style.css: .ignore
src/frama-c/plugins/eva/summary.css: .ignore
src/frama-c/plugins/eva/valueinfos.tsx: CEA_LGPL
src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL
+src/frama-c/react-pivottable.d.ts: CEA_LGPL
src/frama-c/server.ts: CEA_LGPL
src/frama-c/states.ts: CEA_LGPL
src/frama-c/utils.ts: CEA_LGPL
diff --git a/ivette/package.json b/ivette/package.json
index 52655b7d59c4bec9f1c4207977f1c0733d76dad1..33b452fc4f9efd8d3f9bd8f481787e3c1b8b66af 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -75,6 +75,7 @@
"react-dom": "^16",
"react-draggable": "^4.4.4",
"react-fast-compare": "^3.2.0",
+ "react-pivottable": "^0.11.0",
"react-virtualized": "^9.22.3",
"react-window": "",
"source-map-support": "^0.5.21",
diff --git a/ivette/src/frama-c/api/generated/plugins/pivot/general/index.ts b/ivette/src/frama-c/api/generated/plugins/pivot/general/index.ts
new file mode 100644
index 0000000000000000000000000000000000000000..16efe72359dd0a0c80f98eab75fc0e2ffae21baf
--- /dev/null
+++ b/ivette/src/frama-c/api/generated/plugins/pivot/general/index.ts
@@ -0,0 +1,89 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+/* --- Generated Frama-C Server API --- */
+
+/**
+ Pivot Table Services
+ @packageDocumentation
+ @module frama-c/api/plugins/pivot/general
+*/
+
+//@ts-ignore
+import * as Json from 'dome/data/json';
+//@ts-ignore
+import * as Compare from 'dome/data/compare';
+//@ts-ignore
+import * as Server from 'frama-c/server';
+//@ts-ignore
+import * as State from 'frama-c/states';
+
+
+/** State of the pivot table source data. */
+export type tableStateType = string[][];
+
+/** Safe decoder for `tableStateType` */
+export const jTableStateTypeSafe: Json.Safe<tableStateType> =
+ Json.jArray(Json.jArray(Json.jFail(Json.jString,'String expected')));
+
+/** Loose decoder for `tableStateType` */
+export const jTableStateType: Json.Loose<tableStateType> =
+ Json.jTry(jTableStateTypeSafe);
+
+/** Natural order for `tableStateType` */
+export const byTableStateType: Compare.Order<tableStateType> =
+ Compare.array(Compare.array(Compare.string));
+
+/** Signal for state [`pivotState`](#pivotstate) */
+export const signalPivotState: Server.Signal = {
+ name: 'plugins.pivot.general.signalPivotState',
+};
+
+const getPivotState_internal: Server.GetRequest<null,tableStateType> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.pivot.general.getPivotState',
+ input: Json.jNull,
+ output: jTableStateType,
+ signals: [],
+};
+/** Getter for state [`pivotState`](#pivotstate) */
+export const getPivotState: Server.GetRequest<null,tableStateType>= getPivotState_internal;
+
+const pivotState_internal: State.Value<tableStateType> = {
+ name: 'plugins.pivot.general.pivotState',
+ signal: signalPivotState,
+ getter: getPivotState,
+};
+/** State of the pivot table source data. */
+export const pivotState: State.Value<tableStateType> = pivotState_internal;
+
+const compute_internal: Server.ExecRequest<null,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.pivot.general.compute',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Computes the pivot table. */
+export const compute: Server.ExecRequest<null,null>= compute_internal;
+
+/* ------------------------------------- */
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index ecdd4f2fd82278d3e7e1e09a2aa92189dc0518c9..cbd203691f69193bd4f1eb1e0dc2002be378c02c 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -33,6 +33,7 @@ import Status from 'frama-c/kernel/Status';
import ASTview from 'frama-c/kernel/ASTview';
import ASTinfo from 'frama-c/kernel/ASTinfo';
import SourceCode from 'frama-c/kernel/SourceCode';
+import PivotTable from 'frama-c/kernel/PivotTable';
import Locations from 'frama-c/kernel/Locations';
import Properties from 'frama-c/kernel/Properties';
import Messages from 'frama-c/kernel/Messages';
@@ -90,6 +91,12 @@ Ivette.registerGroup({
title: 'Messages emitted by Frama-C',
children: <Messages />,
});
+ Ivette.registerComponent({
+ id: 'frama-c.pivottable',
+ label: 'Pivot Table',
+ title: 'Pivot Table',
+ children: <PivotTable />,
+ });
});
/* --------------------------------------------------------------------------*/
@@ -115,4 +122,13 @@ Ivette.registerView({
],
});
+Ivette.registerView({
+ id: 'pivot-table',
+ rank: 2,
+ label: 'Pivot Table',
+ layout: [
+ ['frama-c.pivottable'],
+ ],
+});
+
/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/kernel/PivotTable.tsx b/ivette/src/frama-c/kernel/PivotTable.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..28d3865a677283ca852d45949ea1313e97810195
--- /dev/null
+++ b/ivette/src/frama-c/kernel/PivotTable.tsx
@@ -0,0 +1,129 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Pivot Table
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import { TitleBar } from 'ivette';
+import * as Server from 'frama-c/server';
+import { Button } from 'dome/controls/buttons';
+import { LED } from 'dome/controls/displays';
+import { Scroll } from 'dome/layout/boxes';
+import * as Status from 'frama-c/kernel/Status';
+import * as States from 'frama-c/states';
+import * as PivotState from 'frama-c/api/plugins/pivot/general';
+import PivotTableUI from 'react-pivottable/PivotTableUI';
+import 'react-pivottable/pivottable.css';
+
+// --------------------------------------------------------------------------
+// --- Pivot Table for Properties
+// --------------------------------------------------------------------------
+
+interface PivotTableProps {
+ data: string[][];
+}
+
+export function Pivot(props: PivotTableProps) : JSX.Element {
+ const [state, setState] = React.useState({});
+ return (
+ <PivotTableUI
+ data={props.data}
+ onChange={setState}
+ {...state}
+ />
+ );
+}
+
+function PivotTable (rawData: PivotState.tableStateType): JSX.Element {
+ const data = new Array(rawData.length > 0 ? rawData.length - 1 : 0);
+ if (rawData.length > 0) {
+ const headers = rawData[0];
+ for (let i = 1; i < rawData.length; i++) {
+ const src = rawData[i];
+ data[i - 1] = {};
+ for (let j = 0; j < headers.length; j++) {
+ data[i - 1][headers[j]] = src[j];
+ }
+ }
+ }
+ return (<Pivot data={data} />);
+}
+
+function PivotTableBuild () : JSX.Element {
+ const rawData = States.useSyncValue(PivotState.pivotState);
+ const [computing, setComputing] = React.useState(false);
+ const [error, setError] = React.useState('');
+ async function handleError (err: string) : Promise<void> {
+ const msg =
+ `The pivot table could not be built: an error has occured (${err}).`;
+ setError(msg);
+ Status.setMessage({ text: msg, kind: 'error' });
+ }
+ async function compute () : Promise<void> {
+ setComputing(true);
+ setError('');
+ Server.send(PivotState.compute, [])
+ .then(() => setComputing(false))
+ .catch((err) => { setComputing(false); handleError(err); });
+ }
+ if (rawData && rawData.length > 0) {
+ return (PivotTable(rawData));
+ }
+ if (computing) {
+ return (
+ <div className="pivot-centered">
+ <div>
+ <LED status="active" blink /> Computing…
+ </div>
+ </div>
+ );
+ }
+ const err = error ? <div className="part"> {error} </div> : undefined;
+ return (
+ <div className="pivot-centered">
+ {err}
+ <div className="part">
+ <Button
+ icon="EXECUTE"
+ label="Compute"
+ title="Builds the pivot table. This may take a few moments."
+ onClick={ compute }
+ />
+ </div>
+ </div>
+ );
+}
+
+export default function PivotTableComponent () : JSX.Element {
+ return (
+ <>
+ <TitleBar />
+ <Scroll>
+ <PivotTableBuild />
+ </Scroll>
+ </>
+ );
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index 8b8b0435238982f4201588f9a930c83850d3f9a2..295008738903d77b302382ab92371a4d20bf5ecb 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -103,5 +103,30 @@
white-space: pre-line;
}
+/* -------------------------------------------------------------------------- */
+/* --- Pivot table --- */
+/* -------------------------------------------------------------------------- */
+
+.pivot-centered {
+ user-select: text;
+ display: flex;
+ flex-wrap: wrap;
+ flex-direction: column;
+ justify-content: center;
+ align-content: center;
+ height: 80%;
+}
+
+.pivot-centered .part {
+ user-select: text;
+ margin-top: 10px;
+ margin-bottom: 10px;
+ text-align: center;
+}
+
+.pivot-centered .dome-xButton-led {
+ display: inline-block;
+ vertical-align: baseline;
+}
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/react-pivottable.d.ts b/ivette/src/frama-c/react-pivottable.d.ts
new file mode 100644
index 0000000000000000000000000000000000000000..69405ebe30afd6ccfd34a8248511096bf09ad711
--- /dev/null
+++ b/ivette/src/frama-c/react-pivottable.d.ts
@@ -0,0 +1,23 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+declare module 'react-pivottable/PivotTableUI';
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index cf9d9194ab96324c64e326719d726c7346dcf010..c423bf7fe1d48d7ea40479de19ef7cbb61633836 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -2571,6 +2571,11 @@ class-utils@^0.3.5:
isobject "^3.0.0"
static-extend "^0.1.1"
+classnames@^2.2.5:
+ version "2.3.1"
+ resolved "https://registry.yarnpkg.com/classnames/-/classnames-2.3.1.tgz#dfcfa3891e306ec1dad105d0e88f4417b8535e8e"
+ integrity sha512-OlQdbZ7gLfGarSqxesMesDa5uz7KFbID8Kpq/SxIoNGDqY8lSYs0D+hhtBXhcdB3rcbXArFr7vlHheLk1voeNA==
+
clean-css@^4.2.3:
version "4.2.4"
resolved "https://registry.yarnpkg.com/clean-css/-/clean-css-4.2.4.tgz#733bf46eba4e607c6891ea57c24a989356831178"
@@ -5054,6 +5059,13 @@ immediate@~3.0.5:
resolved "https://registry.yarnpkg.com/immediate/-/immediate-3.0.6.tgz#9db1dbd0faf8de6fbe0f5dd5e56bb606280de69b"
integrity sha1-nbHb0Pr43m++D13V5Wu2BigN5ps=
+immutability-helper@^2.3.1:
+ version "2.9.1"
+ resolved "https://registry.yarnpkg.com/immutability-helper/-/immutability-helper-2.9.1.tgz#71c423ba387e67b6c6ceba0650572f2a2a6727df"
+ integrity sha512-r/RmRG8xO06s/k+PIaif2r5rGc3j4Yhc01jSBfwPCXDLYZwp/yxralI37Df1mwmuzcCsen/E/ITKcTEvc1PQmQ==
+ dependencies:
+ invariant "^2.2.0"
+
immutable@:
version "4.0.0"
resolved "https://registry.yarnpkg.com/immutable/-/immutable-4.0.0.tgz#b86f78de6adef3608395efb269a91462797e2c23"
@@ -5150,6 +5162,13 @@ interpret@^1.4.0:
resolved "https://registry.yarnpkg.com/interpret/-/interpret-1.4.0.tgz#665ab8bc4da27a774a40584e812e3e0fa45b1a1e"
integrity sha512-agE4QfB2Lkp9uICn7BAqoscw4SZP9kTE2hxiFI3jBPmXJfdqiahTbUuKGsMoN2GtqL9AxhYioAcVvgsb1HvRbA==
+invariant@^2.2.0:
+ version "2.2.4"
+ resolved "https://registry.yarnpkg.com/invariant/-/invariant-2.2.4.tgz#610f3c92c9359ce1db616e538008d23ff35158e6"
+ integrity sha512-phJfQVBuaJM5raOpJjSfkiD6BpbCE4Ns//LaXl6wGYtUBY83nWS6Rf9tXm2e8VaK60JEjYldbPif/A2B1C2gNA==
+ dependencies:
+ loose-envify "^1.0.0"
+
ip-regex@^2.1.0:
version "2.1.0"
resolved "https://registry.yarnpkg.com/ip-regex/-/ip-regex-2.1.0.tgz#fa78bf5d2e6913c911ce9f819ee5146bb6d844e9"
@@ -5843,7 +5862,7 @@ loglevel@^1.6.8:
resolved "https://registry.yarnpkg.com/loglevel/-/loglevel-1.8.0.tgz#e7ec73a57e1e7b419cb6c6ac06bf050b67356114"
integrity sha512-G6A/nJLRgWOuuwdNuA6koovfEV1YpqqAG4pRUlFaz3jj2QNZ8M4vBqnVA+HBTmU/AMNUtlOsMmSpF6NyOjztbA==
-loose-envify@^1.1.0, loose-envify@^1.4.0:
+loose-envify@^1.0.0, loose-envify@^1.1.0, loose-envify@^1.4.0:
version "1.4.0"
resolved "https://registry.yarnpkg.com/loose-envify/-/loose-envify-1.4.0.tgz#71ee51fa7be4caec1a63839f7e682d8132d30caf"
integrity sha512-lyuxPGr/Wfhrlem2CL/UcnUc1zcqKAImBDzukY7Y5F/yQiNdko6+fRLevlw1HgMySw7f611UIY408EtxRSoK3Q==
@@ -6988,6 +7007,15 @@ promise-inflight@^1.0.1:
resolved "https://registry.yarnpkg.com/promise-inflight/-/promise-inflight-1.0.1.tgz#98472870bf228132fcbdd868129bad12c3c029e3"
integrity sha1-mEcocL8igTL8vdhoEputEsPAKeM=
+prop-types@>=15.0.0, prop-types@^15.5.10:
+ version "15.8.1"
+ resolved "https://registry.yarnpkg.com/prop-types/-/prop-types-15.8.1.tgz#67d87bf1a694f48435cf332c24af10214a3140b5"
+ integrity sha512-oj87CgZICdulUohogVAR7AjlC0327U4el4L6eAvOqCeudMDVU0NThNaV+b9Df4dXgSP1gXMTnPdhfe/2qDH5cg==
+ dependencies:
+ loose-envify "^1.4.0"
+ object-assign "^4.1.1"
+ react-is "^16.13.1"
+
prop-types@^15.6.0, prop-types@^15.6.1, prop-types@^15.6.2, prop-types@^15.7.2:
version "15.7.2"
resolved "https://registry.yarnpkg.com/prop-types/-/prop-types-15.7.2.tgz#52c41e75b8c87e72b9d9360e0206b99dcbffa6c5"
@@ -7170,6 +7198,14 @@ react-dom@^16:
prop-types "^15.6.2"
scheduler "^0.19.1"
+react-draggable@^3.0.3:
+ version "3.3.2"
+ resolved "https://registry.yarnpkg.com/react-draggable/-/react-draggable-3.3.2.tgz#966ef1d90f2387af3c2d8bd3516f601ea42ca359"
+ integrity sha512-oaz8a6enjbPtx5qb0oDWxtDNuybOylvto1QLydsXgKmwT7e3GXC2eMVDwEMIUYJIFqVG72XpOv673UuuAq6LhA==
+ dependencies:
+ classnames "^2.2.5"
+ prop-types "^15.6.0"
+
react-draggable@^4.4.4:
version "4.4.4"
resolved "https://registry.yarnpkg.com/react-draggable/-/react-draggable-4.4.4.tgz#5b26d9996be63d32d285a426f41055de87e59b2f"
@@ -7197,7 +7233,7 @@ react-hot-loader@^4:
shallowequal "^1.1.0"
source-map "^0.7.3"
-react-is@^16.7.0, react-is@^16.8.1:
+react-is@^16.13.1, react-is@^16.7.0, react-is@^16.8.1:
version "16.13.1"
resolved "https://registry.yarnpkg.com/react-is/-/react-is-16.13.1.tgz#789729a4dc36de2999dc156dd6c1d9c18cea56a4"
integrity sha512-24e6ynE2H+OKt4kqsOvNd8kBpV65zoxbA4BVsEOB3ARVWQki/DHzaUoC5KuON/BiccDaCCTZBuOcfZs70kR8bQ==
@@ -7207,6 +7243,24 @@ react-lifecycles-compat@^3.0.4:
resolved "https://registry.yarnpkg.com/react-lifecycles-compat/-/react-lifecycles-compat-3.0.4.tgz#4f1a273afdfc8f3488a8c516bfda78f872352362"
integrity sha512-fBASbA6LnOU9dOU2eW7aQ8xmYBSXUIWr+UmF9b1efZBazGNO+rcXT/icdKnYm2pTwcRylVUYwW7H1PHfLekVzA==
+react-pivottable@^0.11.0:
+ version "0.11.0"
+ resolved "https://registry.yarnpkg.com/react-pivottable/-/react-pivottable-0.11.0.tgz#2ac9a28db6bdcefdb7bdeeb1ed067df229bb9dd8"
+ integrity sha512-hFU10XYL28NWVRnm+RRyHrzsAn/xIJzPgwPebUE2Hx5JZQl/Zxty3WUL/5cAcdK4AmTb9FQBRopLKLwuiI6VlA==
+ dependencies:
+ immutability-helper "^2.3.1"
+ prop-types "^15.5.10"
+ react-draggable "^3.0.3"
+ react-sortablejs "^1.3.4"
+ sortablejs "^1.6.1"
+
+react-sortablejs@^1.3.4:
+ version "1.5.1"
+ resolved "https://registry.yarnpkg.com/react-sortablejs/-/react-sortablejs-1.5.1.tgz#ba05a554548cf9733cc2d5411ece9b97f911b63e"
+ integrity sha512-bKIc1UVhjZt55Nb6WZFxZ8Jwyngg8CTt+w+iG1pA5k9LQsg1J0X6nLppHatSSDZDECtRZKp2z47tmmhPRJNj4g==
+ dependencies:
+ prop-types ">=15.0.0"
+
react-virtualized@^9.22.3:
version "9.22.3"
resolved "https://registry.yarnpkg.com/react-virtualized/-/react-virtualized-9.22.3.tgz#f430f16beb0a42db420dbd4d340403c0de334421"
@@ -7943,6 +7997,11 @@ sort-keys@^1.0.0:
dependencies:
is-plain-obj "^1.0.0"
+sortablejs@^1.6.1:
+ version "1.14.0"
+ resolved "https://registry.yarnpkg.com/sortablejs/-/sortablejs-1.14.0.tgz#6d2e17ccbdb25f464734df621d4f35d4ab35b3d8"
+ integrity sha512-pBXvQCs5/33fdN1/39pPL0NZF20LeRbLQ5jtnheIPN9JQAaufGjKdWduZn4U7wCtVuzKhmRkI0DFYHYRbB2H1w==
+
source-list-map@^2.0.0:
version "2.0.1"
resolved "https://registry.yarnpkg.com/source-list-map/-/source-list-map-2.0.1.tgz#3993bd873bfc48479cca9ea3a547835c7c154b34"
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 044cf5f450289b8bdbb8b30ca552da416397558c..6a73eae995e2013ed87e6509821403728bd6d297 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -283,7 +283,7 @@
end
(* Update lexer buffer. *)
- let update_line_loc lexbuf line =
+ let update_line_pos lexbuf line =
let pos = lexbuf.Lexing.lex_curr_p in
lexbuf.Lexing.lex_curr_p <-
{ pos with
@@ -291,10 +291,7 @@
Lexing.pos_bol = pos.Lexing.pos_cnum;
}
- let update_newline_loc lexbuf =
- update_line_loc lexbuf (lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum + 1)
-
- let update_file_loc lexbuf file =
+ let update_file_pos lexbuf file =
let pos = lexbuf.Lexing.lex_curr_p in
lexbuf.Lexing.lex_curr_p <- { pos with Lexing.pos_fname = file }
@@ -349,8 +346,8 @@ let utf8_char = ['\128'-'\254']+
rule token = parse
| space+ { token lexbuf }
- | '\n' { update_newline_loc lexbuf; token lexbuf }
- | comment_line '\n' { update_newline_loc lexbuf; token lexbuf }
+ | '\n' { Lexing.new_line lexbuf; token lexbuf }
+ | comment_line '\n' { Lexing.new_line lexbuf; token lexbuf }
| comment_line eof { token lexbuf }
| "*/" { lex_error lexbuf "unexpected block-comment closing" }
| "/*" { if !accept_c_comments_into_acsl_spec
@@ -502,7 +499,7 @@ and chr buffer = parse
| _ { Buffer.add_string buffer (lexeme lexbuf); chr buffer lexbuf }
and hash = parse
- '\n' { update_newline_loc lexbuf; token lexbuf}
+ '\n' { Lexing.new_line lexbuf; token lexbuf}
| [' ''\t'] { hash lexbuf}
| rD+ { (* We are seeing a line number. This is the number for the
* next line *)
@@ -517,14 +514,14 @@ and hash = parse
"Bad line number in preprocessed file: %s" s;
(-1)
in
- update_line_loc lexbuf (lineno - 1);
+ update_line_pos lexbuf (lineno - 1);
(* A file name may follow *)
file lexbuf }
| "line" { hash lexbuf } (* MSVC line number info *)
| _ { endline lexbuf}
and file = parse
- '\n' { update_newline_loc lexbuf; token lexbuf}
+ '\n' { Lexing.new_line lexbuf; token lexbuf}
| [' ''\t''\r'] { file lexbuf}
| '"' ([^ '\012' '\t' '"']|"\\\"")* '"' {
let n = Lexing.lexeme lexbuf in
@@ -532,38 +529,36 @@ and file = parse
((String.length n) - 2) in
let unescape = Str.regexp_string "\\\"" in
let n1 = Str.global_replace unescape "\"" n1 in
- update_file_loc lexbuf n1;
+ update_file_pos lexbuf n1;
endline lexbuf
}
| _ { endline lexbuf}
and endline = parse
- '\n' { update_newline_loc lexbuf; token lexbuf}
+ '\n' { Lexing.new_line lexbuf; token lexbuf}
| eof { EOF }
| _ { endline lexbuf}
and comment = parse
- '\n' { update_newline_loc lexbuf; comment lexbuf}
+ '\n' { Lexing.new_line lexbuf; comment lexbuf}
| "*/" { token lexbuf}
| eof { lex_error lexbuf "non-terminating block-comment" }
| _ { comment lexbuf}
{
- let set_initial_location dest_lexbuf src_loc =
- Lexing.(
- dest_lexbuf.lex_curr_p <-
- { src_loc with
- pos_bol = src_loc.pos_bol - src_loc.pos_cnum;
- pos_cnum = 0; };
- )
-
- let parse_from_location f (loc, s : Filepath.position * string) =
+ (* When Ocaml 4.11+ becomes mandatory, we can probably replace this with
+ Lexing.set_position. *)
+ let set_initial_position dest_lexbuf src_pos =
+ dest_lexbuf.Lexing.lex_curr_p <- src_pos;
+ dest_lexbuf.lex_abs_pos <- src_pos.pos_cnum
+
+ let parse_from_position f (pos, s : Filepath.position * string) =
let finally _ = Logic_utils.exit_kw_c_mode () in
let output = Kernel.logwith finally ~wkey:Kernel.wkey_annot_error
in
let lb = from_string s in
- set_initial_location lb (Cil_datatype.Position.to_lexing_pos loc);
+ set_initial_position lb (Cil_datatype.Position.to_lexing_pos pos);
try
let res = f token lb in
Some (Cil_datatype.Position.of_lexing_pos lb.Lexing.lex_curr_p, res)
@@ -584,11 +579,11 @@ and comment = parse
Kernel.fatal ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "Unknown error (%s)"
(Printexc.to_string exn)
- let lexpr = parse_from_location Logic_parser.lexpr_eof
+ let lexpr = parse_from_position Logic_parser.lexpr_eof
- let annot = parse_from_location Logic_parser.annot
+ let annot = parse_from_position Logic_parser.annot
- let spec = parse_from_location Logic_parser.spec
+ let spec = parse_from_position Logic_parser.spec
let ext_spec lexbuf = try
accept_c_comments_into_acsl_spec := true ;
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f958082d4b04d4d907094cd9ea3fefcb985d5284..264239138bb9d1bc00fe45a8bac7a0e0fd433de1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -59,6 +59,31 @@ let valid_sid = false
open Cil_types
open Cil_datatype
+(* Maps the start and end positions of a function declaration or definition
+ (including its possible contract) to its name. *)
+module FuncLocs = struct
+ include
+ State_builder.List_ref
+ (Datatype.Triple
+ (Cil_datatype.Position)(Cil_datatype.Position)(Datatype.String)
+ )
+ (struct
+ let name = "FuncLocs"
+ let dependencies = [ Kernel.Files.self ]
+ end)
+
+ let add_loc ?spec loc1 loc2 funcname =
+ let startpos =
+ match spec with
+ | None -> fst loc1
+ | Some (_, spec_loc) -> fst spec_loc
+ in
+ let endpos = snd loc2 in
+ add (startpos, endpos, funcname)
+end
+
+let func_locs () = FuncLocs.get ()
+
let stripUnderscore s =
if String.length s = 1 then begin
if s = "_" then
@@ -8613,12 +8638,14 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * C
List.exists (fun (_,el) -> List.exists is_fc_stdlib el) a
in
(* Make a first version of the varinfo *)
+ let vi_loc = convLoc cloc in
let vi = makeVarInfoCabs ~ghost ~isformal:false ~referenced:islibc
- ~isglobal:true ~isgenerated (convLoc cloc) (t,s,b,attr_list) (n,ndt,a)
+ ~isglobal:true ~isgenerated vi_loc (t,s,b,attr_list) (n,ndt,a)
in
(* Add the variable to the environment before doing the initializer
* because it might refer to the variable itself *)
if isFunctionType vi.vtype then begin
+ FuncLocs.add_loc ?spec:logic_spec (CurrentLoc.get ()) vi_loc n;
if inite != Cabs.NO_INIT then
Kernel.error ~once:true ~current:true
"Function declaration with initializer (%s)\n" vi.vname;
@@ -9240,6 +9267,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
Kernel.debug ~dkey:Kernel.dkey_typing_global
"Definition of %s at %a\n" n Cil_printer.pp_location idloc;
CurrentLoc.set idloc;
+ FuncLocs.add_loc ?spec loc1 endloc n;
IH.clear callTempVars;
(* Make the fundec right away, and we'll populate it later. We
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index 44ea2ddf74785720d77ef8af20e9510925f8866b..f15e3a97b31a45f205d88aad2d1c1a375f4b208a 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -280,6 +280,22 @@ val stmtFallsThrough: Cil_types.stmt -> bool
val fieldsToInit: Cil_types.compinfo -> string option -> Cil_types.offset list
+(**
+ Returns a mapping (pos_start, pos_end, funcname) for each function
+ declaration and definition, spanning the entire function, including
+ its specification (if it has one).
+
+ Currently, for function declarations, the location ends at the function
+ name, before the formal parameter list. For definitions, it spans until the
+ closing brace.
+
+ Note that the list is _not_ sorted, and must be further processed
+ for efficient data retrieval.
+
+ @since Frama-C+dev
+*)
+val func_locs : unit -> (Filepath.position * Filepath.position * string) list
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index ee6d4ef5573f305005e6e8ca321218f73bf56986..ef12ae7e9f1918b0e6d6f610be9b26642b78176d 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -206,6 +206,10 @@ module Position = struct
let pp_with_col fmt pos =
Format.fprintf fmt "%a char %d" pretty pos
(pos.Filepath.pos_cnum - pos.Filepath.pos_bol)
+ let pretty_debug fmt pos =
+ Format.fprintf fmt "%a:%d:%d"
+ Datatype.Filepath.pretty pos.Filepath.pos_path
+ pos.Filepath.pos_lnum pos.Filepath.pos_cnum
end
module Location = struct
@@ -242,11 +246,8 @@ module Location = struct
Format.fprintf fmt "generated"
let pretty_debug fmt loc =
- Format.fprintf fmt "(%a:%d:%d,%a:%d:%d)"
- Datatype.Filepath.pretty (fst loc).Filepath.pos_path
- (fst loc).Filepath.pos_lnum (fst loc).Filepath.pos_cnum
- Datatype.Filepath.pretty (snd loc).Filepath.pos_path
- (snd loc).Filepath.pos_lnum (snd loc).Filepath.pos_cnum
+ Format.fprintf fmt "(%a,%a)"
+ Position.pretty_debug (fst loc) Position.pretty_debug (snd loc)
let of_lexing_loc (pos1, pos2) =
Position.of_lexing_pos pos1, Position.of_lexing_pos pos2
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index df5138305b7a051784a19e7f9c6e893383ac0648..f1064f288f97e0a6192087f5def008d9a4ea80ca 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -58,6 +58,11 @@ module Position: sig
val pp_with_col : Format.formatter -> t -> unit
val of_lexing_pos : Lexing.position -> t
val to_lexing_pos : t -> Lexing.position
+
+ (** Pretty-print file, line and character offset.
+ @since Frama-C+dev
+ *)
+ val pretty_debug: t Pretty_utils.formatter
end
(** Cil locations. *)
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
new file mode 100644
index 0000000000000000000000000000000000000000..78cc4db8fb9090341dae3e3b3f7ec0a13f1661ed
--- /dev/null
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -0,0 +1,544 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Data for a GUI-based pivot table *)
+
+open Cil_types
+
+module PivotSourceState =
+ State_builder.List_ref
+ (Datatype.List(Datatype.String))
+ (struct
+ let name = "PivotSourceState"
+ let dependencies = [ Ast.self; Db.Value.self; Property_status.self;
+ Messages.self ]
+ end)
+
+type syntax_domain =
+ | Code
+ | Declaration
+ | Annotation
+
+type message_domain = Log.kind
+
+type domain =
+ | Syntax of syntax_domain
+ | Property
+ | Message of message_domain
+
+let string_of_string_list sep =
+ Format.asprintf "%a"
+ (Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep Format.pp_print_string)
+
+let split_loc (loc : Cil_types.location) =
+ let fp = (fst loc).pos_path in
+ let line = string_of_int (fst loc).pos_lnum in
+ let fp_pretty = Filepath.Normalized.to_pretty_string fp in
+ let dir = Filename.dirname fp_pretty in
+ let name = Filename.basename fp_pretty in
+ let ext = Filename.extension name in
+ dir, name, ext, line
+
+let node_of_instr = function
+ | Set _ -> "assignment"
+ | Call _ -> "call"
+ | Local_init _ -> "local_init"
+ | Asm _ -> "asm"
+ | Skip _ -> "nop"
+ | Code_annot _ ->
+ (* should be done by the annotations visitor *)
+ assert false
+
+let opt_node_of_stmtkind = function
+ | Instr _ -> None
+ | Return (_, _) -> Some "return"
+ | Goto (_, _) -> Some "goto"
+ | Break _ -> Some "break"
+ | Continue _ -> Some "continue"
+ | If (_, _, _, _) -> Some "if"
+ | Switch (_, _, _, _) -> Some "switch"
+ | Loop (_, _, _, _, _) -> Some "loop"
+ | Block _ -> None
+ | UnspecifiedSequence _ -> Some "unspecified_sequence"
+ | Throw (_, _) -> Some "throw"
+ | TryCatch (_, _, _) -> Some "try_catch"
+ | TryFinally (_, _, _) -> Some "try_finally"
+ | TryExcept (_, _, _, _) -> Some "try_except"
+
+let node_of_code_annotation_node = function
+ | AAssert _ -> "assert"
+ | AStmtSpec _ -> "stmt_spec"
+ | AInvariant _ -> "invariant"
+ | AVariant _ -> "variant"
+ | AAssigns _ -> "assigns"
+ | AAllocation _ -> "allocation"
+ | APragma _ -> "ca_pragma"
+ | AExtended _ -> "extended"
+
+let node_of_global_annotation = function
+ | Dfun_or_pred _ -> "logic_fun_or_pred"
+ | Dvolatile _ -> "logic_volatile"
+ | Daxiomatic _ -> "axiomatic"
+ | Dtype _ -> "logic_type"
+ | Dlemma _ -> "logic_lemma"
+ | Dinvariant _ -> "invariant"
+ | Dtype_annot _ -> "type_annot"
+ | Dmodel_annot _ -> "model_annot"
+ | Dextended _ -> "ga_extended"
+
+let domain_and_node_of_global = function
+ | GType _ -> Declaration, "gtype"
+ | GCompTag _ -> Declaration, "gcomptag"
+ | GCompTagDecl _ -> Declaration, "gcomptagdecl"
+ | GEnumTag _ -> Declaration, "genumtag"
+ | GEnumTagDecl _ -> Declaration, "genumtagdecl"
+ | GVarDecl _ -> Declaration, "global_var"
+ | GFunDecl _ -> Declaration, "gfundecl"
+ | GVar _ -> Declaration, "gvar"
+ | GFun _ -> Declaration, "gfun"
+ | GAsm _ -> Code, "gasm"
+ | GPragma _ -> Code, "gpragma"
+ | GText _ -> Code, "gtext"
+ | GAnnot _ -> Code, "gannot"
+
+let names_of_global = function
+ | GType (_, _) -> []
+ | GCompTag (_, _) -> []
+ | GCompTagDecl (_, _) -> []
+ | GEnumTag (_, _) -> []
+ | GEnumTagDecl (_, _) -> []
+ | GVarDecl (vi, _) -> [vi.vname]
+ | GFunDecl (_, vi, _) -> [vi.vname]
+ | GVar (vi, _, _) -> [vi.vname]
+ | GFun ({svar}, _) -> [svar.vname]
+ | GAsm (_, _) -> []
+ | GPragma (_, _) -> []
+ | GText _ -> []
+ | GAnnot (_, _) -> []
+
+let name_of_logic_info li = li.l_var_info.lv_name
+
+let name_of_global_annotation = function
+ | Dvolatile (_, _, _, _, _) -> None
+ | Dfun_or_pred (li, _)
+ | Dinvariant (li, _)
+ | Dtype_annot (li, _) -> Some (name_of_logic_info li)
+ | Daxiomatic (name, _, _, _)
+ | Dtype ({lt_name = name}, _)
+ | Dlemma (name, _, _, _, _, _)
+ | Dmodel_annot ({mi_name = name}, _)
+ | Dextended ({ext_name = name}, _, _) -> Some name
+
+let node_of_predicate_kind = function
+ | Assert -> "assert"
+ | Check -> "check"
+ | Admit -> "admit"
+
+let node_of_property = function
+ | Property.IPPredicate idp ->
+ Format.asprintf "%a" Property.pretty_predicate_kind idp.ip_kind
+ | IPCodeAnnot ica -> node_of_code_annotation_node ica.ica_ca.annot_content
+ | IPAxiomatic _ -> "axiomatic"
+ | IPLemma _ -> "lemma"
+ | IPBehavior _ -> "behavior"
+ | IPComplete _ -> "complete"
+ | IPDisjoint _ -> "disjoint"
+ | IPAllocation _ -> "allocates"
+ | IPAssigns _ -> "assigns"
+ | IPFrom _ -> "from"
+ | IPDecrease _ -> "loop variant"
+ | IPExtended _ -> "extended"
+ | IPReachable _ -> "reachable"
+ | IPPropertyInstance _ -> "instance"
+ | IPTypeInvariant _ -> "type_invariant"
+ | IPGlobalInvariant _ -> "global_invariant"
+ | IPOther _ -> "other"
+
+let names_of_property = function
+ | Property.IPPredicate idp -> idp.ip_pred.ip_content.tp_statement.pred_name
+ | IPCodeAnnot _ -> []
+ | IPAxiomatic _ -> []
+ | IPLemma _ -> []
+ | IPBehavior _ -> []
+ | IPComplete _ -> []
+ | IPDisjoint _ -> []
+ | IPAllocation _ -> []
+ | IPAssigns _ -> []
+ | IPFrom _ -> []
+ | IPDecrease _ -> []
+ | IPExtended _ -> []
+ | IPReachable _ -> []
+ | IPPropertyInstance _ -> []
+ | IPTypeInvariant _ -> []
+ | IPGlobalInvariant _ -> []
+ | IPOther _ -> []
+
+let plugin_of_emitters el =
+ match el with
+ | []
+ | ["Call Preconditions"]
+ | ["Frama-C kernel"] -> "kernel"
+ | ["Eva"] -> "eva"
+ | _ -> "<unknown emitters (" ^ string_of_string_list "," el ^ ")>"
+
+let string_of_syntax_domain = function
+ | Code -> "code"
+ | Declaration -> "decl"
+ | Annotation -> "annot"
+
+let string_of_message_domain = function
+ | Log.Result -> "result"
+ | Feedback -> "feedback"
+ | Debug -> "debug"
+ | Warning -> "warning"
+ | Error -> "error"
+ | Failure -> "failure"
+
+let split_domain = function
+ | Syntax d -> "syntax", string_of_syntax_domain d
+ | Property -> "property", ""
+ | Message d -> "message", string_of_message_domain d
+
+module FunctionAtPos = struct
+ let tbl :
+ (Filepath.Normalized.t,
+ (Filepath.position * Filepath.position * string) Array.t)
+ Hashtbl.t =
+ Hashtbl.create 16
+
+ let binary_search a pos : string option =
+ let cmp = Cil_datatype.Position.compare in
+ let rec aux lo hi =
+ if lo > hi then None
+ else
+ let mid = (hi + lo) / 2 in
+ let (mstart, mend, mfunc) = a.(mid) in
+ if cmp pos mstart >= 0 then
+ if cmp pos mend <= 0 then Some mfunc
+ else aux (mid + 1) hi
+ else aux lo (mid - 1)
+ in
+ aux 0 (Array.length a - 1)
+
+ let compute () =
+ let tmp = Hashtbl.create 16 in
+ let files =
+ List.fold_left (fun acc ((pos1, _, _) as triple) ->
+ let fp = pos1.Filepath.pos_path in
+ Hashtbl.add tmp fp triple;
+ Datatype.Filepath.Set.add fp acc
+ ) Datatype.Filepath.Set.empty (Cabs2cil.func_locs ())
+ in
+ Hashtbl.clear tbl;
+ Datatype.Filepath.Set.iter (fun fp ->
+ let l =
+ List.sort (fun (start1, _, _) (start2, _, _) ->
+ Cil_datatype.Position.compare start1 start2
+ ) (Hashtbl.find_all tmp fp)
+ in
+ Hashtbl.replace tbl fp (Array.of_list l)
+ ) files
+
+ let find pos =
+ let fp = pos.Filepath.pos_path in
+ Option.bind (Hashtbl.find_opt tbl fp)
+ (fun a -> binary_search a pos)
+
+end
+
+type entry = {
+ loc: Cil_datatype.Location.t;
+ func: string option;
+ domain: domain;
+ plugin: string;
+ status: string;
+ node: string;
+ names: string list;
+ text: string;
+}
+
+let headers = ["Directory"; "Filename"; "Extension"; "Line Number";
+ "Function"; "Domain"; "Kind"; "Plugin"; "Status"; "Node";
+ "Names"; "Text"]
+
+let add_entry_str entry =
+ let dir, fname, ext, line = split_loc entry.loc in
+ let funcname = Option.fold ~none:"" ~some:Stdlib.Fun.id entry.func in
+ let domain, kind = split_domain entry.domain in
+ let names = string_of_string_list ":" entry.names in
+ let entry = [dir; fname; ext; line; funcname;
+ domain; kind; entry.plugin; entry.status; entry.node;
+ names; entry.text]
+ in
+ if PivotSourceState.get () = [] then
+ PivotSourceState.add headers;
+ PivotSourceState.add entry
+
+let new_entry ?func ?(plugin="") ?(status="") ?(node="") ?(names=[]) ?(text="") loc domain =
+ { loc; func; domain; plugin; status; node; names; text }
+
+let add_entry ?func ?plugin ?status ?node ?names ?text loc domain =
+ let entry = new_entry ?func ?plugin ?status ?node ?names ?text loc domain in
+ add_entry_str entry
+
+class full_visitor = object(self)
+ inherit Cil.nopCilVisitor
+ val mutable cur_func = None
+ method add ?func ?node ?names domain =
+ let loc = Cil.CurrentLoc.get () in
+ let func = if func <> None && func <> Some "" then func else cur_func in
+ add_entry ?func ?node ?names loc domain
+ method add_code ?func ?names node =
+ self#add ?func ~node ?names (Syntax Code)
+ method add_decl ?func ?names node =
+ self#add ?func ~node ?names (Syntax Declaration)
+ method add_annot ?names node =
+ self#add ~node ?names (Syntax Annotation)
+
+ method! vvrbl (_v:varinfo) = DoChildren
+ method! vvdec (_v:varinfo) = DoChildren
+ method! vexpr (_e:exp) = DoChildren
+ method! vlval (_l:lval) = DoChildren
+ method! voffs (_o:offset) = DoChildren
+ method! vinitoffs (_o:offset) = DoChildren
+
+ method! vinst (i:instr) =
+ let node = node_of_instr i in
+ self#add_code node;
+ DoChildren
+
+ method! vstmt (s:stmt) =
+ begin
+ match opt_node_of_stmtkind s.skind with
+ | None -> ()
+ | Some node -> self#add_code node
+ end;
+ DoChildren
+
+ method! vfunc (f:fundec) =
+ cur_func <- Some f.svar.vname;
+ Cil.DoChildrenPost (fun fd ->
+ cur_func <- None;
+ fd
+ )
+
+ method! vglob (g:global) =
+ let domain, node = domain_and_node_of_global g in
+ let names = names_of_global g in
+ let func = "<global>" in
+ if domain = Declaration then
+ self#add_decl ~func ~names node
+ else
+ self#add_code ~func ~names node;
+ DoChildren
+
+ method! vblock _ = DoChildren
+ method! vinit _ _ _ = DoChildren
+ method! vlocal_init _ _ = DoChildren
+ method! vtype _ = DoChildren
+ method! vcompinfo _ = DoChildren
+ method! venuminfo _ = DoChildren
+ method! vfieldinfo _ = DoChildren
+ method! venumitem _ = DoChildren
+ method! vattr _ = DoChildren
+ method! vattrparam _ = DoChildren
+ method! vmodel_info _ = DoChildren
+ method! vlogic_type _ = DoChildren
+ method! videntified_term _ = DoChildren
+ method! vterm _ = DoChildren
+ method! vterm_node _ = DoChildren
+ method! vterm_lval _ = DoChildren
+ method! vterm_lhost _ = DoChildren
+ method! vterm_offset _ = DoChildren
+ method! vlogic_label _ = DoChildren
+ method! vlogic_info_decl _ = DoChildren
+ method! vlogic_info_use _ = DoChildren
+ method! vlogic_type_info_decl _ = DoChildren
+ method! vlogic_type_info_use _ = DoChildren
+ method! vlogic_type_def _ = DoChildren
+ method! vlogic_ctor_info_decl _ = DoChildren
+ method! vlogic_ctor_info_use _ = DoChildren
+ method! vlogic_var_use _ = DoChildren
+ method! vlogic_var_decl _ = DoChildren
+ method! vquantifiers _ = DoChildren
+ method! videntified_predicate _ =
+ (* should be done by the annotations visitor *)
+ assert false
+ method! vpredicate_node _ = DoChildren
+ method! vpredicate _ = DoChildren
+ method! vbehavior _ = DoChildren
+ method! vassigns _ = DoChildren
+ method! vfrees _ = DoChildren
+ method! vallocates _ = DoChildren
+ method! vallocation _ = DoChildren
+ method! vloop_pragma _ = DoChildren
+ method! vslice_pragma _ = DoChildren
+ method! vimpact_pragma _ = DoChildren
+ method! vdeps _ = DoChildren
+ method! vfrom _ = DoChildren
+ method! vcode_annot _ =
+ (* should be done by the annotations visitor *)
+ assert false
+ method! vannotation ga =
+ let node = node_of_global_annotation ga in
+ let names = Option.to_list (name_of_global_annotation ga) in
+ self#add_annot ~names node;
+ DoChildren
+end
+
+let ca_visitor_cur_func : string option ref = ref None
+let ca_visitor_cur_emitter = ref "<unknown>"
+class code_annot_visitor = object(self)
+ inherit Cil.nopCilVisitor
+
+ method add_annot ?(names=[]) node =
+ let loc = Cil.CurrentLoc.get () in
+ let func = !ca_visitor_cur_func in
+ let plugin = !ca_visitor_cur_emitter in
+ let domain = Syntax Annotation in
+ add_entry ?func ~plugin ~node ~names loc domain
+
+ method! videntified_predicate {ip_content = {tp_kind}} =
+ let node = node_of_predicate_kind tp_kind in
+ self#add_annot node;
+ DoChildren
+
+ method! vcode_annot ca =
+ let content = ca.annot_content in
+ self#add_annot (node_of_code_annotation_node content);
+ DoChildren
+
+ method! vannotation ga =
+ let node = node_of_global_annotation ga in
+ let names = Option.to_list (name_of_global_annotation ga) in
+ self#add_annot ~names node;
+ DoChildren
+end
+
+let visit_annots () =
+ let vis = new code_annot_visitor in
+ Annotations.iter_all_code_annot (
+ fun stmt emitter ca ->
+ let kf = Kernel_function.find_englobing_kf stmt in
+ ca_visitor_cur_func := Some (Kernel_function.get_name kf);
+ ca_visitor_cur_emitter := Emitter.get_name emitter;
+ ignore (Cil.visitCilCodeAnnotation (vis :> Cil.cilVisitor) ca)
+ )
+
+let visit_properties () =
+ Property_status.iter
+ (fun ip ->
+ let loc = Property.location ip in
+ let func = Option.map Kernel_function.get_name (Property.get_kf ip) in
+ let emitters =
+ Property_status.fold_on_statuses (fun emitter _status acc ->
+ Emitter.Usable_emitter.get_name emitter.emitter :: acc
+ ) ip []
+ in
+ let plugin = plugin_of_emitters emitters in
+ let domain = Property in
+ let status =
+ Format.asprintf "%a"
+ Property_status.Feedback.pretty (Property_status.Feedback.get ip)
+ in
+ let node = node_of_property ip in
+ let names = names_of_property ip in
+ add_entry ?func ~node ~status ~plugin ~names loc domain
+ )
+
+let visit_messages () =
+ FunctionAtPos.compute ();
+ Messages.iter (fun ev ->
+ let plugin = ev.evt_plugin in
+ let loc_of_pos p = (p, p) in
+ let loc, func =
+ match ev.evt_source with
+ | None -> Cil_datatype.Location.unknown, "<global>"
+ | Some pos ->
+ let funcname =
+ match FunctionAtPos.find pos with
+ | None -> Metrics_parameters.warning
+ "FUNCTION NOT FOUND FOR NON-GLOBAL MESSAGE POS: %a"
+ Cil_datatype.Position.pretty_debug pos;
+ "<unknown>"
+ | Some name -> name
+ in
+ loc_of_pos pos, funcname
+ in
+ let domain = Message (ev.evt_kind) in
+ let text = ev.evt_message in
+ add_entry ~func ~plugin ~text loc domain
+ )
+
+(* Useful mainly for debugging *)
+let _pp_as_csv (data : string list list) =
+ let pp_list = string_of_string_list "," in
+ List.iter (fun ls -> Format.printf "%s@\n" (pp_list ls)) (List.rev data)
+
+(* Server / Ivette stuff *)
+
+open Server
+
+let package =
+ Package.package
+ ~plugin:"pivot"
+ ~name:"general"
+ ~title:"Pivot Table Services"
+ ~readme:"pivot.md"
+ ()
+
+module TableState = struct
+ type t = string list list
+ let jtype =
+ Data.declare ~package
+ ~name:"tableStateType"
+ ~descr:(Markdown.plain "State of the pivot table source data.")
+ Package.(Jarray (Jarray Jstring))
+ let to_json ll =
+ `List (List.rev_map (fun l -> `List (List.map (fun s -> `String s) l)) ll)
+end
+
+let pivot_signal =
+ States.register_value ~package
+ ~name:"pivotState"
+ ~descr:(Markdown.plain "State of the pivot table source data.")
+ ~output:(module TableState)
+ ~get:PivotSourceState.get
+ ~add_hook:PivotSourceState.add_hook_on_update
+ ()
+
+let compute () =
+ let ast = Ast.get () in
+ let vis = new full_visitor in
+ ignore (Cil.visitCilFile (vis :> Cil.cilVisitor) ast);
+ visit_annots ();
+ visit_properties ();
+ visit_messages ();
+ (*_pp_as_csv (PivotSourceState.get ());*)
+ (* Signals that the pivot table has been updated. *)
+ Server.Request.emit pivot_signal
+
+let _compute =
+ Server.Request.register ~package
+ ~kind:`EXEC ~name:"compute"
+ ~descr:(Markdown.plain "Computes the pivot table.")
+ ~input:(module Data.Junit) ~output:(module Data.Junit) compute
diff --git a/src/plugins/metrics/metrics_pivot.mli b/src/plugins/metrics/metrics_pivot.mli
new file mode 100644
index 0000000000000000000000000000000000000000..98ffe7ef308729877bd4ce7bf50dd0584b275cde
--- /dev/null
+++ b/src/plugins/metrics/metrics_pivot.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Nothing is exported. *)
diff --git a/tests/syntax/func_locs.i b/tests/syntax/func_locs.i
new file mode 100644
index 0000000000000000000000000000000000000000..9bde496168fe2aa66a3b12a9963fbfa61147fbb0
--- /dev/null
+++ b/tests/syntax/func_locs.i
@@ -0,0 +1,36 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-no-print"
+*/
+
+
+//@ assigns \nothing;
+void with_spec() {
+}
+
+int gx;
+
+/*@
+ requires req: a >= 0 || gx == 0;
+ assigns \result \from a;
+ ensures ens: \result == a;
+ */
+int id(int a);
+
+/*@
+ requires req: a >= 0;
+*/
+int id(int a);
+
+int decl_no_spec(); int id(int a);
+
+int def_no_spec() {
+ return 2;
+}
+
+/*@
+ requires \true;
+*/
+int main() {
+ return 0;
+}
diff --git a/tests/syntax/func_locs.ml b/tests/syntax/func_locs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e28f0429b68ca220b12e37f15c4417edc32179c6
--- /dev/null
+++ b/tests/syntax/func_locs.ml
@@ -0,0 +1,9 @@
+let run () =
+ List.iter (fun (pos1, pos2, fname) ->
+ Format.printf "%a - %a -> %s@."
+ Cil_datatype.Position.pp_with_col pos1
+ Cil_datatype.Position.pp_with_col pos2
+ fname
+ ) (Cabs2cil.func_locs ())
+
+let () = Db.Main.extend run
diff --git a/tests/syntax/oracle/func_locs.res.oracle b/tests/syntax/oracle/func_locs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8fd4ca099e2fa45737df2beec4c827b0473d0f65
--- /dev/null
+++ b/tests/syntax/oracle/func_locs.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing func_locs.i (no preprocessing)
+[kernel] func_locs.i:20: Warning:
+ found two contracts (old location: func_locs.i:13). Merging them
+func_locs.i:31 char 3 - func_locs.i:36 char 1 -> main
+func_locs.i:27 char 4 - func_locs.i:29 char 1 -> def_no_spec
+func_locs.i:25 char 20 - func_locs.i:25 char 26 -> id
+func_locs.i:25 char 0 - func_locs.i:25 char 16 -> decl_no_spec
+func_locs.i:20 char 3 - func_locs.i:23 char 6 -> id
+func_locs.i:13 char 3 - func_locs.i:18 char 6 -> id
+func_locs.i:7 char 3 - func_locs.i:9 char 1 -> with_spec