Merge branch 'feature/ivette/pointed_value' into 'master'

[ivette] Display lvalues through pointers and pretty offsetmaps

See merge request frama-c/frama-c!3436

ivette/src/frama-c/api/generated/plugins/eva/values/index.ts

@@ -176,4 +176,27 @@ export const getValues: Server.GetRequest<
     alarms: [ "True" | "False" | "Unknown", string ][] }
   >= getValues_internal;
 
+const getPointedLvalues_internal: Server.GetRequest<
+  { callstack?: callstack, pointer: marker },
+  { lvalues?: [ string, marker ][] }
+  > = {
+  kind: Server.RqKind.GET,
+  name:   'plugins.eva.values.getPointedLvalues',
+  input:  Json.jObject({ callstack: jCallstack, pointer: jMarkerSafe,}),
+  output: Json.jObject({
+            lvalues: Json.jList(
+                       Json.jTry(
+                         Json.jPair(
+                           Json.jFail(Json.jString,'String expected'),
+                           jMarkerSafe,
+                         ))),
+          }),
+  signals: [],
+};
+/** Pointed lvalues for the given marker */
+export const getPointedLvalues: Server.GetRequest<
+  { callstack?: callstack, pointer: marker },
+  { lvalues?: [ string, marker ][] }
+  >= getPointedLvalues_internal;
+
 /* ------------------------------------- */

ivette/src/frama-c/plugins/eva/model.ts

@@ -92,6 +92,17 @@ export class Model implements ModelCallbacks {
     return undefined;
   }
 
+  addProbe(location: States.Location) {
+    const { fct, marker } = location;
+    if (fct && marker) {
+      const probe = new Probe(this, fct, marker);
+      probe.setPersistent();
+      probe.requestProbeInfo();
+      this.probes.set(marker, probe);
+      this.forceLayout();
+    }
+  }
+
   getStacks(p: Probe | undefined): Values.callstack[] {
     return p ? this.stacks.getStacks(p.marker) : [];
   }

ivette/src/frama-c/plugins/eva/sized.tsx

@@ -109,7 +109,7 @@ export class FontSizer {
 /* --------------------------------------------------------------------------*/
 
 export const WSIZER = new FontSizer(7, 6);
-export const HSIZER = new FontSizer(14, 6);
+export const HSIZER = new FontSizer(15, 6);
 
 export interface SizedAreaProps {
   cols: number;

ivette/src/frama-c/plugins/eva/valuetable.tsx

@@ -27,6 +27,8 @@
 // React & Dome
 import React from 'react';
 import * as Dome from 'dome';
+import * as Server from 'frama-c/server';
+import * as Values from 'frama-c/api/plugins/eva/values';
 import { classes } from 'dome/misc/utils';
 import { VariableSizeList } from 'react-window';
 import { Hpack, Filler } from 'dome/layout/boxes';
@@ -49,6 +51,8 @@ import { Callsite } from './stacks';
 import { Stmt } from './valueinfos';
 import './style.css';
 
+const D = new Dome.Debug('Source Code');
+
 // --------------------------------------------------------------------------
 // --- Cell Diffs
 // --------------------------------------------------------------------------
@@ -177,12 +181,31 @@ function TableCell(props: TableCellProps) {
     probe.setPersistent();
     if (probe.zoomable) probe.setZoomed(!probe.zoomed);
   };
+
+  async function onContextMenu() {
+    Server
+      .send(Values.getPointedLvalues, { pointer: marker, callstack })
+      .then((r) => {
+        const lvalues = r.lvalues ?? [];
+        const items: Dome.PopupMenuItem[] = lvalues.map((lval) => {
+          const [text, lvalMarker] = lval;
+          const label = `Display values for ${text}`;
+          const location = { fct: probe.fct, marker: lvalMarker };
+          const onItemClick = () => model.addProbe(location);
+          return { label, onClick: onItemClick };
+        });
+        if (items.length > 0) Dome.popupMenu(items);
+      })
+      .catch((err) => D.error(`Fail to recover pointed lvalues: ${err}`));
+  }
+
   return (
     <div
       className={className}
       style={style}
       onClick={onClick}
       onDoubleClick={onDoubleClick}
+      onContextMenu={onContextMenu}
     >
       {contents}
     </div>

src/kernel_services/abstract_interp/bottom.ml

@@ -140,6 +140,10 @@ module Bound_Lattice
   let is_included = is_included Lattice.is_included
 end
 
+let to_option = function
+  | `Bottom -> None
+  | `Value v -> Some v
+
 let to_list = function
   | `Bottom  -> []
   | `Value v -> [v]

src/kernel_services/abstract_interp/bottom.mli

@@ -70,6 +70,7 @@ module Bound_Lattice
     the empty list is the bottom case. *)
 
 (** Conversion functions. *)
+val to_option : 'a or_bottom -> 'a option
 val to_list: 'a or_bottom -> 'a list
 val bot_of_list: 'a list -> 'a list or_bottom
 val list_of_bot: 'a list or_bottom -> 'a list

src/plugins/value/alarmset.ml

@@ -188,6 +188,10 @@ let iter f = function
   | Just m -> M.iter f m
   | AllBut _ -> assert false
 
+let fold f acc = function
+  | Just m -> M.fold f m acc
+  | AllBut _ -> assert false
+
 let exists test ~default = function
   | Just m -> M.exists test m || default True
   | AllBut m -> M.exists test m || default Unknown

src/plugins/value/alarmset.mli

@@ -98,6 +98,7 @@ val exists: (alarm -> status -> bool) -> default:(status -> bool) -> t -> bool
 val for_all: (alarm -> status -> bool) -> default:(status -> bool) -> t -> bool
 
 val iter: (alarm -> status -> unit) -> t -> unit
+val fold : (alarm -> status -> 'a -> 'a) -> 'a -> t -> 'a
 
 (** Emits the alarms according to the given warn mode, at the given
     instruction. *)