From a46527cd5e90e5f9c0b42d13cef2a00d22536d2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Jun 2022 13:55:38 +0200
Subject: [PATCH] [Ivette] Eva domain states: adds a checkbox to print the
entire domain state.
---
.../src/frama-c/plugins/eva/DomainStates.tsx | 19 ++++++++++++++++---
.../frama-c/plugins/eva/api/general/index.ts | 10 +++++++---
src/plugins/value/api/general_requests.ml | 13 +++++++++----
3 files changed, 32 insertions(+), 10 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
index ca4f8da2be5..be4845187da 100644
--- a/ivette/src/frama-c/plugins/eva/DomainStates.tsx
+++ b/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"
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 9d3579ba0b3..3ed2ea6b595 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/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;
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 0a981edd276..eb76164294f 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/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
--
GitLab