diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx index ca4f8da2be526eedeea49fcc9fca34abf01e8a28..be4845187da7c108616b84d6ab715fb7732b2345 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 9d3579ba0b302412089088a1a7e96d56ea3a0c79..3ed2ea6b595d436fd82035130a5f13647d828103 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 0a981edd2760bf3fd68aaca570a94593e553945a..eb76164294fca8a88a3e39f3c1937a952a9308e1 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