From f1a9b0af81ada31049cebcf9acbfae540af790d3 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 9 Feb 2022 13:15:38 +0100
Subject: [PATCH] [ivette] Simplifying the server request
---
.../frama-c/plugins/eva/api/general/index.ts | 24 ++++---------------
ivette/src/frama-c/plugins/eva/valuetable.tsx | 17 +++++++------
src/plugins/value/api/general_requests.ml | 20 ++++------------
3 files changed, 16 insertions(+), 45 deletions(-)
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 44a3298c83d..24d4223a917 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -584,8 +584,6 @@ export const functionStats: State.Array<
export interface evalTermInput {
/** The statement at which we will perform the evaluation. */
at_stmt: marker;
- /** If true, evaluation is performed after <at_stmt> computation. */
- after: boolean;
/** The term to be evaluated. */
term: string;
}
@@ -594,7 +592,6 @@ export interface evalTermInput {
export const jEvalTermInput: Json.Loose<evalTermInput> =
Json.jObject({
at_stmt: jMarkerSafe,
- after: Json.jFail(Json.jBoolean,'Boolean expected'),
term: Json.jFail(Json.jString,'String expected'),
});
@@ -605,32 +602,19 @@ export const jEvalTermInputSafe: Json.Safe<evalTermInput> =
/** Natural order for `evalTermInput` */
export const byEvalTermInput: Compare.Order<evalTermInput> =
Compare.byFields
- <{ at_stmt: marker, after: boolean, term: string }>({
+ <{ at_stmt: marker, term: string }>({
at_stmt: byMarker,
- after: Compare.boolean,
term: Compare.string,
});
-const evalTerm_internal: Server.GetRequest<
- evalTermInput,
- [ string, marker ] |
- undefined
- > = {
+const evalTerm_internal: Server.GetRequest<evalTermInput,marker | undefined> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.evalTerm',
input: jEvalTermInput,
- output: Json.jTry(
- Json.jPair(
- Json.jFail(Json.jString,'String expected'),
- jMarkerSafe,
- )),
+ output: jMarker,
signals: [],
};
/** Evaluate a term in the abstract state of a given statement. The evaluation is performed after the statement computation if the given boolean is true. */
-export const evalTerm: Server.GetRequest<
- evalTermInput,
- [ string, marker ] |
- undefined
- >= evalTerm_internal;
+export const evalTerm: Server.GetRequest<evalTermInput,marker | undefined>= evalTerm_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 80c5bba7a93..2d49bf5af7a 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -913,19 +913,18 @@ interface EvaluationModeProps {
setLocPin: (loc: Location, pin: boolean) => void;
}
-function evaluationMode(props: EvaluationModeProps): void {
+function useEvaluationMode(props: EvaluationModeProps): void {
const { computationState, selection, setLocPin } = props;
- const handleError = (): void => {};
- const addProbe = (result: [ string, Ast.marker ] | undefined): void => {
+ const handleError = (): void => { return; };
+ const addProbe = (target: Ast.marker | undefined): void => {
const fct = selection?.current?.fct;
- const [_, loc] = result ?? [];
- if (fct && loc) setLocPin({ fct, target: loc }, true);
+ if (fct && target) setLocPin({ fct, target }, true);
};
React.useEffect(() => {
- if (computationState !== 'computed') return () => {}
- const onEnter = (pattern: string) => {
+ if (computationState !== 'computed') return () => { return; };
+ const onEnter = (pattern: string): void => {
const marker = selection?.current?.marker;
- const data = { at_stmt: marker, after: true, term: pattern };
+ const data = { at_stmt: marker, term: pattern };
Server.send(Eva.evalTerm, data).then(addProbe).catch(handleError);
};
const evalMode = {
@@ -1111,7 +1110,7 @@ function EvaTable(): JSX.Element {
/* Handle Evaluation mode */
const computationState = States.useSyncValue(Eva.computationState);
- evaluationMode({ computationState, selection, setLocPin });
+ useEvaluationMode({ computationState, selection, setLocPin });
/* Builds the component */
return (
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 66203d23203..2845e11f263 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -470,7 +470,7 @@ let _array =
(* ----- Arbitrary ACSL term evaluation ------------------------------------- *)
-type eval_term_input = { at_stmt : stmt ; after : bool ; term : string }
+type eval_term_input = { at_stmt : stmt ; term : string }
module EvalTermInput = struct
open Server.Data
@@ -482,11 +482,6 @@ module EvalTermInput = struct
Record.field record ~name:"at_stmt" ~descr:(Markdown.plain descr)
(module Kernel_ast.Marker)
- let after =
- let descr = "If true, evaluation is performed after <at_stmt> computation." in
- Record.field record ~name:"after" ~descr:(Markdown.plain descr)
- (module Data.Jbool)
-
let term =
let descr = "The term to be evaluated." in
Record.field record ~name:"term" ~descr:(Markdown.plain descr)
@@ -507,31 +502,24 @@ module EvalTermInput = struct
| PLval (_, Kstmt s, _) | PExp (_, Kstmt s, _)
| PTermLval (_, Kstmt s, _, _)
| PVDecl (_, Kstmt s, _) ->
- let after = R.get after record in
let term = R.get term record in
- Some { at_stmt = s; after ; term }
+ Some { at_stmt = s ; term }
| _ -> None
end
-module EvalTermOutput =
- Data.Joption (Data.Jpair (Data.Jstring) (Kernel_ast.Marker))
+module EvalTermOutput = Data.Joption (Kernel_ast.Marker)
let logic_environment () =
let open Logic_typing in
Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
let evaluate_term = Option.map @@ fun input ->
- let open Eval_terms in
let env = logic_environment () in
let kf = Kernel_function.find_englobing_kf input.at_stmt in
let term = !Db.Properties.Interp.term ~env kf input.term in
- let state = Db.Value.get_stmt_state ~after:input.after input.at_stmt in
- let v = (eval_term ~alarm_mode:Ignore (env_only_here state) term).eover in
let exp = !Db.Properties.Interp.term_to_exp ~result:None term in
- let loc = Printer_tag.PExp (Some kf, Kstmt input.at_stmt, exp) in
- Format.fprintf Format.str_formatter "%a" Cvalue.V.pretty v ;
- (Format.flush_str_formatter (), loc)
+ Printer_tag.PExp (Some kf, Kstmt input.at_stmt, exp)
let descr =
"Evaluate a term in the abstract state of a given statement. \
--
GitLab