From 6e67007200ae70f3af839e3e1d88c01f84b6e600 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 6 Dec 2022 13:50:08 +0100
Subject: [PATCH] [server] replace PType with PGlobal
---
ivette/src/frama-c/kernel/api/ast/index.ts | 5 ++-
.../ast_printing/cil_printer.ml | 1 +
.../ast_printing/printer_tag.ml | 43 +++++++++++++------
src/plugins/server/kernel_ast.ml | 12 ++++--
4 files changed, 41 insertions(+), 20 deletions(-)
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 33db76d4d32..765167a4084 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -245,13 +245,13 @@ export const markerInfo: State.Array<string,markerInfoData> = markerInfo_interna
export type marker =
Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
- Json.key<'#property'>;
+ Json.key<'#property'> | Json.key<'#type'>;
/** Decoder for `marker` */
export const jMarker: Json.Decoder<marker> =
Json.jUnion<Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
- Json.key<'#property'>>(
+ Json.key<'#property'> | Json.key<'#type'>>(
Json.jKey<'#stmt'>('#stmt'),
Json.jKey<'#decl'>('#decl'),
Json.jKey<'#lval'>('#lval'),
@@ -259,6 +259,7 @@ export const jMarker: Json.Decoder<marker> =
Json.jKey<'#term'>('#term'),
Json.jKey<'#global'>('#global'),
Json.jKey<'#property'>('#property'),
+ Json.jKey<'#type'>('#type'),
);
/** Natural order for `marker` */
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index afdf8712c8b..a7ab50d3001 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1777,6 +1777,7 @@ class cil_printer () = object (self)
fprintf fmt "%a %a;@\n"
self#compkind comp
self#compname comp
+
| GVar (vi, io, l) ->
self#line_directive ~forcefile:true fmt l;
Format.fprintf fmt "@[<hov 2>";
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 3718f384dd3..b9f386abb97 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -40,8 +40,12 @@ type localizable =
let glabel = function
| GType(tinfo,_) -> tinfo.tname
- | GCompTag(comp, _) | GCompTagDecl(comp, _) -> comp.cname
- | GEnumTag(enum, _) | GEnumTagDecl(enum, _) -> enum.ename
+ | GCompTag(comp, _) | GCompTagDecl(comp, _) ->
+ Printf.sprintf "%s %s"
+ (if comp.cstruct then "struct" else "union")
+ comp.cname
+ | GEnumTag(enum, _) | GEnumTagDecl(enum, _) ->
+ Printf.sprintf "enum %s" enum.ename
| GVarDecl(vi,_) | GVar(vi, _, _)
| GFun( { svar=vi }, _) | GFunDecl(_,vi,_) -> vi.vname
| GPragma((Attr(a,_) | AttrAnnot a),_) -> a
@@ -58,7 +62,7 @@ let label = function
| PTermLval _ -> "(term)"
| PGlobal g -> glabel g
| PIP _ -> "(property)"
- | PType _ -> "(type)"
+ | PType ty -> Pretty_utils.to_string Printer.pp_typ ty
let decl_of = function
| GCompTag(comp,loc) -> GCompTagDecl(comp,loc)
@@ -676,13 +680,14 @@ struct
method! global fmt g =
match g with
- (* these globals are already covered by PVDecl *)
- | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ -> super#global fmt g
- | _ ->
- Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PGlobal g))
- super#global
- g
+ (* these globals are already covered by the underlying parser *)
+ | GVarDecl _ | GVar _ | GFunDecl _ | GFun _
+ | GCompTag _ | GCompTagDecl _
+ | GEnumTag _ | GEnumTagDecl _
+ | GType _ ->
+ super#global fmt g
+ | GAsm _ | GPragma _ | GText _ | GAnnot _ ->
+ Format.fprintf fmt "@{<%s>%a@}" (Tag.create (PGlobal g)) super#global g
method! extended fmt ext =
let loc =
@@ -814,19 +819,29 @@ struct
let tag = Tag.create (PStmtStart(f,s)) in
Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
+ method! ikind fmt c =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PType(TInt(c,[]))))
+ super#ikind c
+
+ method! fkind fmt c =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PType(TFloat(c,[]))))
+ super#fkind c
+
method! compname fmt comp =
- Format.fprintf fmt "@{<%s>%a}"
- (Tag.create (PType (TComp (comp, []))))
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PGlobal(Globals.Types.global Struct comp.cname)))
super#compname comp
method! enuminfo fmt enum =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PType (TEnum (enum, []))))
+ (Tag.create (PGlobal(Globals.Types.global Enum enum.ename)))
super#enuminfo enum
method! typeinfo fmt tinfo =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PType (TNamed (tinfo, []))))
+ (Tag.create (PGlobal(Globals.Types.global Typedef tinfo.tname)))
super#typeinfo tinfo
initializer force_brace <- true
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 170fafd311e..e314f33f7c5 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -730,12 +730,16 @@ let () = Information.register
~label:"Sizeof"
~descr:"Size of a C type"
begin fun fmt loc ->
- match loc with
- | PType typ -> Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
- | _ -> raise Not_found
+ let typ =
+ match loc with
+ | PType typ -> typ
+ | PGlobal (GType(ti,_)) -> ti.ttype
+ | PGlobal (GCompTagDecl(ci,_)) -> TComp(ci,[])
+ | PGlobal (GEnumTagDecl(ei,_)) -> TEnum(ei,[])
+ | _ -> raise Not_found
+ in Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
end
-
(* -------------------------------------------------------------------------- *)
(* --- Marker at a position --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab