diff --git a/ivette/src/frama-c/api/generated/kernel/ast/index.ts b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
index e6053cb2610892878eaa809c997d6c6064afa04d..89d14dc6e8599a29643125ac8fdd0c722e8ec1e1 100644
--- a/ivette/src/frama-c/api/generated/kernel/ast/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
@@ -53,14 +53,6 @@ import { jTextSafe } from 'frama-c/api/kernel/data';
import { tag } from 'frama-c/api/kernel/data';
//@ts-ignore
import { text } from 'frama-c/api/kernel/data';
-//@ts-ignore
-import { bySource } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { jSource } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { jSourceSafe } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { source } from 'frama-c/api/kernel/services';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
@@ -77,6 +69,33 @@ export const changed: Server.Signal = {
name: 'kernel.ast.changed',
};
+/** Source file positions. */
+export type source =
+ { dir: string, base: string, file: string, line: number };
+
+/** Loose decoder for `source` */
+export const jSource: Json.Loose<source> =
+ Json.jObject({
+ dir: Json.jFail(Json.jString,'String expected'),
+ base: Json.jFail(Json.jString,'String expected'),
+ file: Json.jFail(Json.jString,'String expected'),
+ line: Json.jFail(Json.jNumber,'Number expected'),
+ });
+
+/** Safe decoder for `source` */
+export const jSourceSafe: Json.Safe<source> =
+ Json.jFail(jSource,'Source expected');
+
+/** Natural order for `source` */
+export const bySource: Compare.Order<source> =
+ Compare.byFields
+ <{ dir: string, base: string, file: string, line: number }>({
+ dir: Compare.string,
+ base: Compare.string,
+ file: Compare.string,
+ line: Compare.number,
+ });
+
/** Marker kind */
export enum markerKind {
/** Expression */
diff --git a/ivette/src/frama-c/api/generated/kernel/properties/index.ts b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
index 6c5a7309f5003aeccd2b0cba0b173e9a7af87853..1379aced2c69b7e54f858187595db95f925a2968 100644
--- a/ivette/src/frama-c/api/generated/kernel/properties/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
@@ -38,21 +38,21 @@ import * as Server from 'frama-c/server';
import * as State from 'frama-c/states';
//@ts-ignore
-import { byTag } from 'frama-c/api/kernel/data';
+import { bySource } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { jTag } from 'frama-c/api/kernel/data';
+import { jSource } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { jTagSafe } from 'frama-c/api/kernel/data';
+import { jSourceSafe } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { tag } from 'frama-c/api/kernel/data';
+import { source } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { bySource } from 'frama-c/api/kernel/services';
+import { byTag } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { jSource } from 'frama-c/api/kernel/services';
+import { jTag } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { jSourceSafe } from 'frama-c/api/kernel/services';
+import { jTagSafe } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { source } from 'frama-c/api/kernel/services';
+import { tag } from 'frama-c/api/kernel/data';
/** Property Kinds */
export enum propKind {
diff --git a/ivette/src/frama-c/api/generated/kernel/services/index.ts b/ivette/src/frama-c/api/generated/kernel/services/index.ts
index bda3ec1dbb7fcaa329c3d665a68fc1e18bb95556..d271d8fd722e44a281c5214cc56d93f47746cfc9 100644
--- a/ivette/src/frama-c/api/generated/kernel/services/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/services/index.ts
@@ -37,6 +37,22 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byMarker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { bySource } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarkerSafe } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jSource } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jSourceSafe } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { marker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { source } from 'frama-c/api/kernel/ast';
//@ts-ignore
import { byTag } from 'frama-c/api/kernel/data';
//@ts-ignore
@@ -87,33 +103,6 @@ const save_internal: Server.SetRequest<string,string | undefined> = {
/** Save the current session. Returns an error, if not successfull. */
export const save: Server.SetRequest<string,string | undefined>= save_internal;
-/** Source file positions. */
-export type source =
- { dir: string, base: string, file: string, line: number };
-
-/** Loose decoder for `source` */
-export const jSource: Json.Loose<source> =
- Json.jObject({
- dir: Json.jFail(Json.jString,'String expected'),
- base: Json.jFail(Json.jString,'String expected'),
- file: Json.jFail(Json.jString,'String expected'),
- line: Json.jFail(Json.jNumber,'Number expected'),
- });
-
-/** Safe decoder for `source` */
-export const jSourceSafe: Json.Safe<source> =
- Json.jFail(jSource,'Source expected');
-
-/** Natural order for `source` */
-export const bySource: Compare.Order<source> =
- Compare.byFields
- <{ dir: string, base: string, file: string, line: number }>({
- dir: Compare.string,
- base: Compare.string,
- file: Compare.string,
- line: Compare.number,
- });
-
/** Log messages categories. */
export enum logkind {
/** User Error */
@@ -164,6 +153,10 @@ export interface messageData {
category?: string;
/** Source file position */
source?: source;
+ /** Marker at the message position (if any) */
+ marker?: marker;
+ /** Function containing the message position (if any) */
+ fct?: Json.key<'#fct'>;
}
/** Loose decoder for `messageData` */
@@ -175,6 +168,8 @@ export const jMessageData: Json.Loose<messageData> =
message: Json.jFail(Json.jString,'String expected'),
category: Json.jString,
source: jSource,
+ marker: jMarker,
+ fct: Json.jKey<'#fct'>('#fct'),
});
/** Safe decoder for `messageData` */
@@ -185,13 +180,16 @@ export const jMessageDataSafe: Json.Safe<messageData> =
export const byMessageData: Compare.Order<messageData> =
Compare.byFields
<{ key: Json.key<'#message'>, kind: logkind, plugin: string,
- message: string, category?: string, source?: source }>({
+ message: string, category?: string, source?: source, marker?: marker,
+ fct?: Json.key<'#fct'> }>({
key: Compare.string,
kind: byLogkind,
plugin: Compare.alpha,
message: Compare.string,
category: Compare.defined(Compare.string),
source: Compare.defined(bySource),
+ marker: Compare.defined(byMarker),
+ fct: Compare.defined(Compare.string),
});
/** Signal for array [`message`](#message) */
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 57f65e5d2f6ab5190a84b31ed932be0d5aade5c4..ca92fa637777ba381e9b2dd8c94b185ece5934a9 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -42,7 +42,7 @@ import { Scroll, Folder } from 'dome/layout/boxes';
import { RSplit } from 'dome/layout/splitters';
-import { source as SourceLoc } from 'frama-c/api/kernel/services';
+import * as Ast from 'frama-c/api/kernel/ast';
import { statusData } from 'frama-c/api/kernel/properties';
import * as Properties from 'frama-c/api/kernel/properties';
import * as Eva from 'frama-c/api/plugins/eva/general';
@@ -245,13 +245,13 @@ const renderNames: Renderer<string[]> =
return (label ? <Label label={label} /> : null);
};
-const renderDir: Renderer<SourceLoc> =
- (loc: SourceLoc) => (
+const renderDir: Renderer<Ast.source> =
+ (loc: Ast.source) => (
<Code className="code-column" label={loc.dir} title={loc.file} />
);
-const renderFile: Renderer<SourceLoc> =
- (loc: SourceLoc) => (
+const renderFile: Renderer<Ast.source> =
+ (loc: Ast.source) => (
<Code className="code-column" label={loc.base} title={loc.file} />
);
@@ -286,7 +286,7 @@ function ColumnTag<Row>(props: ColumnProps<Row, States.Tag>) {
// -------------------------------------------------------------------------
const bySource =
- Compare.byFields<SourceLoc>({ file: Compare.alpha, line: Compare.number });
+ Compare.byFields<Ast.source>({ file: Compare.alpha, line: Compare.number });
const byStatus =
Compare.byRank(
@@ -327,8 +327,8 @@ const byProperty: Compare.ByFields<Property> = {
taint: byTaint,
};
-const byDir = Compare.byFields<SourceLoc>({ dir: Compare.alpha });
-const byFile = Compare.byFields<SourceLoc>({ base: Compare.alpha });
+const byDir = Compare.byFields<Ast.source>({ dir: Compare.alpha });
+const byFile = Compare.byFields<Ast.source>({ base: Compare.alpha });
const byColumn: Arrays.ByColumns<Property> = {
dir: Compare.byFields<Property>({ source: byDir }),
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index e38461a97fa668b18180a6cc3cef2af45fb0bbe6..b635b6facafb4e03e68f036e3b61d139dbe154bc 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -33,8 +33,7 @@ import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { TitleBar } from 'ivette';
import * as Preferences from 'ivette/prefs';
-import { functions, markerInfo } from 'frama-c/api/kernel/ast';
-import { source } from 'frama-c/api/kernel/services';
+import { functions, markerInfo, source } from 'frama-c/api/kernel/ast';
import 'codemirror/addon/selection/active-line';
import 'codemirror/addon/dialog/dialog.css';
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 1c00c79b8609999042fe6023274499198ebf22bb..0736b25b9d0e2ff17b1d17b90d33a96e8a491810 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -43,9 +43,9 @@ PLUGIN_CMO:= \
data main request states \
server_doc \
server_batch \
+ kernel_ast \
kernel_main \
kernel_project \
- kernel_ast \
kernel_properties
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index c59c6950196bf9e022025e75741a04ab02a877a7..01389a481eb1e168ddf288c8ff6f166e9324e8c3 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -46,6 +46,52 @@ let ast_update_hook f =
let () = ast_update_hook (fun _ -> Request.emit changed_signal)
+(* -------------------------------------------------------------------------- *)
+(* --- File Positions --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Position =
+struct
+ type t = Filepath.position
+
+ let jtype = Data.declare ~package ~name:"source"
+ ~descr:(Md.plain "Source file positions.")
+ (Jrecord [
+ "dir", Jstring;
+ "base", Jstring;
+ "file", Jstring;
+ "line", Jnumber;
+ ])
+
+ let to_json p =
+ let path = Filepath.(Normalized.to_pretty_string p.pos_path) in
+ let file =
+ if Server_parameters.has_relative_filepath ()
+ then path
+ else (p.Filepath.pos_path :> string)
+ in
+ `Assoc [
+ "dir" , `String (Filename.dirname path) ;
+ "base" , `String (Filename.basename path) ;
+ "file" , `String file ;
+ "line" , `Int p.Filepath.pos_lnum ;
+ ]
+
+ let of_json js =
+ let fail () = failure_from_type_error "Invalid source format" js in
+ match js with
+ | `Assoc assoc ->
+ begin
+ match List.assoc "file" assoc, List.assoc "line" assoc with
+ | `String path, `Int line ->
+ Log.source ~file:(Filepath.Normalized.of_string path) ~line
+ | _, _ -> fail ()
+ | exception Not_found -> fail ()
+ end
+ | _ -> fail ()
+
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
@@ -207,7 +253,7 @@ struct
States.column
~name:"sloc"
~descr:(Md.plain "Source location")
- ~data:(module Kernel_main.LogSource)
+ ~data:(module Position)
~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
model
in
@@ -470,7 +516,7 @@ struct
States.column model
~name:"sloc"
~descr:(Md.plain "Source location")
- ~data:(module Kernel_main.LogSource)
+ ~data:(module Position)
~get:(fun kf -> fst (Kernel_function.get_location kf));
States.register_array model
~package ~key
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index aa917218f410d85d2ade7922da578687cffe8355..d85697dec6786bf566dabe44780959aa27ab7572 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -27,6 +27,8 @@
open Package
open Cil_types
+module Position : Data.S with type t = Filepath.position
+
module Kf : Data.S with type t = kernel_function
module Ki : Data.S with type t = kinstr
module Stmt : Data.S with type t = stmt
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 1c0e569403aa949984e4fe7b89dc10a34334d4a1..dd00d78a8f55782fb857f39cfab1eb2129cb0204 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -84,51 +84,6 @@ let () =
try Project.save_all (Filepath.Normalized.of_string file); None
with Project.IOError err -> Some err)
-(* -------------------------------------------------------------------------- *)
-(* --- File Positions --- *)
-(* -------------------------------------------------------------------------- *)
-
-module LogSource =
-struct
- type t = Filepath.position
-
- let jtype = Data.declare ~package ~name:"source"
- ~descr:(Md.plain "Source file positions.")
- (Jrecord [
- "dir", Jstring;
- "base", Jstring;
- "file", Jstring;
- "line", Jnumber;
- ])
-
- let to_json p =
- let path = Filepath.(Normalized.to_pretty_string p.pos_path) in
- let file =
- if Server_parameters.has_relative_filepath ()
- then path
- else (p.Filepath.pos_path :> string)
- in
- `Assoc [
- "dir" , `String (Filename.dirname path) ;
- "base" , `String (Filename.basename path) ;
- "file" , `String file ;
- "line" , `Int p.Filepath.pos_lnum ;
- ]
-
- let of_json js =
- let fail () = failure_from_type_error "Invalid source format" js in
- match js with
- | `Assoc assoc ->
- begin
- match List.assoc "file" assoc, List.assoc "line" assoc with
- | `String path, `Int line ->
- Log.source ~file:(Filepath.Normalized.of_string path) ~line
- | _, _ -> fail ()
- | exception Not_found -> fail ()
- end
- | _ -> fail ()
-
-end
(* -------------------------------------------------------------------------- *)
(* --- Log Lind --- *)
@@ -194,9 +149,25 @@ let () = States.option model ~name:"category"
let () = States.option model ~name:"source"
~descr:(Md.plain "Source file position")
- ~data:(module LogSource)
+ ~data:(module Kernel_ast.Position)
~get:(fun (evt, _) -> evt.Log.evt_source)
+let getMarker (evt, _id) =
+ Option.bind evt.Log.evt_source Printer_tag.loc_to_localizable
+
+let getFunction t =
+ Option.bind (getMarker t) Printer_tag.kf_of_localizable
+
+let () = States.option model ~name:"marker"
+ ~descr:(Md.plain "Marker at the message position (if any)")
+ ~data:(module Kernel_ast.Marker)
+ ~get:getMarker
+
+let () = States.option model ~name:"fct"
+ ~descr:(Md.plain "Function containing the message position (if any)")
+ ~data:(module Kernel_ast.Kf)
+ ~get:getFunction
+
let iter f = ignore (Messages.fold (fun i evt -> f (evt, i); succ i) 0)
let _array =
@@ -229,7 +200,7 @@ struct
let category = Record.option jlog ~name:"category"
~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring)
let source = Record.option jlog ~name:"source"
- ~descr:(Md.plain "Source file position") (module LogSource)
+ ~descr:(Md.plain "Source file position") (module Kernel_ast.Position)
let data = Record.publish ~package ~name:"log"
~descr:(Md.plain "Message event record.") jlog
diff --git a/src/plugins/server/kernel_main.mli b/src/plugins/server/kernel_main.mli
index ead76ffab68c5141d8c8c01a9db4bceb9d09a883..b8dd233dda0114f5408609e620b4c97c80429cc5 100644
--- a/src/plugins/server/kernel_main.mli
+++ b/src/plugins/server/kernel_main.mli
@@ -24,7 +24,6 @@
(** Kernel Services *)
(* -------------------------------------------------------------------------- *)
-module LogSource : Data.S with type t = Filepath.position
module LogEvent : Data.S with type t = Log.event
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 534bee463c92d8665d56f5b438d6ca7a5851f08f..4e91e13653b2d5171d6fa710f32f87523dccea77 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -24,7 +24,6 @@ module Md = Markdown
module Pkg = Package
open Data
-open Kernel_main
open Kernel_ast
let package = Pkg.package ~title:"Property Services" ~name:"properties" ()
@@ -297,7 +296,7 @@ let () = States.column model ~name:"kinstr"
let () = States.column model ~name:"source"
~descr:(Md.plain "Position")
- ~data:(module LogSource)
+ ~data:(module Kernel_ast.Position)
~get:(fun ip -> Property.location ip |> fst)
let () = States.column model ~name:"alarm"