From 95ddbd6f07111dca1d77cdd82658ec610496e8fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 18 Dec 2020 17:46:43 +0100
Subject: [PATCH] [ivette/eva] show alarms
---
ivette/src/frama-c/eva/Values.tsx | 41 +++++++++++++++++++++++++++----
ivette/src/frama-c/eva/layout.ts | 4 ++-
ivette/src/frama-c/eva/model.ts | 6 ++++-
ivette/src/frama-c/eva/style.css | 16 +++++++++++-
4 files changed, 59 insertions(+), 8 deletions(-)
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index 3392392807d..ee3bb0c523f 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -7,7 +7,7 @@ import React from 'react';
import * as Dome from 'dome';
import { classes } from 'dome/misc/utils';
import { VariableSizeList } from 'react-window';
-import { Vfill, Hpack, Filler } from 'dome/layout/boxes';
+import { Vfill, Hpack, Vpack, Filler } from 'dome/layout/boxes';
import { Icon } from 'dome/controls/icons';
import { Label, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
@@ -26,7 +26,7 @@ import * as Ast from 'frama-c/api/kernel/ast';
// Locals
import { SizedArea, HSIZER, WSIZER } from './sized';
import { Diff } from './diffed';
-import { sizeof, valueAt, diffAfter, diffThen, diffElse } from './cells';
+import { sizeof, valueAt, diffAfter, diffThen, diffElse, EvaAlarm } from './cells';
import { Row } from './layout';
import { Probe } from './probes';
import { Callsite } from './stacks';
@@ -149,14 +149,44 @@ function ProbeInfos() {
);
}
+// --------------------------------------------------------------------------
+// --- Alarms Panel
+// --------------------------------------------------------------------------
+
+function AlarmsInfo() {
+ const model = useModel();
+ const probe = model.getFocused();
+ if (probe) {
+ const callstack = model.getCallstack();
+ const domain =
+ model.values.getValues(probe.marker, probe.stmt, callstack);
+ const alarms = domain?.alarms ?? [];
+ if (alarms.length > 0) {
+ console.log('ALARMS', alarms);
+ const renderAlarm = ([status, alarm]: EvaAlarm) => {
+ const className = `eva-alarm-info eva-alarm-${status}`;
+ return (
+ <Code className={className} icon='WARNING'>{alarm}</Code>
+ );
+ };
+ return (
+ <Vpack className="eva-info">
+ {alarms.map(renderAlarm)}
+ </Vpack>
+ );
+ }
+ }
+ return null;
+}
+
// --------------------------------------------------------------------------
// --- Stack Panel
// --------------------------------------------------------------------------
-function StackInfos() {
+function StackInfo() {
const model = useModel();
const [, setSelection] = States.useSelection();
- const callstack = model.getCallstack();
+ const callstack = model.getCalls();
if (callstack.length <= 1) return null;
const makeCallsite = ({ caller, stmt, rank }: Callsite) => {
if (!caller || !stmt) return null;
@@ -425,7 +455,8 @@ function ValuesComponent() {
)}
</AutoSizer>
</Vfill>
- <StackInfos />
+ <AlarmsInfo />
+ <StackInfo />
</Vfill>
</>
);
diff --git a/ivette/src/frama-c/eva/layout.ts b/ivette/src/frama-c/eva/layout.ts
index d31e9c7f53a..61dc7f4d11e 100644
--- a/ivette/src/frama-c/eva/layout.ts
+++ b/ivette/src/frama-c/eva/layout.ts
@@ -30,6 +30,7 @@ export interface Row {
/* --------------------------------------------------------------------------*/
const PADDING = 2;
+const INSET = 1;
const HCROP = 18;
const VCROP = 1;
@@ -64,7 +65,8 @@ export class LayoutEngine {
private rows: Row[] = [];
crop(zoomed: boolean, s: Size): Size {
- const cols = zoomed ? s.cols : Math.min(s.cols, this.hcrop);
+ const s_cols = s.cols + INSET;
+ const cols = zoomed ? s_cols : Math.min(s_cols, this.hcrop);
const rows = zoomed ? s.rows : Math.min(s.rows, this.vcrop);
return {
cols: Math.max(HCROP, cols),
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
index 1ee86bc301a..6f24c809c84 100644
--- a/ivette/src/frama-c/eva/model.ts
+++ b/ivette/src/frama-c/eva/model.ts
@@ -109,7 +109,11 @@ export class Model implements ModelCallbacks {
return cs !== undefined ? cs === row.callstack : false;
}
- getCallstack(): Callsite[] {
+ getCallstack(): Values.callstack | undefined {
+ return this.callstack;
+ }
+
+ getCalls(): Callsite[] {
const c = this.callstack;
return c === undefined ? [] : this.stacks.getCalls(c);
}
diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css
index 81387ed81fb..12ff6e4916e 100644
--- a/ivette/src/frama-c/eva/style.css
+++ b/ivette/src/frama-c/eva/style.css
@@ -144,14 +144,28 @@
.eva-state-Then .eva-diff { background: green; }
.eva-state-Else .eva-diff { background: orange; }
+/* -------------------------------------------------------------------------- */
+/* --- Alarms --- */
+/* -------------------------------------------------------------------------- */
+
.eva-cell-alarms {
- fill: red;
+ fill: orange;
position: absolute;
top: -1px;
right: 3px;
z-index: 1;
}
+.eva-alarm-info {
+ font-size: x-small;
+ padding: 0px;
+ margin: 1px;
+}
+
+.eva-alarm-True { fill: green; }
+.eva-alarm-False { fill: red; }
+.eva-alarm-Unknown { fill: darkorange; }
+
/* -------------------------------------------------------------------------- */
/* --- Table Rows Background --- */
/* -------------------------------------------------------------------------- */
--
GitLab