diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 907787a07bc9b6d5ee54ea6b5263e640ff437866..7f6dc684a7e408b10805a21a16ebd90cdf9033da 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 a03ba1c9bf6e1662f13fbaabbbd9fa7eff102525..992743ff4c890b8cce406f532cc797df62d110dc 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -202,27 +202,21 @@ function filterAlarm(alarm: string | undefined): boolean {
}
function filterEva(p: Property): boolean {
- let b = true;
if ('priority' in p && p.priority === false && filter('eva.priority_only'))
- b = false;
+ return false;
if ('taint' in p) {
switch (p.taint) {
case 'not_tainted':
case 'not_applicable':
- if (filter('eva.data_tainted_only') || filter('eva.ctrl_tainted_only'))
- b = false;
- break;
- case 'data_tainted':
- if (filter('eva.ctrl_tainted_only'))
- b = false;
- break;
- case 'control_tainted':
- if (filter('eva.data_tainted_only'))
- b = false;
- break;
+ return !filter('eva.data_tainted_only') &&
+ !filter('eva.ctrl_tainted_only');
+ case 'direct_taint':
+ return !(filter('eva.ctrl_tainted_only'));
+ case 'indirect_taint':
+ return !(filter('eva.data_tainted_only'));
}
}
- return b;
+ return true;
}
function filterProperty(p: Property): boolean {
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 932488fecae57980244f4ec7f97e0d99a4db764a..fe8ebaddbc40f66b911d413addc181aa30b8f865 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/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 0cc4595adf33d3b1fd1d4afe1a6329010a34775d..cf5797288c8a25bac16d62fbdfff5c641d670080 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -247,12 +247,12 @@ export enum taintStatus {
error = 'error',
/** **Not applicable:** no taint for this kind of property */
not_applicable = 'not_applicable',
- /** **Data tainted:**
+ /** **Direct taint:**
this property is related to a memory location that can be affected by an attacker */
- data_tainted = 'data_tainted',
- /** **Control tainted:**
+ direct_taint = 'direct_taint',
+ /** **Indirect taint:**
this property is related to a memory location whose assignment depends on path conditions that can be affected by an attacker */
- control_tainted = 'control_tainted',
+ indirect_taint = 'indirect_taint',
/** **Untainted property:** this property is safe */
not_tainted = 'not_tainted',
}
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index df135da7849fbc957d259dbdf022611f6cd5107c..9a535134ce61730528cc9ed81d7eb2c3fe3c5af9 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -289,6 +289,22 @@ module Results: sig
(** Memory zone read to compute data addresses. *)
}
+ (** Taint of a memory zone, according to the taint domain. *)
+ type taint =
+ | Direct
+ (** Direct data dependency from values provided by the attacker to the given
+ memory zone, meaning that the attacker may be able to alter its value. *)
+ | Indirect
+ (** Indirect dependency from values provided by the attacker to the given
+ memory zone. The attacker cannot directly alter this memory, but he may
+ be able to impact on the path by which its value is computed. *)
+ | Untainted
+ (** No taint: the given memory zone cannot be modified by the attacker. *)
+
+ (** Evaluates the taint of a given memory zone, according to the taint domain.
+ Returns an error if the taint domain was not enabled. *)
+ val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
+
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
val expr_dependencies : Cil_types.exp -> request -> deps
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index e5e522cdd535b6c06febe29b902ffa85661deffc..af6c92b62aeadc55eb1666d4ff39e73cee6ac886 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -161,33 +161,95 @@ let () = Request.register ~package
(* ----- Register Eva information ------------------------------------------- *)
+let term_lval_to_lval tlval =
+ try !Db.Properties.Interp.term_lval_to_lval ~result:None tlval
+ with Db.Properties.Interp.No_conversion -> raise Not_found
+
let print_value fmt loc =
- let stmt, eval =
+ let is_scalar = Cil.isScalarType in
+ let kinstr, eval =
match loc with
- | Printer_tag.PLval (_kf, Kstmt stmt, lval)
- when Cil.isScalarType (Cil.typeOfLval lval) ->
- stmt, Results.eval_lval lval
- | Printer_tag.PExp (_kf, Kstmt stmt, expr)
- when Cil.isScalarType (Cil.typeOf expr) ->
- stmt, Results.eval_exp expr
+ | Printer_tag.PLval (_kf, ki, lval) when is_scalar (Cil.typeOfLval lval) ->
+ ki, Results.eval_lval lval
+ | Printer_tag.PExp (_kf, ki, expr) when is_scalar (Cil.typeOf expr) ->
+ ki, Results.eval_exp expr
+ | PVDecl (_kf, ki, vi) when is_scalar vi.vtype ->
+ ki, Results.eval_var vi
+ | PTermLval (_kf, ki, _ip, tlval) ->
+ let lval = term_lval_to_lval tlval in
+ ki, Results.eval_lval lval
| _ -> raise Not_found
in
- let eval_cvalue at = Results.(at stmt |> eval |> as_cvalue_or_uninitialized) in
- let before = eval_cvalue Results.before in
- let after = eval_cvalue Results.after in
let pretty = Cvalue.V_Or_Uninitialized.pretty in
- if Cvalue.V_Or_Uninitialized.equal before after
- then pretty fmt before
- else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+ let eval_cvalue at = Results.(eval at |> as_cvalue_or_uninitialized) in
+ let before = eval_cvalue (Results.before_kinstr kinstr) in
+ match kinstr with
+ | Kglobal -> pretty fmt before
+ | Kstmt stmt ->
+ let after = eval_cvalue (Results.after stmt) in
+ if Cvalue.V_Or_Uninitialized.equal before after
+ then pretty fmt before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
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
+let print_taint fmt marker =
+ let loc = Cil_datatype.Location.unknown in
+ let expr, stmt =
+ match marker with
+ | Printer_tag.PLval (_kf, Kstmt stmt, lval) ->
+ Cil.new_exp ~loc (Lval lval), stmt
+ | Printer_tag.PExp (_kf, Kstmt stmt, expr) -> expr, stmt
+ | PVDecl (_kf, Kstmt stmt, vi) ->
+ Cil.new_exp ~loc (Lval (Var vi, NoOffset)), stmt
+ | PTermLval (_kf, Kstmt stmt, _ip, tlval) ->
+ let lval = term_lval_to_lval tlval in
+ Cil.new_exp ~loc (Lval lval), stmt
+ | _ -> raise Not_found
+ in
+ let evaluate_taint request =
+ let deps = Results.expr_dependencies expr request in
+ Result.get_ok (Results.is_tainted deps.data request),
+ Result.get_ok (Results.is_tainted deps.indirect request)
+ in
+ let before = evaluate_taint Results.(before stmt) in
+ let after = evaluate_taint Results.(after stmt) in
+ let str_taint = function
+ | Results.Untainted -> "untainted"
+ | Direct -> "direct taint"
+ | Indirect -> "indirect taint"
+ in
+ let pretty fmt = let open Results in function
+ | taint, Untainted -> Format.fprintf fmt "%s" (str_taint taint)
+ | t1, t2 ->
+ Format.fprintf fmt
+ "%s to the value, %s %s to values used to compute lvalues addresses"
+ (str_taint t1) (if t1 = Untainted then "but" else "and") (str_taint t2)
+ in
+ if before = after
+ then Format.fprintf fmt "%a" pretty before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+
+let () =
+ let enable () = Analysis.is_computed () && Taint_domain.Store.is_computed () in
+ let title =
+ "Taint status:\n\
+ - Direct taint: data dependency from values provided by the attacker, \
+ meaning that the attacker may be able to alter this value\n\
+ - Indirect taint: the attacker cannot directly alter this value, but he \
+ may be able to impact the path by which its value is computed.\n\
+ - Untainted: cannot be modified by the attacker."
+ in
+ Server.Kernel_ast.Information.register
+ ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
+ ~title ~enable print_taint
+
let () =
Analysis.register_computation_hook
(fun _ -> Server.Kernel_ast.Information.update ())
@@ -196,7 +258,9 @@ let () =
module Taint = struct
open Server.Data
- open Taint_domain
+
+ type taint = Results.taint = Direct | Indirect | Untainted
+ type error = NotComputed | Irrelevant | LogicError
let dictionary = Enum.dictionary ()
@@ -220,39 +284,69 @@ module Taint = struct
tag (Error Irrelevant) "not_applicable" "—"
"Not applicable" "no taint for this kind of property"
- let tag_data_tainted =
- tag (Ok Data) "data_tainted" "Tainted (data)"
- "Data tainted"
+ let tag_direct_taint =
+ tag (Ok Direct) "direct_taint" "Tainted (direct)"
+ "Direct taint"
"this property is related to a memory location that can be affected \
by an attacker"
- let tag_control_tainted =
- tag (Ok Control) "control_tainted" "Tainted (control)"
- "Control tainted"
+ let tag_indirect_taint =
+ tag (Ok Indirect) "indirect_taint" "Tainted (indirect)"
+ "Indirect taint"
"this property is related to a memory location whose assignment depends \
on path conditions that can be affected by an attacker"
let tag_untainted =
- tag (Ok None) "not_tainted" "Untainted"
+ tag (Ok Untainted) "not_tainted" "Untainted"
"Untainted property" "this property is safe"
let () = Enum.set_lookup dictionary
begin function
- | Error Taint_domain.NotComputed -> tag_not_computed
- | Error Taint_domain.Irrelevant -> tag_not_applicable
- | Error Taint_domain.LogicError -> tag_error
- | Ok Data -> tag_data_tainted
- | Ok Control -> tag_control_tainted
- | Ok None -> tag_untainted
+ | Error NotComputed -> tag_not_computed
+ | Error Irrelevant -> tag_not_applicable
+ | Error LogicError -> tag_error
+ | Ok Direct -> tag_direct_taint
+ | Ok Indirect -> tag_indirect_taint
+ | Ok Untainted -> tag_untainted
end
let data = Request.dictionary ~package ~name:"taintStatus"
~descr:(Markdown.plain "Taint status of logical properties") dictionary
- include (val data : S with type t = taint_result)
+ include (val data : S with type t = (taint, error) result)
+
+ let zone_of_predicate kinstr predicate =
+ let state = Results.(before_kinstr kinstr |> get_cvalue_model) in
+ let env = Eval_terms.env_only_here state in
+ let logic_deps = Eval_terms.predicate_deps env predicate in
+ match Option.map Cil_datatype.Logic_label.Map.bindings logic_deps with
+ | Some [ BuiltinLabel Here, zone ] -> Ok zone
+ | _ -> Error LogicError
+
+ let get_predicate = function
+ | Property.IPCodeAnnot ica ->
+ begin
+ match ica.ica_ca.annot_content with
+ | AAssert (_, predicate) | AInvariant (_, _, predicate) ->
+ Ok predicate.tp_statement
+ | _ -> Error Irrelevant
+ end
+ | IPPropertyInstance { ii_pred = None } -> Error LogicError
+ | IPPropertyInstance { ii_pred = Some ip } -> Ok ip.ip_content.tp_statement
+ | _ -> Error Irrelevant
+
+ let is_tainted_property ip =
+ if not (Analysis.is_computed () && Taint_domain.Store.is_computed ())
+ then Error NotComputed
+ else
+ let (let+) = Result.bind in
+ let kinstr = Property.get_kinstr ip in
+ let+ predicate = get_predicate ip in
+ let+ zone = zone_of_predicate kinstr predicate in
+ let result = Results.(before_kinstr kinstr |> is_tainted zone) in
+ Result.map_error (fun _ -> NotComputed) result
end
-
let model = States.model ()
let () = States.column model ~name:"priority"
@@ -265,7 +359,7 @@ let () = States.column model ~name:"taint"
~descr:(Markdown.plain "Is the property tainted according to \
the Eva taint domain?")
~data:(module Taint)
- ~get:(fun ip -> Taint_domain.is_tainted_property ip)
+ ~get:(fun ip -> Taint.is_tainted_property ip)
let _array =
States.register_array
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index f32bc939b956f7adb1b141cb95258b418d0bb4fb..95ea09a4a544a6ab00a9f0624547c84d57f67bf0 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -24,7 +24,7 @@ open Cil_types
open Cil_datatype
open Locations
-type taint = {
+type taint_state = {
(* Over-approximation of the memory locations that are tainted due to a data
dependency. *)
locs_data: Zone.t;
@@ -73,7 +73,7 @@ module LatticeTaint = struct
include Datatype.Make_with_collections(struct
include Datatype.Serializable_undefined
- type t = taint
+ type t = taint_state
let name = "taint"
@@ -296,7 +296,7 @@ end
module TaintDomain = struct
- type state = taint
+ type state = taint_state
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin
@@ -595,48 +595,11 @@ let flag =
let () = Abstractions.register_hook interpret_taint_logic
-type taint_error = NotComputed | Irrelevant | LogicError
-type taint_ok = Data | Control | None
-type taint_result = (taint_ok, taint_error) result
-
-let zone_of_predicate env predicate =
- let logic_deps = Eval_terms.predicate_deps env predicate in
- let deps_list = Option.map Logic_label.Map.bindings logic_deps in
- match deps_list with
- | Some [ BuiltinLabel Here, zone ] -> Ok zone
- | _ -> Error LogicError
-
-let get_predicate = function
- | Property.IPCodeAnnot ica ->
- begin
- match ica.ica_ca.annot_content with
- | AAssert (_, predicate) | AInvariant (_, _, predicate) ->
- Ok predicate.tp_statement
- | _ -> Error Irrelevant
- end
- | IPPropertyInstance { ii_pred = None } -> Error LogicError
- | IPPropertyInstance { ii_pred = Some pred } -> Ok pred.ip_content.tp_statement
- | _ -> Error Irrelevant
-
-let get_stmt ip =
- let kinstr = Property.get_kinstr ip in
- match kinstr with
- | Kglobal -> Error Irrelevant
- | Kstmt stmt -> Ok stmt
-
-let is_tainted_property ip =
- let (let+) = Result.bind in
- if not (Store.is_computed ()) then Error NotComputed else
- let+ stmt = get_stmt ip in
- let+ predicate = get_predicate ip in
- match Store.get_stmt_state ~after:false stmt with
- | `Bottom -> Ok None
- | `Value state ->
- let cvalue = Db.Value.get_stmt_state ~after:false stmt in
- let env = Eval_terms.env_only_here cvalue in
- let+ zone = zone_of_predicate env predicate in
- if Zone.intersects zone state.locs_data
- then Ok Data
- else if Zone.intersects zone state.locs_control
- then Ok Control
- else Ok None
+type taint = Direct | Indirect | Untainted
+
+let is_tainted { locs_data ; locs_control } ?indirect zone =
+ let intersects_any z = Zone.(intersects (join locs_data locs_control) z) in
+ let is_indirect () = Option.fold indirect ~none:false ~some:intersects_any in
+ if Zone.intersects zone locs_data then Direct
+ else if Zone.intersects zone locs_control || is_indirect () then Indirect
+ else Untainted
diff --git a/src/plugins/eva/domains/taint_domain.mli b/src/plugins/eva/domains/taint_domain.mli
index 7d911a85ec3668bf67076ed7444bab8d9445c60c..263dcf4d714fd2b52e1c8cacc9e643994163b888 100644
--- a/src/plugins/eva/domains/taint_domain.mli
+++ b/src/plugins/eva/domains/taint_domain.mli
@@ -28,25 +28,9 @@ include Abstract_domain.Leaf
val flag: Abstractions.flag
-type taint_error =
- | NotComputed (** The Eva analysis has not been run, or the taint domain
- was not enabled. *)
- | Irrelevant (** Properties other than assertions, invariants and
- preconditions are irrelevant here. *)
- | LogicError (** The memory zone on which the property depends could not
- be computed. *)
+type taint = | Direct | Indirect | Untainted
-type taint_ok =
- | Data (** Data-taint: there is a data dependency from the values provided
- by the attacker to the given property, meaning that the attacker
- may alter the values on which the property depends. *)
- | Control (** Control-taint: there is a control-dependency from the values
- provided by the attacker to the given property. The attacker
- cannot directly alter the values on which the property depends,
- but he may be able to choose the path where these values are
- computed. *)
- | None (** No taint: the property cannot be altered by the attacker. *)
-
-type taint_result = (taint_ok, taint_error) result
-
-val is_tainted_property: Property.t -> taint_result
+(** Is a memory zone tainted according to a given state?Â
+ If [indirect] is provided, return an [Indirect] taint if [indirect] is
+ tainted (either directly or indirectly). *)
+val is_tainted: state -> ?indirect:Locations.Zone.t -> Locations.Zone.t -> taint
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index c7b44e783a11eac858a3a04e99a7e9d4f670b308..d57d536e50ba076ac5d30445a6fb8abbaa1cf401 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -320,6 +320,11 @@ struct
| Some extract ->
convert (Response.map_join extract Cvalue.Model.join (get req))
+ let get_state req key join =
+ match A.Dom.get key with
+ | None -> Result.error DisabledDomain
+ | Some extract -> convert (Response.map_join extract join (get req))
+
let print_states ?filter req =
let state = Response.map_join (fun x -> x) A.Dom.join (get req) in
let print (type s)
@@ -738,6 +743,15 @@ let expr_dependencies expr request =
let lval_to_loc lv = eval_address lv request |> as_precise_loc in
Eva_utils.deps_of_expr lval_to_loc expr
+(* Taint *)
+
+type taint = Taint_domain.taint = Direct | Indirect | Untainted
+
+let is_tainted zone request =
+ let module M = Make () in
+ let state = M.get_state request Taint_domain.key Taint_domain.join in
+ Result.map (fun state -> Taint_domain.is_tainted state zone) state
+
(* Reachability *)
let is_empty rq =
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index ec7bc51d785b9b4c67436b2af5f527584a4412d6..d221fe82aa36ff2d69860d31e068065918aa475d 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -194,6 +194,22 @@ type deps = Function_Froms.Deps.deps = {
(** Memory zone read to compute data addresses. *)
}
+(** Taint of a memory zone, according to the taint domain. *)
+type taint =
+ | Direct
+ (** Direct data dependency from values provided by the attacker to the given
+ memory zone, meaning that the attacker may be able to alter its value. *)
+ | Indirect
+ (** Indirect dependency from values provided by the attacker to the given
+ memory zone. The attacker cannot directly alter this memory, but he may
+ be able to impact on the path by which its value is computed. *)
+ | Untainted
+ (** No taint: the given memory zone cannot be modified by the attacker. *)
+
+(** Evaluates the taint of a given memory zone, according to the taint domain.
+ Returns an error if the taint domain was not enabled. *)
+val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
+
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
val expr_dependencies : Cil_types.exp -> request -> deps
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index a50aeb4f09d790b283cb68bf813a6ca8b6b7ae71..1abf9ab1efbf4e4770fe1f41c422085f0397eef8 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 bda08edd105c008e283deb57aa911bd7ab69d398..c8e0c52dc788c6e55d2f35ce48def72e3e954a40 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 *)