From a4f72af3a9c7452a9dcc1ba7538fe04ff9e2833e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 24 Jan 2023 09:07:30 +0100
Subject: [PATCH] [server] actually parse expressions
---
ivette/src/frama-c/kernel/ASTview.tsx | 7 +-
ivette/src/frama-c/kernel/Locations.tsx | 7 +-
ivette/src/frama-c/plugins/eva/Coverage.tsx | 5 +-
ivette/src/frama-c/plugins/eva/valuetable.tsx | 2 +-
ivette/src/frama-c/states.ts | 4 +-
src/plugins/dive/dive_graph.ml | 4 +-
src/plugins/dive/server_interface.ml | 4 +-
src/plugins/eva/api/general_requests.ml | 54 +++----
src/plugins/eva/api/values_request.ml | 12 +-
src/plugins/server/kernel_ast.ml | 150 +++++++++---------
src/plugins/server/kernel_ast.mli | 41 ++++-
src/plugins/server/kernel_main.ml | 2 +-
src/plugins/server/kernel_properties.ml | 4 +-
src/plugins/studia/studia_request.ml | 2 +-
14 files changed, 162 insertions(+), 136 deletions(-)
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index acf1959aabd..35e03a34f87 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -481,8 +481,9 @@ function createContextMenuHandler(): Editor.Extension {
const items: Dome.PopupMenuItem[] = [];
const attrs = getData(node.id);
if (attrs?.isFunDecl) {
- const groupedCallers = Lodash.groupBy(callers, e => e.kf);
- const locations = callers.map((l) => ({ fct: l.kf, marker: l.stmt }));
+ const groupedCallers = Lodash.groupBy(callers, (cs) => cs.kf);
+ const locations =
+ callers.map(({ kf, stmt }) => ({ fct: kf, marker: stmt }));
Lodash.forEach(groupedCallers, (e) => {
const callerName = e[0].kf;
const callSites = e.length > 1 ? `(${e.length} call sites)` : '';
@@ -495,7 +496,7 @@ function createContextMenuHandler(): Editor.Extension {
})
});
});
- } else if (attrs?.isFun) {
+ } else if (attrs?.isFunction) {
const location = { fct: attrs.name };
const onClick = (): void => update({ location });
const label = `Go to definition of ${attrs.name}`;
diff --git a/ivette/src/frama-c/kernel/Locations.tsx b/ivette/src/frama-c/kernel/Locations.tsx
index 7f955a475a6..559470bcfbe 100644
--- a/ivette/src/frama-c/kernel/Locations.tsx
+++ b/ivette/src/frama-c/kernel/Locations.tsx
@@ -27,14 +27,13 @@
import React from 'react';
import * as States from 'frama-c/states';
-import * as Json from 'dome/data/json';
import { CompactModel } from 'dome/table/arrays';
import { Table, Column, Renderer } from 'dome/table/views';
import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { Space } from 'dome/frame/toolbars';
import { TitleBar } from 'ivette';
-import { markerAttributes } from 'frama-c/kernel/api/ast';
+import { markerAttributes, jMarker } from 'frama-c/kernel/api/ast';
// --------------------------------------------------------------------------
// --- Locations Panel
@@ -56,8 +55,8 @@ export default function LocationsTable(): JSX.Element {
// Renderer for statement markers.
const renderMarker: Renderer<string> =
(loc: string) => {
- const markerId = (loc as Json.key<'#markerInfo'>);
- const info = markersInfo.getData(markerId);
+ const marker = jMarker(loc);
+ const info = markersInfo.getData(marker);
const sloc = info?.sloc;
const position = `${sloc?.base}:${sloc?.line}`;
return <Label label={position} title={info?.descr} />;
diff --git a/ivette/src/frama-c/plugins/eva/Coverage.tsx b/ivette/src/frama-c/plugins/eva/Coverage.tsx
index 69fd1bf7ce9..cad3b95c356 100644
--- a/ivette/src/frama-c/plugins/eva/Coverage.tsx
+++ b/ivette/src/frama-c/plugins/eva/Coverage.tsx
@@ -21,7 +21,6 @@
/* ************************************************************************ */
import React from 'react';
-import * as Json from 'dome/data/json';
import { Table, Column } from 'dome/table/views';
import { CompactModel } from 'dome/table/arrays';
import * as Arrays from 'dome/table/arrays';
@@ -29,10 +28,10 @@ import * as Compare from 'dome/data/compare';
import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
+import * as Ast from 'frama-c/kernel/api/ast';
import * as Eva from 'frama-c/plugins/eva/api/general';
import CoverageMeter, { percent } from './CoverageMeter';
-type key = Json.key<'#fundec'>;
type stats = Eva.functionStatsData;
// --- Coverage Table ---
@@ -71,7 +70,7 @@ const ordering: Arrays.ByColumns<stats> = {
),
};
-class Model extends CompactModel<key, stats> {
+class Model extends CompactModel<Ast.fct, stats> {
constructor() {
super(Eva.functionStats.getkey);
this.setColumnOrder(ordering);
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 5e103a1f5aa..e1623636885 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -933,7 +933,7 @@ function useEvaluationMode(props: EvaluationModeProps): void {
const onEnter = (pattern: string): void => {
const marker = selection?.current?.marker;
const data = { stmt: marker, term: pattern };
- Server.send(Ast.parseTerm, data).then(addProbe).catch(handleError);
+ Server.send(Ast.parseExpr, data).then(addProbe).catch(handleError);
};
const evalMode = {
label: 'Evaluation',
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index ea4469337c9..6025b56eafc 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -799,14 +799,14 @@ export async function resetSelection(): Promise<void> {
export type attributes = Ast.markerAttributesData;
export const defaultMarker: attributes = {
- key: '',
+ marker: Ast.jMarker(''),
labelKind: '',
titleKind: '',
name: '',
descr: '',
isLval: false,
isFunDecl: false,
- isFun: false,
+ isFunction: false,
sloc: { dir: '', base: '', file: '', line: 0 },
};
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 3fedc30df0e..b2416baa851 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -270,9 +270,7 @@ let ouptput_to_dot out_channel g =
module JsonPrinter =
struct
- let output_stmt stmt =
- let kf = Kernel_function.find_englobing_kf stmt in
- Server.Kernel_ast.KfMarker.to_json (kf, PStmtStart (kf, stmt))
+ let output_stmt = Server.Kernel_ast.Stmt.to_json
let output_kinstr = function
| Cil_types.Kglobal -> `String "global"
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index bfff3fc2128..9ca69ddd6ea 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -193,7 +193,7 @@ struct
"is_root", Jboolean;
"backward_explored", Jstring;
"forward_explored", Jstring;
- "writes", Jarray Kernel_ast.KfMarker.jtype;
+ "writes", Jarray Kernel_ast.Location.jtype;
"values", Joption Jstring;
"range", Junion [ Jnumber ; Jstring ];
"type", Joption Jstring;
@@ -211,7 +211,7 @@ struct
"src", NodeId.jtype ;
"dst", NodeId.jtype ;
"kind", Jstring ;
- "origins", Jarray Kernel_ast.KfMarker.jtype
+ "origins", Jarray Kernel_ast.Location.jtype
])
end
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index fdb4c9cb1f3..75d3f5312fd 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -57,39 +57,35 @@ let _computation_signal =
~add_hook:Analysis.register_computation_hook
()
-
-
(* ----- Callsites ---------------------------------------------------------- *)
-module CallSite = struct
- open Data
- type callsite
- let record: callsite Record.signature = Record.signature ()
-
- let kf_field = Record.field record ~name:"kf"
- ~descr:(Markdown.plain "Function") (module Kernel_ast.Kf)
-
- let stmt_field = Record.field record ~name:"stmt"
- ~descr:(Markdown.plain "Statement") (module Kernel_ast.Stmt)
-
- let data = Record.publish ~package ~name:"CallSite"
- ~descr:(Markdown.plain "CallSite") record
-
- module R : Record.S with type r = callsite = (val data)
-
- let convert (kf, stmts) = stmts |> List.map @@ fun stmt ->
- R.default |> R.set kf_field kf |> R.set stmt_field stmt
-
- let callers kf = Results.callsites kf |> List.map convert |> List.concat
-
- let () = Request.register ~package
- ~kind:`GET ~name:"getCallers"
- ~descr:(Markdown.plain "Get the list of call site of a function")
- ~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (R))
- callers
+module CallSite =
+struct
+ type t = kernel_function * stmt
+ let jtype = Data.declare ~package ~name:"CallSite"
+ ~descr:(Markdown.plain "Call site, combining function and stmt")
+ (Jrecord [
+ "kf", Kernel_ast.Function.jtype;
+ "stmt", Kernel_ast.Stmt.jtype;
+ ])
+ let to_json (kf,stmt) = `Assoc [
+ "kf", Kernel_ast.Function.to_json kf;
+ "stmt", Kernel_ast.Stmt.to_json stmt;
+ ]
+ let of_json js =
+ Json.field "fct" js |> Kernel_ast.Function.of_json,
+ Json.field "stmt" js |> Kernel_ast.Stmt.of_json
end
+let callers kf =
+ let list = Results.callsites kf in
+ List.concat (List.map (fun (kf, l) -> List.map (fun s -> kf, s) l) list)
+let () = Request.register ~package
+ ~kind:`GET ~name:"getCallers"
+ ~descr:(Markdown.plain "Get the list of call site of a function")
+ ~input:(module Kernel_ast.Function) ~output:(module Data.Jlist (CallSite))
+ callers
(* ----- Functions ---------------------------------------------------------- *)
@@ -180,7 +176,7 @@ let () = Request.register ~package
~kind:`GET ~name:"getDeadCode"
~descr:(Markdown.plain "Get the lists of unreachable and of non terminating \
statements in a function")
- ~input:(module Kernel_ast.Kf)
+ ~input:(module Kernel_ast.Function)
~output:(module DeadCode)
dead_code
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index b8ba7218782..72290c183f6 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -31,7 +31,7 @@ module CSet = CS.Set
module CSmap = CS.Hashtbl
module Md = Markdown
-module Jkf = Kernel_ast.Kf
+module Jfct = Kernel_ast.Function
module Jstmt = Kernel_ast.Stmt
module Jmarker = Kernel_ast.Marker
@@ -209,8 +209,8 @@ module Jcalls : Request.Output with type t = callstack = struct
type t = callstack
let jtype = Package.(Jarray (Jrecord [
- "callee" , Jkf.jtype ;
- "caller" , Joption Jkf.jtype ;
+ "callee" , Jfct.jtype ;
+ "caller" , Joption Jfct.jtype ;
"stmt" , Joption Jstmt.jtype ;
"rank" , Joption Jnumber ;
]))
@@ -219,7 +219,7 @@ module Jcalls : Request.Output with type t = callstack = struct
match ki , cs with
| Kglobal , _ | _ , [] -> [ `Assoc [ "callee", jcallee ] ]
| Kstmt stmt , (called,ki) :: cs ->
- let jcaller = Jkf.to_json called in
+ let jcaller = Jfct.to_json called in
let callsite = `Assoc [
"callee", jcallee ;
"caller", jcaller ;
@@ -231,7 +231,7 @@ module Jcalls : Request.Output with type t = callstack = struct
let to_json = function
| [] -> `List []
- | (callee,ki)::cs -> `List (jcallstack (Jkf.to_json callee) ki cs)
+ | (callee,ki)::cs -> `List (jcallstack (Jfct.to_json callee) ki cs)
end
@@ -512,7 +512,7 @@ let () =
let getStmtInfo = Request.signature ~input:(module Jstmt) () in
let set_fct = Request.result getStmtInfo ~name:"fct"
~descr:(Md.plain "Englobing function")
- (module Jkf)
+ (module Jfct)
and set_rank = Request.result getStmtInfo ~name:"rank"
~descr:(Md.plain "Global stmt order")
(module Jint)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 1a5e672aac8..403d0724a15 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -92,6 +92,39 @@ struct
end
+(* -------------------------------------------------------------------------- *)
+(* --- Functions --- *)
+(* -------------------------------------------------------------------------- *)
+
+let jFunction = Data.declare ~package ~name:"fct"
+ ~descr:(Md.plain "Function names")
+ (Pkg.Jkey "fct")
+
+module Function =
+struct
+ type t = kernel_function
+ let jtype = jFunction
+ let to_json kf =
+ `String (Kernel_function.get_name kf)
+ let of_json js =
+ let fn = Js.to_string js in
+ try Globals.Functions.find_by_name fn
+ with Not_found -> Data.failure "Undefined function '%s'" fn
+end
+
+module Fundec =
+struct
+ type t = fundec
+ let jtype = jFunction
+ let to_json fundec =
+ `String fundec.svar.vname
+ let of_json js =
+ let fn = Js.to_string js in
+ try Kernel_function.get_definition (Globals.Functions.find_by_name fn)
+ with Not_found | Kernel_function.No_Definition ->
+ Data.failure "Undefined function definition '%s'" fn
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
@@ -219,7 +252,7 @@ struct
| _ -> Data.failure "not a stmt marker"
end
-module Ki =
+module Kinstr =
struct
type t = kinstr
let jtype = Pkg.Joption Marker.jtype
@@ -231,57 +264,24 @@ struct
| js -> Kstmt (Stmt.of_json js)
end
-module Kf =
-struct
- type t = kernel_function
- let jtype = Pkg.Jkey "fct"
- let to_json kf =
- `String (Kernel_function.get_name kf)
- let of_json js =
- let key = Js.to_string js in
- try Globals.Functions.find_by_name key
- with Not_found -> Data.failure "Undefined function '%s'" key
-end
+(* -------------------------------------------------------------------------- *)
+(* --- Record for (Kf * Marker) --- *)
+(* -------------------------------------------------------------------------- *)
-module Fundec =
+module Location =
struct
- type t = fundec
- let jtype = Pkg.Jkey "fundec"
- let to_json fundec =
- `String fundec.svar.vname
+ type t = Function.t * Marker.t
+ let jtype = Data.declare
+ ~package ~name:"location"
+ ~descr:(Md.plain "Location: function and marker")
+ (Jrecord ["fct", Function.jtype; "marker", Marker.jtype])
+ let to_json (kf, loc) = `Assoc [
+ "fct", Function.to_json kf ;
+ "marker", Marker.to_json loc ;
+ ]
let of_json js =
- let key = Js.to_string js in
- try Kernel_function.get_definition (Globals.Functions.find_by_name key)
- with Not_found | Kernel_function.No_Definition ->
- Data.failure "Undefined function definition '%s'" key
-end
-
-module KfMarker = struct
- type record
- let record : record Record.signature = Record.signature ()
-
- let fct = Record.field record ~name:"fct"
- ~descr:(Md.plain "Function") (module Kf)
- let marker = Record.field record ~name:"marker"
- ~descr:(Md.plain "Marker") (module Marker)
-
- let data =
- Record.publish ~package ~name:"location"
- ~descr:(Md.plain "Location: function and marker") record
-
- module R : Record.S with type r = record = (val data)
- type t = kernel_function * Printer_tag.localizable
- let jtype = R.jtype
-
- let to_json (kf, loc) =
- R.default |>
- R.set fct kf |>
- R.set marker loc |>
- R.to_json
-
- let of_json json =
- let r = R.of_json json in
- R.get fct r, R.get marker r
+ Json.field "fct" js |> Function.of_json,
+ Json.field "marker" js |> Marker.of_json
end
(* -------------------------------------------------------------------------- *)
@@ -315,17 +315,15 @@ struct
| PGlobal _ -> if short then "Decl" else "Declaration"
| PType _ -> "Type"
- let kf tag =
+ let is_function tag =
match varinfo_of_localizable tag with
- | Some vi -> Globals.Functions.get vi
- | None -> raise Not_found
+ | Some vi -> Globals.Functions.mem vi
+ | None -> false
- let fundecl = function
- | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Globals.Functions.get vi
- | _ -> raise Not_found
-
- let is_kf tag = try let _ = kf tag in true with Not_found -> false
- let is_fundecl tag = try let _ = fundecl tag in true with Not_found -> false
+ let is_fundecl = function
+ | PGlobal (GFun _ | GFunDecl _) -> true
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Globals.Functions.mem vi
+ | _ -> false
let scope tag =
Option.map Kernel_function.get_name @@ Printer_tag.kf_of_localizable tag
@@ -351,7 +349,7 @@ struct
let () =
States.column
~name:"name"
- ~descr:(Md.plain "Marker short name")
+ ~descr:(Md.plain "Marker short name or identifier when relevant.")
~data:(module Jalpha)
~get:(fun (tag, _) -> Printer_tag.label tag)
model
@@ -371,20 +369,21 @@ struct
~data:(module Jbool)
~get:(fun (tag, _) -> Lval.mem tag)
model
+
let () =
States.column
- ~name:"isFunDecl"
- ~descr:(Md.plain "Whether it is a function declaration or definition")
+ ~name:"isFunction"
+ ~descr:(Md.plain "Whether it is a function symbol")
~data:(module Jbool)
- ~get:(fun (tag, _) -> is_fundecl tag)
+ ~get:(fun (tag, _) -> is_function tag)
model
let () =
States.column
- ~name:"isFun"
- ~descr:(Md.plain "Whether it is a function symbol")
+ ~name:"isFunDecl"
+ ~descr:(Md.plain "Whether it is a function declaration")
~data:(module Jbool)
- ~get:(fun (tag, _) -> is_kf tag)
+ ~get:(fun (tag, _) -> is_fundecl tag)
model
let () =
@@ -407,7 +406,9 @@ struct
~package
~name:"markerAttributes"
~descr:(Md.plain "Marker attributes")
- ~key:snd ~keyType:Jstring
+ ~key:snd
+ ~keyName:"marker"
+ ~keyType:Marker.jtype
~iter:Marker.iter
~add_reload_hook:ast_update_hook
model
@@ -423,7 +424,7 @@ end
let () = Request.register ~package
~kind:`GET ~name:"getMainFunction"
~descr:(Md.plain "Get the current 'main' function.")
- ~input:(module Junit) ~output:(module Joption (Kf))
+ ~input:(module Junit) ~output:(module Joption(Function))
begin fun () ->
try Some (fst (Globals.entry_point ()))
with Globals.No_such_entry_point _ -> None
@@ -432,7 +433,7 @@ let () = Request.register ~package
let () = Request.register ~package
~kind:`GET ~name:"getFunctions"
~descr:(Md.plain "Collect all functions in the AST")
- ~input:(module Junit) ~output:(module Jlist(Kf))
+ ~input:(module Junit) ~output:(module Jlist(Function))
begin fun () ->
let pool = ref [] in
Globals.Functions.iter (fun kf -> pool := kf :: !pool) ;
@@ -442,7 +443,7 @@ let () = Request.register ~package
let () = Request.register ~package
~kind:`GET ~name:"printFunction"
~descr:(Md.plain "Print the AST of a function")
- ~input:(module Kf) ~output:(module Jtext)
+ ~input:(module Function) ~output:(module Jtext)
begin fun kf ->
let libc = Kernel.PrintLibc.get () in
try
@@ -756,7 +757,7 @@ let () =
Request.register
~package ~descr ~kind:`GET ~name:"getMarkerAt"
~input:(module Jtriple (Jstring) (Jint) (Jint))
- ~output:(module Jpair (Joption (Kf)) (Joption (Marker)))
+ ~output:(module Jpair (Joption (Function)) (Joption (Marker)))
get_kf_marker
(* -------------------------------------------------------------------------- *)
@@ -852,7 +853,7 @@ let () =
TermHash.add cache entry m
end
-(* request to parse a new marker from ACSL term *)
+(* request to parse a new marker from C expression or l-value *)
let () =
let module Md = Markdown in
let s = Request.signature ~output:(module Data.Joption(Marker)) () in
@@ -863,8 +864,8 @@ let () =
~descr:(Md.plain "ACSL term to parse")
(module Data.Jstring) in
Request.register_sig ~package s
- ~kind:`GET ~name:"parseTerm"
- ~descr:(Md.plain "Parse an ACSL Term and returns the associated marker")
+ ~kind:`GET ~name:"parseExpr"
+ ~descr:(Md.plain "Parse a C expression and returns the associated marker")
begin fun rq () ->
match Printer_tag.ki_of_localizable @@ get_marker rq with
| Kglobal -> failwith "No statement at selection point"
@@ -876,6 +877,7 @@ let () =
let entry = (stmt, term) in
let cache = TERMCACHE.get () in
try Some (TermHash.find cache entry) with Not_found ->
+ try
let marker =
match Logic_to_c.term_to_exp term with
| { enode = Lval lv } ->
@@ -883,6 +885,8 @@ let () =
| exp ->
Printer_tag.PExp(Some kf, Kstmt stmt, exp)
in TermHash.add cache entry marker ; Some marker
+ with Logic_to_c.No_conversion ->
+ failwith "Not a C-expression"
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 50702ec1922..7ac955f9929 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -26,7 +26,23 @@
open Cil_types
+(** Represented by a Json record with file, dir, basename, line *)
+module Position : Data.S with type t = Filepath.position
+
+(** Json key representing a function name *)
+val jFunction : Package.jtype
+
+(** Represented by the function name as [jFunction]. *)
+module Function : Data.S with type t = kernel_function
+
+(** Represented by the function name as [jFunction]. *)
+module Fundec : Data.S with type t = fundec
+(* -------------------------------------------------------------------------- *)
+(** Ast Markers *)
+(* -------------------------------------------------------------------------- *)
+
+(** Exported as Json string with their unique tag. *)
module Marker :
sig
include Data.S with type t = Printer_tag.localizable
@@ -40,13 +56,26 @@ sig
end
-module Position : Data.S with type t = Filepath.position
-module Kf : Data.S with type t = kernel_function
-module Fundec : Data.S with type t = fundec
-module Ki : Data.S with type t = kinstr
+(* -------------------------------------------------------------------------- *)
+(** Ast Markers of Specific Kinds *)
+(* -------------------------------------------------------------------------- *)
+
+(** Markers that are l-values. *)
+module Lval :
+sig
+ include Data.S with type t = kinstr * lval
+ val mem : Marker.t -> bool
+ val find : Marker.t -> t
+end
+
+(** Markers that are statements. *)
module Stmt : Data.S with type t = stmt
-module Lval : Data.S with type t = kinstr * lval
-module KfMarker : Data.S with type t = kernel_function * Printer_tag.localizable
+
+(** Optional markers interpreted as kinstr. *)
+module Kinstr : Data.S with type t = kinstr
+
+(** Represented as a Json record with function name and marker tag. *)
+module Location : Data.S with type t = Function.t * Marker.t
(* -------------------------------------------------------------------------- *)
(** Ast Printer *)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index e5c6252aa5d..c94df8b12ab 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -160,7 +160,7 @@ let () = States.option model ~name:"marker"
let () = States.option model ~name:"fct"
~descr:(Md.plain "Function containing the message position (if any)")
- ~data:(module Kernel_ast.Kf)
+ ~data:(module Kernel_ast.Function)
~get:getFunction
let iter f = ignore (Messages.fold (fun i evt -> f (evt, i); succ i) 0)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 7d54d4144eb..f07736aa520 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -288,11 +288,11 @@ let () = States.column model ~name:"status"
let () = States.column model ~name:"fct"
~descr:(Md.plain "Function")
- ~data:(module Joption(Kf)) ~get:Property.get_kf
+ ~data:(module Joption(Function)) ~get:Property.get_kf
let () = States.column model ~name:"kinstr"
~descr:(Md.plain "Instruction")
- ~data:(module Ki) ~get:Property.get_kinstr
+ ~data:(module Kinstr) ~get:Property.get_kinstr
let () = States.column model ~name:"source"
~descr:(Md.plain "Position")
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
index b9f3024420a..4bc6362c4e4 100644
--- a/src/plugins/studia/studia_request.ml
+++ b/src/plugins/studia/studia_request.ml
@@ -37,7 +37,7 @@ module Effects = struct
type record
let record: record Record.signature = Record.signature ()
- module Location = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Marker)
+ module Location = Data.Jpair (Kernel_ast.Function) (Kernel_ast.Marker)
let direct = Record.field record ~name:"direct"
~descr:(Markdown.plain "List of statements with direct effect.")
--
GitLab