diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 40bf034596919523dba48b67e06bb05d0d6a69d2..3cf0aa6167a7d830ff1ac6c00efac554b9f49824 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -528,4 +528,49 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
+/** <markerFromTerm> input */
+export interface markerFromTermInput {
+ /** The statement at which we will build the marker. */
+ at_stmt: marker;
+ /** The ACSL term. */
+ term: string;
+}
+
+/** Loose decoder for `markerFromTermInput` */
+export const jMarkerFromTermInput: Json.Loose<markerFromTermInput> =
+ Json.jObject({
+ at_stmt: jMarkerSafe,
+ term: Json.jFail(Json.jString,'String expected'),
+ });
+
+/** Safe decoder for `markerFromTermInput` */
+export const jMarkerFromTermInputSafe: Json.Safe<markerFromTermInput> =
+ Json.jFail(jMarkerFromTermInput,'MarkerFromTermInput expected');
+
+/** Natural order for `markerFromTermInput` */
+export const byMarkerFromTermInput: Compare.Order<markerFromTermInput> =
+ Compare.byFields
+ <{ at_stmt: marker, term: string }>({
+ at_stmt: byMarker,
+ term: Compare.string,
+ });
+
+const markerFromTerm_internal: Server.GetRequest<
+ markerFromTermInput,
+ marker |
+ undefined
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.markerFromTerm',
+ input: jMarkerFromTermInput,
+ output: jMarker,
+ signals: [],
+};
+/** Build a marker from an ACSL term. */
+export const markerFromTerm: Server.GetRequest<
+ markerFromTermInput,
+ marker |
+ undefined
+ >= markerFromTerm_internal;
+
/* ------------------------------------- */
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 24d4223a9170fdb5fe946480fed241ed943d432e..55d8b6b7768e3e1717a91f126b192ce459c819bd 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -580,41 +580,4 @@ export const functionStats: State.Array<
functionStatsData
> = functionStats_internal;
-/** <evalTerm> input */
-export interface evalTermInput {
- /** The statement at which we will perform the evaluation. */
- at_stmt: marker;
- /** The term to be evaluated. */
- term: string;
-}
-
-/** Loose decoder for `evalTermInput` */
-export const jEvalTermInput: Json.Loose<evalTermInput> =
- Json.jObject({
- at_stmt: jMarkerSafe,
- term: Json.jFail(Json.jString,'String expected'),
- });
-
-/** Safe decoder for `evalTermInput` */
-export const jEvalTermInputSafe: Json.Safe<evalTermInput> =
- Json.jFail(jEvalTermInput,'EvalTermInput expected');
-
-/** Natural order for `evalTermInput` */
-export const byEvalTermInput: Compare.Order<evalTermInput> =
- Compare.byFields
- <{ at_stmt: marker, term: string }>({
- at_stmt: byMarker,
- term: Compare.string,
- });
-
-const evalTerm_internal: Server.GetRequest<evalTermInput,marker | undefined> = {
- kind: Server.RqKind.GET,
- name: 'plugins.eva.general.evalTerm',
- input: jEvalTermInput,
- 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,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 8a33bd72c34fb791010b901304fb26bf21fd84ee..143e13562d771da204a991dd5a60478981e26213 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -925,7 +925,7 @@ function useEvaluationMode(props: EvaluationModeProps): void {
const onEnter = (pattern: string): void => {
const marker = selection?.current?.marker;
const data = { at_stmt: marker, term: pattern };
- Server.send(Eva.evalTerm, data).then(addProbe).catch(handleError);
+ Server.send(Ast.markerFromTerm, data).then(addProbe).catch(handleError);
};
const evalMode = {
title: 'Evaluation',
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 84d21cb8a070f28a812fe2a47965b64a0191e041..83e79307fbb54d277ebf9b0e8fa82d931a6afe55 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -746,3 +746,64 @@ let () =
set_files
(* -------------------------------------------------------------------------- *)
+(* ----- Build a marker from an ACSL term ----------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+type marker_term_input = { at_stmt : stmt ; term : string }
+
+module MarkerTermInput = struct
+ type record
+ let record : record Record.signature = Record.signature ()
+
+ let at_stmt =
+ let descr = "The statement at which we will build the marker." in
+ Record.field record ~name:"at_stmt" ~descr:(Markdown.plain descr)
+ (module Marker)
+
+ let term =
+ let descr = "The ACSL term." in
+ Record.field record ~name:"term" ~descr:(Markdown.plain descr)
+ (module Data.Jstring)
+
+ let data =
+ Record.publish record ~package ~name:"markerFromTermInput"
+ ~descr:(Markdown.plain "<markerFromTerm> input")
+
+ module R : Record.S with type r = record = (val data)
+ type t = marker_term_input option
+ let jtype = R.jtype
+
+ let of_json js =
+ let record = R.of_json js in
+ match R.get at_stmt record with
+ | PStmt (_, s) | PStmtStart (_, s)
+ | PLval (_, Kstmt s, _) | PExp (_, Kstmt s, _)
+ | PTermLval (_, Kstmt s, _, _)
+ | PVDecl (_, Kstmt s, _) ->
+ let term = R.get term record in
+ Some { at_stmt = s ; term }
+ | _ -> None
+
+end
+
+module MarkerTermOutput = Data.Joption (Marker)
+
+let logic_environment () =
+ let open Logic_typing in
+ Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
+
+let build_marker = Option.map @@ fun input ->
+ 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 exp = !Db.Properties.Interp.term_to_exp ~result:None term in
+ Printer_tag.PExp (Some kf, Kstmt input.at_stmt, exp)
+
+let descr = "Build a marker from an ACSL term."
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"markerFromTerm" ~descr:(Markdown.plain descr)
+ ~input:(module MarkerTermInput) ~output:(module MarkerTermOutput)
+ build_marker
+
+(**************************************************************************)
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 2845e11f2633ab9186da245cebc19e07221a69f9..8053dcd4eee70529da2424b8b09cb8371a66745d 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -468,68 +468,4 @@ let _array =
model
-(* ----- Arbitrary ACSL term evaluation ------------------------------------- *)
-
-type eval_term_input = { at_stmt : stmt ; term : string }
-
-module EvalTermInput = struct
- open Server.Data
- type record
- let record : record Record.signature = Record.signature ()
-
- let at_stmt =
- let descr = "The statement at which we will perform the evaluation." in
- Record.field record ~name:"at_stmt" ~descr:(Markdown.plain descr)
- (module Kernel_ast.Marker)
-
- let term =
- let descr = "The term to be evaluated." in
- Record.field record ~name:"term" ~descr:(Markdown.plain descr)
- (module Data.Jstring)
-
- let data =
- Record.publish record ~package ~name:"evalTermInput"
- ~descr:(Markdown.plain "<evalTerm> input")
-
- module R : Record.S with type r = record = (val data)
- type t = eval_term_input option
- let jtype = R.jtype
-
- let of_json js =
- let record = R.of_json js in
- match R.get at_stmt record with
- | PStmt (_, s) | PStmtStart (_, s)
- | PLval (_, Kstmt s, _) | PExp (_, Kstmt s, _)
- | PTermLval (_, Kstmt s, _, _)
- | PVDecl (_, Kstmt s, _) ->
- let term = R.get term record in
- Some { at_stmt = s ; term }
- | _ -> None
-
-end
-
-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 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 exp = !Db.Properties.Interp.term_to_exp ~result:None term in
- Printer_tag.PExp (Some kf, Kstmt input.at_stmt, exp)
-
-let descr =
- "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."
-
-let () = Request.register ~package
- ~kind:`GET ~name:"evalTerm" ~descr:(Markdown.plain descr)
- ~input:(module EvalTermInput) ~output:(module EvalTermOutput)
- evaluate_term
-
-
(**************************************************************************)