diff --git a/Makefile b/Makefile
index e9664546176d1f99637970d4274ede5bfbcf060d..7dd57fbf16620ad4344ab825ae8e30793e42e470 100644
--- a/Makefile
+++ b/Makefile
@@ -829,7 +829,7 @@ PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
- values/numerors domains/numerors
+ api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
@@ -912,6 +912,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
engine/compute_functions engine/analysis register \
api/general_requests \
utils/unit_tests \
+ api/values_request \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 5d791ad40ee2ce6301155c602be4b5fb34761a11..a412c54e05be8e26a83069fbe6381e14e0c6e32d 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1210,6 +1210,8 @@ src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/api/values_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index 623884b14adfa9242c3387102ec72042534bad37..0b6931ec606e425b8f53499034958425e9f588a8 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -43,10 +43,6 @@ export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Marker kind */
export enum markerKind {
- /** Variable */
- variable = 'variable',
- /** Function */
- function = 'function',
/** Expression */
expression = 'expression',
/** Lvalue */
@@ -83,12 +79,44 @@ const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
+/** Marker variable */
+export enum markerVar {
+ /** None */
+ none = 'none',
+ /** Variable */
+ variable = 'variable',
+ /** Function */
+ function = 'function',
+}
+
+/** Loose decoder for `markerVar` */
+export const jMarkerVar: Json.Loose<markerVar> = Json.jEnum(markerVar);
+
+/** Safe decoder for `markerVar` */
+export const jMarkerVarSafe: Json.Safe<markerVar> =
+ Json.jFail(Json.jEnum(markerVar),'kernel.ast.markerVar expected');
+
+/** Natural order for `markerVar` */
+export const byMarkerVar: Compare.Order<markerVar> =
+ Compare.byEnum(markerVar);
+
+const markerVarTags_internal: Server.GetRequest<null,tag[]> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.markerVarTags',
+ input: Json.jNull,
+ output: Json.jList(jTag),
+};
+/** Registered tags for the above type. */
+export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_internal;
+
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
+ /** Marker variable */
+ var: markerVar;
/** Marker short name */
name: string;
/** Marker declaration or description */
@@ -101,6 +129,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> =
key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
'#markerInfo expected'),
kind: jMarkerKindSafe,
+ var: jMarkerVarSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
});
@@ -112,10 +141,11 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
/** Natural order for `markerInfoData` */
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
- <{ key: Json.key<'#markerInfo'>, kind: markerKind, name: string,
- descr: string }>({
+ <{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
+ name: string, descr: string }>({
key: Compare.string,
kind: byMarkerKind,
+ var: byMarkerVar,
name: Compare.alpha,
descr: Compare.string,
});
diff --git a/ivette/api/plugins/eva/index.ts b/ivette/api/plugins/eva/general/index.ts
similarity index 92%
rename from ivette/api/plugins/eva/index.ts
rename to ivette/api/plugins/eva/general/index.ts
index 4b46b34354923641cd17852220a4a7ff037b790f..9f77331803e084829e2e0d6ac13847d0f4d7f625 100644
--- a/ivette/api/plugins/eva/index.ts
+++ b/ivette/api/plugins/eva/general/index.ts
@@ -3,7 +3,7 @@
/**
Eva General Services
@packageDocumentation
- @module api/plugins/eva
+ @module api/plugins/eva/general
*/
//@ts-ignore
@@ -21,7 +21,7 @@ const getCallers_internal: Server.GetRequest<
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
> = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.getCallers',
+ name: 'plugins.eva.general.getCallers',
input: Json.jKey<'#fct'>('#fct'),
output: Json.jList(Json.jTry(
Json.jPair(
diff --git a/ivette/api/plugins/eva/values/index.ts b/ivette/api/plugins/eva/values/index.ts
new file mode 100644
index 0000000000000000000000000000000000000000..22375d253f9b2f0bac5f1242c8cfe80693973c0e
--- /dev/null
+++ b/ivette/api/plugins/eva/values/index.ts
@@ -0,0 +1,154 @@
+/* --- Generated Frama-C Server API --- */
+
+/**
+ Eva Values
+ @packageDocumentation
+ @module api/plugins/eva/values
+*/
+
+//@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';
+
+//@ts-ignore
+import { byMarker } from 'api/kernel/ast';
+//@ts-ignore
+import { jMarker } from 'api/kernel/ast';
+//@ts-ignore
+import { jMarkerSafe } from 'api/kernel/ast';
+//@ts-ignore
+import { marker } from 'api/kernel/ast';
+
+/** CallStack */
+export interface callstack {
+ /** Callstack id */
+ id: number;
+ /** Short name for the callstack */
+ short: string;
+ /** Full name for the callstack */
+ full: string;
+}
+
+/** Loose decoder for `callstack` */
+export const jCallstack: Json.Loose<callstack> =
+ Json.jObject({
+ id: Json.jFail(Json.jNumber,'Number expected'),
+ short: Json.jFail(Json.jString,'String expected'),
+ full: Json.jFail(Json.jString,'String expected'),
+ });
+
+/** Safe decoder for `callstack` */
+export const jCallstackSafe: Json.Safe<callstack> =
+ Json.jFail(jCallstack,'Callstack expected');
+
+/** Natural order for `callstack` */
+export const byCallstack: Compare.Order<callstack> =
+ Compare.byFields
+ <{ id: number, short: string, full: string }>({
+ id: Compare.number,
+ short: Compare.string,
+ full: Compare.string,
+ });
+
+/** Data for array rows [`values`](#values) */
+export interface valuesData {
+ /** Entry identifier. */
+ key: Json.key<'#values'>;
+ /** CallStack */
+ callstack: callstack;
+ /** Value inferred just before the selected point */
+ value_before: string;
+ /** Did the evaluation led to an alarm? */
+ alarm: boolean;
+ /** Value inferred just after the selected point */
+ value_after?: string;
+}
+
+/** Loose decoder for `valuesData` */
+export const jValuesData: Json.Loose<valuesData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey<'#values'>('#values'),'#values expected'),
+ callstack: jCallstackSafe,
+ value_before: Json.jFail(Json.jString,'String expected'),
+ alarm: Json.jFail(Json.jBoolean,'Boolean expected'),
+ value_after: Json.jString,
+ });
+
+/** Safe decoder for `valuesData` */
+export const jValuesDataSafe: Json.Safe<valuesData> =
+ Json.jFail(jValuesData,'ValuesData expected');
+
+/** Natural order for `valuesData` */
+export const byValuesData: Compare.Order<valuesData> =
+ Compare.byFields
+ <{ key: Json.key<'#values'>, callstack: callstack, value_before: string,
+ alarm: boolean, value_after?: string }>({
+ key: Compare.string,
+ callstack: byCallstack,
+ value_before: Compare.string,
+ alarm: Compare.boolean,
+ value_after: Compare.defined(Compare.string),
+ });
+
+/** Signal for array [`values`](#values) */
+export const signalValues: Server.Signal = {
+ name: 'plugins.eva.values.signalValues',
+};
+
+const reloadValues_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.values.reloadValues',
+ input: Json.jNull,
+ output: Json.jNull,
+};
+/** Force full reload for array [`values`](#values) */
+export const reloadValues: Server.GetRequest<null,null>= reloadValues_internal;
+
+const fetchValues_internal: Server.GetRequest<
+ number,
+ { pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
+ reload: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.values.fetchValues',
+ input: Json.jNumber,
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jValuesData),
+ removed: Json.jList(Json.jKey<'#values'>('#values')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
+};
+/** Data fetcher for array [`values`](#values) */
+export const fetchValues: Server.GetRequest<
+ number,
+ { pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
+ reload: boolean }
+ >= fetchValues_internal;
+
+const values_internal: State.Array<Json.key<'#values'>,valuesData> = {
+ name: 'plugins.eva.values.values',
+ getkey: ((d:valuesData) => d.key),
+ signal: signalValues,
+ fetch: fetchValues,
+ reload: reloadValues,
+ order: byValuesData,
+};
+/** Abstract values inferred by the Eva analysis */
+export const values: State.Array<Json.key<'#values'>,valuesData> = values_internal;
+
+const getValues_internal: Server.GetRequest<marker,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.values.getValues',
+ input: jMarker,
+ output: Json.jNull,
+};
+/** Get the abstract values computed for an expression or lvalue */
+export const getValues: Server.GetRequest<marker,null>= getValues_internal;
+
+/* ------------------------------------- */
diff --git a/ivette/package.json b/ivette/package.json
index c86d31fa83b3763daf8f92c58127c066a9dce062..d496a65fb2830caeadbaab293a543e2abf2a1302 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -33,7 +33,7 @@
"css-loader": "^3.4.0",
"electron": "^7",
"electron-builder": "^22.4.1",
- "electron-devtools-installer": "^2.2.4",
+ "electron-devtools-installer": "^3.0.0",
"electron-webpack": "^2.8.2",
"eslint": "^6.8.0",
"eslint-config-airbnb": "^18.1.0",
diff --git a/ivette/src/dome/src/main/dome.js b/ivette/src/dome/src/main/dome.js
index cd01363afb0b82961da1f77f1baed2b3865e5b7c..e6291c5e4f94505092119aea4872d1cd07500c02 100644
--- a/ivette/src/dome/src/main/dome.js
+++ b/ivette/src/dome/src/main/dome.js
@@ -392,7 +392,10 @@ function createPrimaryWindow()
// React Developper Tools
if (DEVEL)
- installExtension(REACT_DEVELOPER_TOOLS,true);
+ installExtension(REACT_DEVELOPER_TOOLS,true)
+ .catch((err) => {
+ console.error('[Dome] Enable to install React dev-tools',err);
+ });
const cwd = process.cwd();
const wdir = cwd === '/' ? app.getPath('home') : cwd ;
const argv = stripElectronArgv(process.argv);
diff --git a/ivette/src/dome/src/misc/devtools.js b/ivette/src/dome/src/misc/devtools.js
index 222b66d9d3d159ba7703dbf7d822519abc0b5ab8..4c921aa6c9ed956aaa131813074cb4303c6af844 100644
--- a/ivette/src/dome/src/misc/devtools.js
+++ b/ivette/src/dome/src/misc/devtools.js
@@ -8,5 +8,5 @@ export const REACT_DEVELOPER_TOOLS = undefined ;
// Shall not be used in non-development mode
export default function installExtension(_id) {
- return Promise.reject();
+ return Promise.resolve();
}
diff --git a/ivette/src/dome/src/renderer/table/arrays.ts b/ivette/src/dome/src/renderer/table/arrays.ts
index 705ec7fd0d214947bfa69aca49718097b11a21a6..e506d8237fc7e5ff1fdd635a9b0b630e761c5161 100644
--- a/ivette/src/dome/src/renderer/table/arrays.ts
+++ b/ivette/src/dome/src/renderer/table/arrays.ts
@@ -429,7 +429,7 @@ export class ArrayModel<Key, Row>
// --------------------------------------------------------------------------
/**
- @template Row - object data that also contains their « key »
+ @template Row - object data that also contains their « key ».
*/
export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
@@ -460,7 +460,6 @@ export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
this.reload();
}
-
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/src/renderer/table/views.tsx b/ivette/src/dome/src/renderer/table/views.tsx
index 5e7888b7c89035af4b1b8de6cfa738f47a075fdd..3089b35483683f8efa470dc7e241091877333937 100644
--- a/ivette/src/dome/src/renderer/table/views.tsx
+++ b/ivette/src/dome/src/renderer/table/views.tsx
@@ -59,6 +59,14 @@ export type RenderByFields<Row> = {
export type index = number | number[]
/**
+ Column Properties.
+
+ __Warning:__ callback properties, namely `getter`, `render`
+ and `onContextMenu`, shall be as stable as possible to prevent
+ the table from constantly re-rendering.
+ Use constant callbacks whenever possible, or memoize them with
+ `React.useCallback()` hook.
+
@template Row - table row data of some table entries
@template Cell - type of cell data to render in this column
*/
@@ -104,14 +112,17 @@ export interface ColumnProps<Row, Cell> {
visible?: boolean | 'never' | 'always';
/**
Data getter for this column.
+ Shall be constant or protected by `React.useCallback`.
*/
getter?: (row: Row, dataKey: string) => Cell | undefined;
/**
Override table by-fields cell renderers.
+ Shall be constant or protected by `React.useCallback`.
*/
render?: Renderer<Cell>;
/**
Override table right-click callback.
+ Shall be constant or protected by `React.useCallback`.
*/
onContextMenu?: (row: Row, index: number, dataKey: string) => void;
}
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index f97145728dc4ddb26db0f447df3a9c93aecd843a..ebfcbe4595ad602b0786f1b65ec8395388e81edb 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -15,7 +15,7 @@ import { IconButton } from 'dome/controls/buttons';
import { Component, TitleBar } from 'frama-c/LabViews';
import { printFunction, markerInfo } from 'api/kernel/ast';
-import { getCallers } from 'api/plugins/eva';
+import { getCallers } from 'api/plugins/eva/general';
import 'codemirror/mode/clike/clike';
import 'codemirror/theme/ambiance.css';
@@ -123,7 +123,7 @@ const ASTview = () => {
const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2);
const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
- function onTextSelection(id: key<'#markerIndo'>) {
+ function onTextSelection(id: key<'#markerInfo'>) {
if (selection.current) {
const location = { ...selection.current, marker: id };
updateSelection({ location });
@@ -133,18 +133,8 @@ const ASTview = () => {
async function onContextMenu(id: key<'#markerInfo'>) {
const items = [];
const selectedMarkerInfo = markersInfo.find((e) => e.key === id);
- switch (selectedMarkerInfo?.kind) {
- case 'function': {
- items.push({
- label: `Go to definition of ${selectedMarkerInfo.name}`,
- onClick: () => {
- const location = { function: selectedMarkerInfo.name };
- updateSelection({ location });
- },
- });
- break;
- }
- case 'declaration': {
+ if (selectedMarkerInfo?.var === 'function') {
+ if (selectedMarkerInfo.kind === 'declaration') {
if (selectedMarkerInfo?.name) {
const locations = await functionCallers(selectedMarkerInfo.name);
const locationsByFunction = _.groupBy(locations, (e) => e.function);
@@ -162,10 +152,15 @@ const ASTview = () => {
});
});
}
- break;
+ } else {
+ items.push({
+ label: `Go to definition of ${selectedMarkerInfo.name}`,
+ onClick: () => {
+ const location = { function: selectedMarkerInfo.name };
+ updateSelection({ location });
+ },
+ });
}
- default:
- break;
}
if (items.length > 0)
Dome.popupMenu(items);
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index a2d04f1270e603b9f71a4ed6d906a6e32560d109..6b16620df021ded5fade5192c5c733823344f255 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -21,6 +21,7 @@ import ASTinfo from './ASTinfo';
import Globals from './Globals';
import Properties from './Properties';
import Locations from './Locations';
+import Values from './Values';
// --------------------------------------------------------------------------
// --- Selection Controls
@@ -101,6 +102,7 @@ export default (() => {
<ASTview />
<ASTinfo />
<Locations />
+ <Values />
</Group>
</LabView>
</Splitter>
diff --git a/ivette/src/renderer/Values.tsx b/ivette/src/renderer/Values.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..652f48fc1072c0a0ea7186293fdcaec0504e00c5
--- /dev/null
+++ b/ivette/src/renderer/Values.tsx
@@ -0,0 +1,141 @@
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import * as States from 'frama-c/states';
+import * as Json from 'dome/data/json';
+import * as Eva from 'api/plugins/eva/values';
+import * as Ast from 'api/kernel/ast';
+import * as Compare from 'dome/data/compare';
+
+import { Table, Column } from 'dome/table/views';
+import { ArrayModel } from 'dome/table/arrays';
+import { Component } from 'frama-c/LabViews';
+import { Icon } from 'dome/controls/icons';
+import { Label } from 'dome/controls/labels';
+
+// --------------------------------------------------------------------------
+// --- Columns
+// --------------------------------------------------------------------------
+
+const CallstackRenderer = (
+ (cs: Eva.callstack) => <Label label={cs.short} title={cs.full} />
+);
+
+const ColumnCallstack = () => Column({
+ id: 'callstack',
+ label: 'Callstack',
+ title: 'Context of the evaluation',
+ align: 'left',
+ width: 150,
+ render: CallstackRenderer,
+});
+
+const AlarmRenderer = (
+ (alarm: boolean) => <>{alarm && <Icon id="ATTENTION" />}</>
+);
+
+const ColumnAlarm = (props: { visible: boolean }) => Column({
+ id: 'alarm',
+ label: 'Alarm',
+ title: 'Did the evaluation emit an alarm?',
+ align: 'center',
+ width: 26,
+ fixed: true,
+ icon: 'WARNING',
+ visible: props.visible,
+ render: AlarmRenderer,
+});
+
+const byValues: Compare.ByFields<Eva.valuesData> =
+ { callstack: Compare.defined(Compare.byFields({ full: Compare.string })) };
+
+class ValuesModel extends ArrayModel<Json.key<'#values'>, Eva.valuesData> {
+ constructor() {
+ super();
+ this.setOrderingByFields(byValues);
+ }
+}
+
+// --------------------------------------------------------------------------
+// --- Values Panel
+// --------------------------------------------------------------------------
+
+const Values = () => {
+
+ const model = React.useMemo(() => new ValuesModel(), []);
+ const evaValues = States.useSyncArray(Eva.values).getArray();
+ const selectMarker = States.useSelection()[0]?.current?.marker;
+ const markerInfo = States.useSyncArray(Ast.markerInfo).getArray();
+ const [name, setName] = React.useState<string | undefined>(undefined);
+
+ States.useRequest(Eva.getValues, selectMarker);
+
+ React.useEffect(() => {
+ model.removeAllData();
+ if (selectMarker && evaValues) {
+ const selectMarkerInfo = markerInfo.find((e) => e.key === selectMarker);
+ if (selectMarkerInfo && selectMarkerInfo.var !== 'function') {
+ switch (selectMarkerInfo.kind) {
+ case 'expression':
+ case 'lvalue':
+ evaValues.forEach((i) => model.setData(i.key, i));
+ setName(selectMarkerInfo.descr);
+ break;
+ case 'declaration':
+ evaValues.forEach((i) => model.setData(i.key, i));
+ setName(selectMarkerInfo.name);
+ break;
+ default:
+ setName(undefined);
+ }
+ }
+ } else {
+ setName(undefined);
+ }
+ model.reload();
+ }, [evaValues, selectMarker, markerInfo, model]);
+
+ // Component
+ return (
+ <>
+ <Table model={model}>
+ <ColumnCallstack />
+ <Column
+ id="value_before"
+ visible={!!name}
+ label={name && `${name} (before)`}
+ title="Values inferred by Eva just before the selected point"
+ disableSort
+ width={300}
+ />
+ <ColumnAlarm visible={!!name} />
+ <Column
+ id="value_after"
+ visible={!!name}
+ label={name && `${name} (after)`}
+ title="Values inferred by Eva just after the selected point"
+ disableSort
+ width={300}
+ />
+ </Table>
+ </>
+ );
+};
+
+// --------------------------------------------------------------------------
+// --- Export Component
+// --------------------------------------------------------------------------
+
+export default () => (
+ <Component
+ id="frama-c.values"
+ label="Eva Values"
+ title="Values inferred by the Eva analysis"
+ >
+ <Values />
+ </Component>
+);
+
+// --------------------------------------------------------------------------
diff --git a/ivette/tests/eva-2.i b/ivette/tests/eva-2.i
new file mode 100644
index 0000000000000000000000000000000000000000..8b0998c24954c340558942ef8f4bf7e1c66205da
--- /dev/null
+++ b/ivette/tests/eva-2.i
@@ -0,0 +1,20 @@
+volatile int nondet;
+
+void fun () {
+ int x = nondet;
+ x = -x;
+}
+
+void yet_another () {
+ int x = nondet;
+ fun ();
+ int y = 100 / x;
+}
+
+void main () {
+ fun ();
+ /*@ assert boh: 1 == 1; */
+ yet_another ();
+ int i = 0;
+ /*@ assert user: i == 0; */
+}
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index 326cb44b75057094cf39c1457749096978a8f9f6..014efd5cfda84900de0d0ebb570171ce8c6ac593 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -3337,6 +3337,15 @@ electron-devtools-installer@^2.2.4:
rimraf "^2.5.2"
semver "^5.3.0"
+electron-devtools-installer@^3.0.0:
+ version "3.1.1"
+ resolved "https://registry.yarnpkg.com/electron-devtools-installer/-/electron-devtools-installer-3.1.1.tgz#7b56c8c86475c5e4e10de6917d150c53c9ceb55e"
+ integrity sha512-g2D4J6APbpsiIcnLkFMyKZ6bOpEJ0Ltcc2m66F7oKUymyGAt628OWeU9nRZoh1cNmUs/a6Cls2UfOmsZtE496Q==
+ dependencies:
+ rimraf "^3.0.2"
+ semver "^7.2.1"
+ unzip-crx-3 "^0.2.0"
+
electron-publish@22.4.1:
version "22.4.1"
resolved "https://registry.yarnpkg.com/electron-publish/-/electron-publish-22.4.1.tgz#a7fcf166786f7d5957f19a70ee8389f219769ba5"
@@ -4813,6 +4822,11 @@ ignore@^4.0.6:
resolved "https://registry.yarnpkg.com/ignore/-/ignore-4.0.6.tgz#750e3db5862087b4737ebac8207ffd1ef27b25fc"
integrity sha512-cyFDKrqc/YdcWFniJhzI42+AzS+gNwmUzOSFcRCQYwySuBBBy/KjuxWLZ/FHEH6Moq1NizMOBWyTcv8O4OZIMg==
+immediate@~3.0.5:
+ version "3.0.6"
+ resolved "https://registry.yarnpkg.com/immediate/-/immediate-3.0.6.tgz#9db1dbd0faf8de6fbe0f5dd5e56bb606280de69b"
+ integrity sha1-nbHb0Pr43m++D13V5Wu2BigN5ps=
+
immutable@^4.0.0-rc.12:
version "4.0.0-rc.12"
resolved "https://registry.yarnpkg.com/immutable/-/immutable-4.0.0-rc.12.tgz#ca59a7e4c19ae8d9bf74a97bdf0f6e2f2a5d0217"
@@ -5393,6 +5407,16 @@ jsx-ast-utils@^2.4.1:
array-includes "^3.1.1"
object.assign "^4.1.0"
+jszip@^3.1.0:
+ version "3.5.0"
+ resolved "https://registry.yarnpkg.com/jszip/-/jszip-3.5.0.tgz#b4fd1f368245346658e781fec9675802489e15f6"
+ integrity sha512-WRtu7TPCmYePR1nazfrtuF216cIVon/3GWOvHS9QR5bIwSbnxtdpma6un3jyGGNhHsKCSzn5Ypk+EkDRvTGiFA==
+ dependencies:
+ lie "~3.3.0"
+ pako "~1.0.2"
+ readable-stream "~2.3.6"
+ set-immediate-shim "~1.0.1"
+
keyv@^3.0.0:
version "3.1.0"
resolved "https://registry.yarnpkg.com/keyv/-/keyv-3.1.0.tgz#ecc228486f69991e49e9476485a5be1e8fc5c4d9"
@@ -5487,6 +5511,13 @@ levn@^0.3.0, levn@~0.3.0:
prelude-ls "~1.1.2"
type-check "~0.3.2"
+lie@~3.3.0:
+ version "3.3.0"
+ resolved "https://registry.yarnpkg.com/lie/-/lie-3.3.0.tgz#dcf82dee545f46074daf200c7c1c5a08e0f40f6a"
+ integrity sha512-UaiMJzeWRlEujzAuw5LokY1L5ecNQYZKfmyZ9L7wDHb/p5etKaxXhohBcrw0EYby+G/NA52vRSN4N39dxHAIwQ==
+ dependencies:
+ immediate "~3.0.5"
+
linkify-it@^2.0.0:
version "2.2.0"
resolved "https://registry.yarnpkg.com/linkify-it/-/linkify-it-2.2.0.tgz#e3b54697e78bf915c70a38acd78fd09e0058b1cf"
@@ -6411,7 +6442,7 @@ package-json@^6.3.0:
registry-url "^5.0.0"
semver "^6.2.0"
-pako@~1.0.5:
+pako@~1.0.2, pako@~1.0.5:
version "1.0.11"
resolved "https://registry.yarnpkg.com/pako/-/pako-1.0.11.tgz#6c9599d340d54dfd3946380252a35705a6b992bf"
integrity sha512-4hLB8Py4zZce5s4yd9XzopqwVv/yGNhV1Bl8NTmCq1763HeK2+EwVTv+leGeL13Dnh2wfbqowVPXCIO0z4taYw==
@@ -7576,6 +7607,13 @@ rimraf@^2.5.2, rimraf@^2.5.4, rimraf@^2.6.3, rimraf@^2.7.1:
dependencies:
glob "^7.1.3"
+rimraf@^3.0.2:
+ version "3.0.2"
+ resolved "https://registry.yarnpkg.com/rimraf/-/rimraf-3.0.2.tgz#f1a5402ba6220ad52cc1282bac1ae3aa49fd061a"
+ integrity sha512-JZkJMZkAGFFPP2YqXZXPbMlMBgsxzE8ILs4lMIX/2o0L9UBw9O/Y3o6wFw/i9YLapcUJWwqbi3kdxIPdC62TIA==
+ dependencies:
+ glob "^7.1.3"
+
ripemd160@^2.0.0, ripemd160@^2.0.1:
version "2.0.2"
resolved "https://registry.yarnpkg.com/ripemd160/-/ripemd160-2.0.2.tgz#a1c1a6f624751577ba5d07914cbc92850585890c"
@@ -7723,7 +7761,7 @@ semver@^6.0.0, semver@^6.1.2, semver@^6.2.0, semver@^6.3.0:
resolved "https://registry.yarnpkg.com/semver/-/semver-6.3.0.tgz#ee0a64c8af5e8ceea67687b133761e1becbd1d3d"
integrity sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==
-semver@^7.1.1:
+semver@^7.1.1, semver@^7.2.1:
version "7.3.2"
resolved "https://registry.yarnpkg.com/semver/-/semver-7.3.2.tgz#604962b052b81ed0786aae84389ffba70ffd3938"
integrity sha512-OrOb32TeeambH6UrhtShmF7CRDqhL6/5XpPNp2DuRH6+9QLw/orhp72j87v8Qa1ScDkvrrBNpZcDejAirJmfXQ==
@@ -7821,6 +7859,11 @@ set-blocking@^2.0.0:
resolved "https://registry.yarnpkg.com/set-blocking/-/set-blocking-2.0.0.tgz#045f9782d011ae9a6803ddd382b24392b3d890f7"
integrity sha1-BF+XgtARrppoA93TgrJDkrPYkPc=
+set-immediate-shim@~1.0.1:
+ version "1.0.1"
+ resolved "https://registry.yarnpkg.com/set-immediate-shim/-/set-immediate-shim-1.0.1.tgz#4b2b1b27eb808a9f8dcc481a58e5e56f599f3f61"
+ integrity sha1-SysbJ+uAip+NzEgaWOXlb1mfP2E=
+
set-value@^2.0.0, set-value@^2.0.1:
version "2.0.1"
resolved "https://registry.yarnpkg.com/set-value/-/set-value-2.0.1.tgz#a18d40530e6f07de4228c7defe4227af8cad005b"
@@ -8761,6 +8804,15 @@ unset-value@^1.0.0:
has-value "^0.3.1"
isobject "^3.0.0"
+unzip-crx-3@^0.2.0:
+ version "0.2.0"
+ resolved "https://registry.yarnpkg.com/unzip-crx-3/-/unzip-crx-3-0.2.0.tgz#d5324147b104a8aed9ae8639c95521f6f7cda292"
+ integrity sha512-0+JiUq/z7faJ6oifVB5nSwt589v1KCduqIJupNVDoWSXZtWDmjDGO3RAEOvwJ07w90aoXoP4enKsR7ecMrJtWQ==
+ dependencies:
+ jszip "^3.1.0"
+ mkdirp "^0.5.1"
+ yaku "^0.16.6"
+
upath@^1.1.1:
version "1.2.0"
resolved "https://registry.yarnpkg.com/upath/-/upath-1.2.0.tgz#8f66dbcd55a883acdae4408af8b035a5044c1894"
@@ -9209,6 +9261,11 @@ xtend@^4.0.0, xtend@~4.0.1:
resolved "https://registry.yarnpkg.com/y18n/-/y18n-4.0.0.tgz#95ef94f85ecc81d007c264e190a120f0a3c8566b"
integrity sha512-r9S/ZyXu/Xu9q1tYlpsLIsa3EeLXXk0VwlxqTcFRfg9EhMW+17kbt9G0NrgCmhGb5vT2hyhJZLfDGx+7+5Uj/w==
+yaku@^0.16.6:
+ version "0.16.7"
+ resolved "https://registry.yarnpkg.com/yaku/-/yaku-0.16.7.tgz#1d195c78aa9b5bf8479c895b9504fd4f0847984e"
+ integrity sha1-HRlceKqbW/hHnIlblQT9TwhHmE4=
+
yallist@^2.1.2:
version "2.1.2"
resolved "https://registry.yarnpkg.com/yallist/-/yallist-2.1.2.tgz#1c11f9218f076089a47dd512f93c6699a6a81d52"
diff --git a/src/libraries/utils/utf8_logic.ml b/src/libraries/utils/utf8_logic.ml
index 1c2f3a6ddf068d4d24cec065a1d52cbad7f28301..92f594e89998bdcfad518673c529275de25a26e6 100644
--- a/src/libraries/utils/utf8_logic.ml
+++ b/src/libraries/utils/utf8_logic.ml
@@ -78,6 +78,9 @@ let integer = from_unichar 0x2124
let real = from_unichar 0x211D
let pi = from_unichar 0x3C0
+
+let infinity = from_unichar 0x221E
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/libraries/utils/utf8_logic.mli b/src/libraries/utils/utf8_logic.mli
index 449e20476bd3f55a53b09dd0cf143395d1ce5fad..7b6ea13a0da7362607108c23d890ca96d5f34184 100644
--- a/src/libraries/utils/utf8_logic.mli
+++ b/src/libraries/utils/utf8_logic.mli
@@ -49,6 +49,7 @@ val boolean: string
val integer: string
val real: string
val pi: string
+val infinity: string
(*
Local Variables:
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 7c18b2b5e3c00b3b5d0847da68dc9c91e6caedac..c9e03ae607829bb4f3833ff2a5a1bf98bbe49414 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -46,11 +46,12 @@ module MarkerKind = struct
let kinds = Enum.dictionary ()
- let kind name = Enum.tag ~name
- ~descr:(Md.plain (String.capitalize_ascii name)) kinds
+ let kind name =
+ Enum.tag
+ ~name
+ ~descr:(Md.plain (String.capitalize_ascii name))
+ kinds
- let var = kind "variable"
- let fct = kind "function"
let expr = kind "expression"
let lval = kind "lvalue"
let decl = kind "declaration"
@@ -59,24 +60,65 @@ module MarkerKind = struct
let term = kind "term"
let prop = kind "property"
- let () = Enum.set_lookup kinds
- begin
- let open Printer_tag in
- function
- | PStmt _ -> stmt
- | PStmtStart _ -> stmt
- | PVDecl _ -> decl
- | PLval (_, _, (Var vi, NoOffset)) ->
- if Cil.isFunctionType vi.vtype then fct else var
- | PLval _ -> lval
- | PExp _ -> expr
- | PTermLval _ -> term
- | PGlobal _ -> glob
- | PIP _ -> prop
- end
-
- let data = Request.dictionary ~package
- ~name:"markerKind" ~descr:(Md.plain "Marker kind") kinds
+ let () =
+ Enum.set_lookup
+ kinds
+ (fun localizable ->
+ let open Printer_tag in
+ match localizable with
+ | PStmt _ -> stmt
+ | PStmtStart _ -> stmt
+ | PVDecl _ -> decl
+ | PLval _ -> lval
+ | PExp _ -> expr
+ | PTermLval _ -> term
+ | PGlobal _ -> glob
+ | PIP _ -> prop)
+
+ let data =
+ Request.dictionary
+ ~package
+ ~name:"markerKind"
+ ~descr:(Md.plain "Marker kind")
+ kinds
+
+ include (val data : S with type t = Printer_tag.localizable)
+end
+
+module MarkerVar = struct
+
+ let vars = Enum.dictionary ()
+
+ let kind name =
+ Enum.tag
+ ~name
+ ~descr:(Md.plain (String.capitalize_ascii name))
+ vars
+
+ let none = kind "none"
+ let var = kind "variable"
+ let fct = kind "function"
+
+ let () =
+ Enum.set_lookup
+ vars
+ (fun localizable ->
+ let open Printer_tag in
+ match localizable with
+ | PLval (_, _, (Var vi, NoOffset))
+ | PVDecl (_, _, vi)
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) ->
+ if Cil.isFunctionType vi.vtype then fct else var
+ | PGlobal (GFun _ | GFunDecl _) -> fct
+ | PLval _ | PStmt _ | PStmtStart _
+ | PExp _ | PTermLval _ | PGlobal _ | PIP _ -> none)
+
+ let data =
+ Request.dictionary
+ ~package
+ ~name:"markerVar"
+ ~descr:(Md.plain "Marker variable")
+ vars
include (val data : S with type t = Printer_tag.localizable)
end
@@ -122,8 +164,18 @@ struct
let model = States.model () in
let () =
States.column
- ~name:"kind" ~descr:(Md.plain "Marker kind")
- ~data:(module MarkerKind) ~get:fst
+ ~name:"kind"
+ ~descr:(Md.plain "Marker kind")
+ ~data:(module MarkerKind)
+ ~get:fst
+ model
+ in
+ let () =
+ States.column
+ ~name:"var"
+ ~descr:(Md.plain "Marker variable")
+ ~data:(module MarkerVar)
+ ~get:fst
model
in
let () =
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 5c30a704fbcb1fc5e59c9b7bbcf611adc6091460..09877676a76673136ad2b7a7f7f179ec8cadfbdd 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -22,8 +22,13 @@
open Server
-let package = Package.package ~plugin:"eva"
- ~title:"Eva General Services" ~readme:"eva.md" ()
+let package =
+ Package.package
+ ~plugin:"eva"
+ ~name:"general"
+ ~title:"Eva General Services"
+ ~readme:"eva.md"
+ ()
module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..85d2df413cded868f8088cdb2d72602a095ca4ac
--- /dev/null
+++ b/src/plugins/value/api/values_request.ml
@@ -0,0 +1,366 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Server
+open Data
+open Cil_types
+module Md = Markdown
+
+let package =
+ Package.package
+ ~plugin:"eva"
+ ~name:"values"
+ ~title:"Eva Values"
+ ~readme:"eva.md"
+ ()
+
+type value =
+ { value: string;
+ alarm: bool; }
+
+type evaluation =
+ | Unreachable
+ | Evaluation of value
+
+type after =
+ | Unchanged
+ | Reduced of evaluation
+
+type before_after =
+ { before: evaluation;
+ after_instr: after option;
+ after_then: after option;
+ after_else: after option; }
+
+type values =
+ { values: before_after;
+ callstack: (Value_util.callstack * before_after) list option; }
+
+let get_value = function
+ | Unreachable -> "Unreachable"
+ | Evaluation { value } -> value
+
+let get_alarm = function
+ | Unreachable -> false
+ | Evaluation { alarm } -> alarm
+
+let get_after_value =
+ Extlib.opt_map
+ (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
+
+module CallStackId =
+ Data.Index
+ (Value_types.Callstack.Map)
+ (struct
+ let name = "eva-callstack-id"
+ end)
+
+(* This pretty-printer drops the toplevel kf, which is always the function
+ in which we are pretty-printing the expression/term *)
+let pretty_callstack fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt callsite) :: q -> begin
+ let rec aux callsite = function
+ | (kf, callsite') :: q -> begin
+ Format.fprintf fmt "%a (%a)"
+ Kernel_function.pretty kf
+ Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite);
+ match callsite' with
+ | Kglobal -> ()
+ | Kstmt callsite' ->
+ Format.fprintf fmt " â†@ ";
+ aux callsite' q
+ end
+ | _ -> assert false
+ in
+ Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
+ aux callsite q;
+ Format.fprintf fmt "@]"
+ end
+ | _ -> assert false
+
+(* This pretty-printer prints only the lists of the functions, not
+ the locations. *)
+let pretty_callstack_short fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt _callsite) :: q ->
+ Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
+ Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
+ (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
+ | _ -> assert false
+
+module CallStack = struct
+ type record
+
+ let record: record Record.signature = Record.signature ()
+
+ let id = Record.field record ~name:"id"
+ ~descr:(Md.plain "Callstack id") (module Jint)
+ let short = Record.field record ~name:"short"
+ ~descr:(Md.plain "Short name for the callstack") (module Jstring)
+ let full = Record.field record ~name:"full"
+ ~descr:(Md.plain "Full name for the callstack") (module Jstring)
+
+ module R =
+ (val
+ (Record.publish
+ ~package
+ ~name:"callstack"
+ ~descr:(Md.plain "CallStack")
+ record) : Record.S with type r = record)
+
+ type t = Value_types.callstack option
+
+ let jtype = R.jtype
+
+ let pp_callstack ~short = function
+ | None -> if short then "all" else ""
+ | Some callstack ->
+ let pp_text =
+ if short
+ then Pretty_utils.to_string ~margin:50 pretty_callstack_short
+ else Pretty_utils.to_string pretty_callstack
+ in
+ (pp_text callstack)
+
+ let id_callstack = function
+ | None -> -1
+ | Some callstack -> CallStackId.get callstack
+
+ let to_json callstack =
+ R.default |>
+ R.set id (id_callstack callstack) |>
+ R.set short (pp_callstack ~short:true callstack) |>
+ R.set full (pp_callstack ~short:false callstack) |>
+ R.to_json
+
+ let key = function
+ | None -> "all"
+ | Some callstack -> string_of_int (CallStackId.get callstack)
+end
+
+
+let consolidated = ref None
+let table = Hashtbl.create 100
+
+let iter f =
+ if Hashtbl.length table > 1
+ then Extlib.may (fun values -> f (None, values)) !consolidated;
+ Hashtbl.iter (fun key data -> f (Some key, data)) table
+
+let array =
+ let model = States.model () in
+ let () =
+ States.column
+ ~name:"callstack"
+ ~descr:(Md.plain "CallStack")
+ ~data:(module CallStack)
+ ~get:fst
+ model
+ in
+ let () =
+ States.column
+ ~name:"value_before"
+ ~descr:(Md.plain "Value inferred just before the selected point")
+ ~data:(module Jstring)
+ ~get:(fun (_, e) -> get_value e.before)
+ model
+ in
+ let () =
+ States.column
+ ~name:"alarm"
+ ~descr:(Md.plain "Did the evaluation led to an alarm?")
+ ~data:(module Jbool)
+ ~get:(fun (_, e) -> get_alarm e.before)
+ model
+ in
+ let () =
+ States.column
+ ~name:"value_after"
+ ~descr:(Md.plain "Value inferred just after the selected point")
+ ~data:(module Joption(Jstring))
+ ~get:(fun (_, e) -> get_after_value e.after_instr)
+ model
+ in
+ States.register_array
+ ~package
+ ~name:"values"
+ ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
+ ~key:(fun (cs, _) -> CallStack.key cs)
+ ~iter
+ model
+
+let update_values values =
+ Hashtbl.clear table;
+ consolidated := Some values.values;
+ let () =
+ match values.callstack with
+ | None -> ()
+ | Some by_callstack ->
+ List.iter
+ (fun (callstack, before_after) ->
+ Hashtbl.add table callstack before_after)
+ by_callstack
+ in
+ States.reload array
+
+module type S = sig
+ val evaluate: kinstr -> exp -> values
+ val lvaluate: kinstr -> lval -> values
+end
+
+module Make (Eva: Analysis.S) : S = struct
+
+ let make_before eval before =
+ let before =
+ match before with
+ | `Bottom -> Unreachable
+ | `Value state -> Evaluation (eval state)
+ in
+ { before; after_instr = None; after_then = None; after_else = None; }
+
+ let make_callstack stmt eval =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ match before with
+ | (`Bottom | `Top) -> []
+ | `Value before ->
+ let aux callstack before acc =
+ let before_after = make_before eval (`Value before) in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make_before_after eval ~before ~after =
+ match before with
+ | `Bottom ->
+ { before = Unreachable;
+ after_instr = None;
+ after_then = None;
+ after_else = None; }
+ | `Value before ->
+ let before = eval before in
+ let after_instr =
+ match after with
+ | `Bottom -> Some (Reduced Unreachable)
+ | `Value after ->
+ let after = eval after in
+ if String.equal before.value after.value
+ then Some Unchanged
+ else Some (Reduced (Evaluation after))
+ in
+ { before = Evaluation before;
+ after_instr; after_then = None; after_else = None; }
+
+ let make_instr_callstack stmt eval =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ let after = Eva.get_stmt_state_by_callstack ~after:true stmt in
+ match before, after with
+ | (`Bottom | `Top), _
+ | _, (`Bottom | `Top) -> []
+ | `Value before, `Value after ->
+ let aux callstack before acc =
+ let before = `Value before in
+ let after =
+ try `Value (Value_types.Callstack.Hashtbl.find after callstack)
+ with Not_found -> `Bottom
+ in
+ let before_after = make_before_after eval ~before ~after in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make eval kinstr =
+ let before = Eva.get_kinstr_state ~after:false kinstr in
+ let values, callstack =
+ match kinstr with
+ | Cil_types.Kglobal ->
+ make_before eval before, None
+ | Cil_types.Kstmt stmt ->
+ match stmt.skind with
+ | Instr _ ->
+ let after = Eva.get_kinstr_state ~after:true kinstr in
+ let values = make_before_after eval ~before ~after in
+ let callstack = make_instr_callstack stmt eval in
+ values, Some callstack
+ | _ ->
+ make_before eval before, Some (make_callstack stmt eval)
+ in
+ { values; callstack; }
+
+
+ let evaluate kinstr expr =
+ let eval state =
+ let value, alarms = Eva.eval_expr state expr in
+ let alarm = not (Alarmset.is_empty alarms) in
+ let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
+ { value = str; alarm }
+ in
+ make eval kinstr
+
+ let lvaluate kinstr lval =
+ let eval state =
+ let value, alarms = Eva.copy_lvalue state lval in
+ let alarm = not (Alarmset.is_empty alarms) in
+ let flagged_value = match value with
+ | `Bottom -> Eval.Flagged_Value.bottom
+ | `Value v -> v
+ in
+ let pretty = Eval.Flagged_Value.pretty Eva.Val.pretty in
+ let str = Format.asprintf "%a" pretty flagged_value in
+ { value = str; alarm }
+ in
+ make eval kinstr
+end
+
+
+let ref_request =
+ let module Analyzer = (val Analysis.current_analyzer ()) in
+ ref (module Make (Analyzer) : S)
+
+let hook (module Analyzer: Analysis.S) =
+ ref_request := (module Make (Analyzer) : S)
+
+let () = Analysis.register_hook hook
+
+
+let update tag =
+ let module Request = (val !ref_request) in
+ match tag with
+ | Printer_tag.PExp (_kf, kinstr, expr) ->
+ update_values (Request.evaluate kinstr expr)
+ | Printer_tag.PLval (_kf, kinstr, lval) ->
+ update_values (Request.lvaluate kinstr lval)
+ | PVDecl (_kf, kinstr, varinfo) ->
+ update_values (Request.lvaluate kinstr (Var varinfo, NoOffset))
+ | _ -> ()
+
+let () =
+ Server.Request.register
+ ~package
+ ~kind:`GET
+ ~name:"getValues"
+ ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
+ ~input:(module Kernel_ast.Marker)
+ ~output:(module Junit)
+ update
diff --git a/src/plugins/value/api/values_request.mli b/src/plugins/value/api/values_request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/value/api/values_request.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)