[Ivette] Eva domain states: adds a checkbox to print the entire domain state.

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

@@ -29,20 +29,23 @@ import * as Eva from 'frama-c/plugins/eva/api/general';
 import * as Boxes from 'dome/layout/boxes';
 import { HSplit } from 'dome/layout/splitters';
 import { Text } from 'frama-c/richtext';
-import { Select } from 'dome/controls/buttons';
+import { Checkbox, Select } from 'dome/controls/buttons';
 import { Label } from 'dome/controls/labels';
 
-const globalSelectedDomain = new GlobalState<string>("");
+const globalSelectedDomain = new GlobalState("");
+const globalFilter = new GlobalState(true);
 
 export function EvaStates(): JSX.Element {
   const [selection] = States.useSelection();
   const selectedLoc = selection?.current;
   const marker = selectedLoc?.marker;
-  const states = States.useRequest(Eva.getStates, marker);
   const [domains, setDomains] = React.useState<string[]>([]);
   const [selected, setSelected] = useGlobalState(globalSelectedDomain);
   const [stateBefore, setStateBefore] = React.useState("");
   const [stateAfter, setStateAfter] = React.useState("");
+  const [filter, setFilter] = useGlobalState(globalFilter);
+
+  const states = States.useRequest(Eva.getStates, [marker, filter]);
 
   React.useEffect(() => {
     if (states && states.length > 0) {
@@ -78,6 +81,16 @@ export function EvaStates(): JSX.Element {
         >
           {list}
         </Select>
+        <Boxes.Filler/>
+        <Checkbox
+          label="Filtered state"
+          title="If enabled, only the part of the states relevant to the
+        selected marker are shown, for domains supporting this feature.
+        For other domains or if disabled, entire domain states are printed.
+        Beware that entire domain states can be very large."
+          value={filter}
+          onChange={setFilter}
+        />
       </Boxes.Hbox>
       <HSplit
         settings="ivette.eva.domainStates.beforeAfterSplit"

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

@@ -581,12 +581,16 @@ export const functionStats: State.Array<
   > = functionStats_internal;
 
 const getStates_internal: Server.GetRequest<
-  marker,
+  [ marker, boolean ],
   [ string, string, string ][]
   > = {
   kind: Server.RqKind.GET,
   name:   'plugins.eva.general.getStates',
-  input:  jMarker,
+  input:  Json.jTry(
+            Json.jPair(
+              jMarkerSafe,
+              Json.jFail(Json.jBoolean,'Boolean expected'),
+            )),
   output: Json.jList(
             Json.jTry(
               Json.jTriple(
@@ -598,7 +602,7 @@ const getStates_internal: Server.GetRequest<
 };
 /** Get the domain states about the given marker */
 export const getStates: Server.GetRequest<
-  marker,
+  [ marker, boolean ],
   [ string, string, string ][]
   >= getStates_internal;
 

src/plugins/value/api/general_requests.ml

@@ -514,13 +514,18 @@ let get_filtered_state request marker =
     then []
     else Results.print_states ~filter:bases request
 
-let get_states marker =
+let get_state filter request marker =
+  if filter
+  then get_filtered_state request marker
+  else Results.print_states request
+
+let get_states (marker, filter) =
   let kinstr = Printer_tag.ki_of_localizable marker in
   match kinstr with
   | Kglobal -> []
   | Kstmt stmt ->
-    let states_before = get_filtered_state (Results.before stmt) marker in
-    let states_after = get_filtered_state (Results.after stmt) marker in
+    let states_before = get_state filter (Results.before stmt) marker in
+    let states_after = get_state filter (Results.after stmt) marker in
     match states_before, states_after with
     | [], _ -> List.map (fun (name, after) -> name, "", after) states_after
     | _, [] -> List.map (fun (name, before) -> name, before, "") states_before
@@ -534,7 +539,7 @@ let get_states marker =
 let () = Request.register ~package
     ~kind:`GET ~name:"getStates"
     ~descr:(Markdown.plain "Get the domain states about the given marker")
-    ~input:(module Kernel_ast.Marker)
+    ~input:(module Data.Jpair (Kernel_ast.Marker) (Data.Jbool))
     ~output:(module Data.Jlist
           (Data.Jtriple (Data.Jstring) (Data.Jstring) (Data.Jstring)))
     get_states