diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts index dc1398e2ab95606276eb5ab92a4475f1ffbe3299..eaaf033326b4ba7835ba5f16fc80c302180a1fee 100644 --- a/ivette/api/generated/kernel/ast/index.ts +++ b/ivette/api/generated/kernel/ast/index.ts @@ -31,6 +31,14 @@ 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, @@ -121,6 +129,8 @@ export interface markerInfoData { name: string; /** Marker declaration or description */ descr: string; + /** Marker position */ + position: source; } /** Loose decoder for `markerInfoData` */ @@ -132,6 +142,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> = var: jMarkerVarSafe, name: Json.jFail(Json.jString,'String expected'), descr: Json.jFail(Json.jString,'String expected'), + position: jSourceSafe, }); /** Safe decoder for `markerInfoData` */ @@ -142,12 +153,13 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> = export const byMarkerInfoData: Compare.Order<markerInfoData> = Compare.byFields <{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar, - name: string, descr: string }>({ + name: string, descr: string, position: source }>({ key: Compare.string, kind: byMarkerKind, var: byMarkerVar, name: Compare.alpha, descr: Compare.string, + position: bySource, }); /** Signal for array [`markerInfo`](#markerinfo) */ diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml index 8d8d6f6c87f5a2e8f075865c0889cb7a5f5ea2f5..bd1fa410041bf8bac9a1852b9e87e0eefba3ec6a 100644 --- a/src/kernel_services/ast_printing/printer_tag.ml +++ b/src/kernel_services/ast_printing/printer_tag.ml @@ -76,9 +76,7 @@ let pretty fmt = function | PExp (_, _, expr) -> Printer.pp_exp fmt expr | PTermLval (_, _, _, lv) -> Printer.pp_term_lval fmt lv | PIP prop -> Description.pp_property fmt prop - | PStmt(_,stmt) | PStmtStart (_, stmt) -> - let p = fst @@ Cil_datatype.Stmt.loc stmt in - Format.fprintf fmt "Statement at %a" Filepath.pp_pos p + | PStmt(_,stmt) | PStmtStart (_, stmt) -> Printer.pp_stmt fmt stmt | PGlobal g -> Printer.pp_global fmt (decl_of g) let pp_ki_loc fmt ki = diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 7f51b3cbee164d0476fbec2cbdf6fc936a447b70..a3fe97c94e4ac970d3f3c228715d63eee5af6714 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -194,6 +194,14 @@ struct ~get:(fun (tag, _) -> Rich_text.to_string Printer_tag.pretty tag) model in + let () = + States.column + ~name:"position" + ~descr:(Md.plain "Marker position") + ~data:(module Kernel_main.LogSource) + ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag)) + model + in States.register_array ~package ~name:"markerInfo"