From 15d6749d10c093fd362b13fe3443ab76b2894083 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 29 Nov 2023 14:59:00 +0100
Subject: [PATCH] [kernel] Slightly improves tag location for properties and
global variables.
Uses Ast.def_or_last_decl for the location of global variables.
Uses Property.location for logical properties.
---
.../ast_printing/printer_tag.ml | 19 ++++++-------------
1 file changed, 6 insertions(+), 13 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 586d04cc483..e01f6c3d0f7 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -127,11 +127,7 @@ let definition_of_declaration = function
| SEnum ei -> GEnumTag(ei,Location.unknown)
| SComp ci -> GCompTag(ci,Location.unknown)
| SType ti -> GType(ti,Location.unknown)
- | SGlobal vi ->
- begin
- try GVar(vi,Globals.Vars.find vi,vi.vdecl)
- with Not_found -> GVarDecl(vi,vi.vdecl)
- end
+ | SGlobal vi -> Ast.def_or_last_decl vi
| SFunction kf -> Kernel_function.get_global kf
let pp_signature fmt d = Printer.pp_global fmt @@ signature_of_declaration d
@@ -410,14 +406,11 @@ let loc_of_localizable = function
| PLval (_,Kstmt st,_) | PExp(_,Kstmt st, _)
| PTermLval(_,Kstmt st,_,_) ->
Stmt.loc st
- | PIP ip ->
- (match Property.get_kinstr ip with
- | Kglobal ->
- (match Property.get_kf ip with
- None -> Location.unknown
- | Some kf -> Kernel_function.get_location kf)
- | Kstmt st -> Stmt.loc st)
- | PVDecl (_,_,vi) -> vi.vdecl
+ | PIP ip -> Property.location ip
+ | PVDecl (_,_,vi) ->
+ if vi.vglob
+ then Global.loc (Ast.def_or_last_decl vi)
+ else vi.vdecl
| PGlobal g -> Global.loc g
| (PLval _ | PTermLval _ | PExp _) as localize ->
(match kf_of_localizable localize with
--
GitLab