From 535b1f37109e82daf2a31ce01825b495af8ff7a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Sep 2022 16:51:09 +0200
Subject: [PATCH] [server] Information: adds an optional longer description,
shown as title.
[descr] is used in the dropdown list of information kinds.
[title] is used as tooltip on the information.
---
ivette/src/frama-c/kernel/ASTinfo.tsx | 16 +++++++---------
ivette/src/frama-c/kernel/Properties.tsx | 4 ++--
ivette/src/frama-c/kernel/api/ast/index.ts | 7 ++++---
src/plugins/eva/api/general_requests.ml | 2 +-
src/plugins/server/kernel_ast.ml | 17 ++++++++++-------
src/plugins/server/kernel_ast.mli | 8 +++++---
6 files changed, 29 insertions(+), 25 deletions(-)
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 907787a07bc..7f6dc684a7e 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -80,20 +80,17 @@ function markerKind (props: AST.markerInfoData): JSX.Element {
interface InfoItemProps {
label: string;
title: string;
- descr: DATA.text;
+ text: DATA.text;
}
function InfoItem(props: InfoItemProps): JSX.Element {
return (
<div className="astinfo-infos">
- <div
- className="dome-text-label astinfo-kind"
- title={props.title}
- >
+ <div className="dome-text-label astinfo-kind" title={props.title}>
{props.label}
</div>
- <div className="dome-text-cell astinfo-data">
- <Text text={props.descr} />
+ <div className="dome-text-cell astinfo-data" title={props.title}>
+ <Text text={props.text} />
</div>
</div>
);
@@ -102,8 +99,9 @@ function InfoItem(props: InfoItemProps): JSX.Element {
interface ASTinfos {
id: string;
label: string;
+ descr: string;
title: string;
- descr: DATA.text;
+ text: DATA.text;
}
interface InfoSectionProps {
@@ -281,7 +279,7 @@ function openFilter(
};
return {
id: info.id,
- label: `${info.title} (${info.label})`,
+ label: `${info.descr} (${info.label})`,
checked,
onClick,
};
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index a03ba1c9bf6..724e84c6564 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -212,11 +212,11 @@ function filterEva(p: Property): boolean {
if (filter('eva.data_tainted_only') || filter('eva.ctrl_tainted_only'))
b = false;
break;
- case 'data_tainted':
+ case 'direct_taint':
if (filter('eva.ctrl_tainted_only'))
b = false;
break;
- case 'control_tainted':
+ case 'indirect_taint':
if (filter('eva.data_tainted_only'))
b = false;
break;
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 932488fecae..fe8ebaddbc4 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -462,7 +462,7 @@ export const getInformationUpdate: Server.Signal = {
const getInformation_internal: Server.GetRequest<
marker |
undefined,
- { id: string, label: string, title: string, descr: text }[]
+ { id: string, label: string, descr: string, title: string, text: text }[]
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getInformation',
@@ -471,8 +471,9 @@ const getInformation_internal: Server.GetRequest<
Json.jObject({
id: Json.jFail(Json.jString,'String expected'),
label: Json.jFail(Json.jString,'String expected'),
+ descr: Json.jFail(Json.jString,'String expected'),
title: Json.jFail(Json.jString,'String expected'),
- descr: jTextSafe,
+ text: jTextSafe,
})),
signals: [ { name: 'kernel.ast.getInformationUpdate' } ],
};
@@ -480,7 +481,7 @@ const getInformation_internal: Server.GetRequest<
export const getInformation: Server.GetRequest<
marker |
undefined,
- { id: string, label: string, title: string, descr: text }[]
+ { id: string, label: string, descr: string, title: string, text: text }[]
>= getInformation_internal;
const getMarkerAt_internal: Server.GetRequest<
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index e5e522cdd53..691e7f73881 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -184,7 +184,7 @@ let () =
Server.Kernel_ast.Information.register
~id:"eva.value"
~label:"Value"
- ~title:"Possible values inferred by Eva"
+ ~descr:"Possible values inferred by Eva"
~enable:Analysis.is_computed
print_value
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index a50aeb4f09d..1abf9ab1efb 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -577,6 +577,7 @@ struct
id: string;
rank: int;
label: string;
+ descr: string;
title: string;
enable: unit -> bool;
pretty: Format.formatter -> Printer_tag.localizable -> unit
@@ -590,15 +591,17 @@ struct
let jtype = Package.(Jrecord[
"id", Jstring ;
"label", Jstring ;
+ "descr", Jstring ;
"title", Jstring ;
- "descr", Jtext.jtype ;
+ "text", Jtext.jtype ;
])
let of_json _ = failwith "Information.Info"
let to_json (info,text) = `Assoc [
"id", `String info.id ;
"label", `String info.label ;
+ "descr", `String info.descr ;
"title", `String info.title ;
- "descr", text ;
+ "text", text ;
]
end
@@ -640,9 +643,9 @@ struct
let update () = Request.emit signal
- let register ~id ~label ~title ?(enable = fun _ -> true) pretty =
+ let register ~id ~label ~descr ?(title = descr) ?(enable = fun _ -> true) pretty =
let rank = incr rankId ; !rankId in
- let info = { id ; rank ; label ; title ; enable ; pretty } in
+ let info = { id ; rank ; label ; descr; title ; enable ; pretty } in
if Hashtbl.mem registry id then
( let msg = Format.sprintf
"Server.Kernel_ast.register_info: duplicate %S" id in
@@ -669,7 +672,7 @@ let () = Request.register ~package
let () = Information.register
~id:"kernel.ast.location"
~label:"Location"
- ~title:"Source file location"
+ ~descr:"Source file location"
begin fun fmt loc ->
let location = Printer_tag.loc_of_localizable loc in
Filepath.pp_pos fmt (fst location)
@@ -678,7 +681,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.varinfo"
~label:"Var"
- ~title:"Variable Information"
+ ~descr:"Variable Information"
begin fun fmt loc ->
match loc with
| PLval (_ , _, (Var x,NoOffset)) | PVDecl(_,_,x) ->
@@ -702,7 +705,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.typeinfo"
~label:"Type"
- ~title:"Type of C/ASCL expression"
+ ~descr:"Type of C/ASCL expression"
begin fun fmt loc ->
let open Printer in
match loc with
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index bda08edd105..c8e0c52dc78 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -71,15 +71,17 @@ sig
(**
Registers a marker information printer.
Identifier [id] shall be unique.
- Label [label] shall be very short.
- Description shall succinctly describe the kind of information.
+ [label] shall be very short.
+ [descr] shall succinctly describe the kind of information.
+ [title] is an optional longer explanation for the kind of information.
If the optional [enable] function is provided, the information printer is
only used when [enable ()] returns true.
The printer is allowed to raise [Not_found] exception when there is no
information for the localizable.
*)
val register :
- id:string -> label:string -> title:string -> ?enable:(unit -> bool) ->
+ id:string -> label:string -> descr:string -> ?title:string ->
+ ?enable:(unit -> bool) ->
(Format.formatter -> Printer_tag.localizable -> unit) -> unit
(** Updated information signal *)
--
GitLab