123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188(**************************************************************************)(* *)(* This file is part of Frama-C. *)(* *)(* Copyright (C) 2007-2023 *)(* CEA (Commissariat à l'énergie atomique et aux énergies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file licenses/LGPLv2.1). *)(* *)(**************************************************************************)openCil_types(* Mapping from vid to varinfos whose name have been printed in the
annotation window *)moduleResolveVid=State_builder.Hashtbl(Datatype.Int.Hashtbl)(Cil_datatype.Varinfo)(structletname="Design.ResolveVid"letsize=67letdependencies=[Ast.self]end)(* Maps Cil_types.typ to unique IDs (necessary for the type links). *)moduleResolveTypId=State_builder.Hashtbl(Cil_datatype.TypNoUnroll.Hashtbl)(Datatype.Int)(structletname="Design.ResolveTypId"letsize=67letdependencies=[Ast.self]end)(* Maps unique IDs back to Cil_types.typ. *)moduleResolveTyp=State_builder.Hashtbl(Datatype.Int.Hashtbl)(Cil_datatype.TypNoUnroll)(structletname="Design.ResolveTyp"letsize=67letdependencies=[Ast.self]end)(* Maps Cil_types.location to unique IDs. *)moduleResolveLocId=State_builder.Hashtbl(Cil_datatype.Location.Hashtbl)(Datatype.Int)(structletname="Design.ResolveLocId"letsize=67letdependencies=[Ast.self]end)(* Maps unique IDs back to Cil_types.location. *)moduleResolveLoc=State_builder.Hashtbl(Datatype.Int.Hashtbl)(Cil_datatype.Location)(structletname="Design.ResolveLoc"letsize=67letdependencies=[Ast.self]end)(* Returns the ID associated to a linked [typ]
(adding it to the maps if needed).
Only typedefs, composite types and enumerations are linked. *)lettid_of_typtyp=matchtypwith|TNamed_|TComp_|TEnum_->(trySome(ResolveTypId.findtyp)with|Not_found->letnextId=ResolveTypId.length()inResolveTypId.replacetypnextId;ResolveTyp.replacenextIdtyp;SomenextId)|_->None(* Returns the ID associated to a location (adding it to the maps if needed). *)letlid_of_locloc=tryResolveLocId.findlocwith|Not_found->letnextId=ResolveLocId.length()inResolveLocId.replacelocnextId;ResolveLoc.replacenextIdloc;nextId(* Returns the base type for a pointer/array, otherwise [t] itself.
E.g. for [t = int***], returns [int]. *)letrecget_type_specifier(t:typ)=matchtwith|TPtr(bt,_)|TArray(bt,_,_)->get_type_specifierbt|_->tletpp_tcomp_unfoldedfmtcompattrs=(* uses GCompTag pretty-printer to expand the composite type *)letcattrs=Cil.addAttributesattrscomp.cattrinletcomp={compwithcattr=cattrs}inPrinter.pp_globalfmt(GCompTag(comp,Cil_datatype.Location.unknown))letpp_enum_unfoldedfmtenumattrs=(* use GEnumTag pretty-printer to expand the enum *)leteattrs=Cil.addAttributesattrsenum.eattrinletenum={enumwitheattr=eattrs}inPrinter.pp_globalfmt(GEnumTag(enum,Cil_datatype.Location.unknown))(* This function is intended to be used in a class extended by {!LinkPrinter}
below, as otherwise the sub-types won't be clickable. Doing it differently
is difficult, because we want to unroll only one level of types
(hence we cannot say that this function is the method [typ] itself),
and we cannot add new public methods in extensible printers. *)letpp_typ_unfoldedfmt(t:typ)=matchtwith|TNamed(ty,attrs)->begin(* unfolds the typedef, and one step further if it is a TComp/TEnum *)matchty.ttypewith|TComp(comp,cattrs)->pp_tcomp_unfoldedfmtcomp(Cil.addAttributesattrscattrs)|TEnum(enum,eattrs)->pp_enum_unfoldedfmtenum(Cil.addAttributesattrseattrs)|_->Printer.pp_typfmt(Cil.typeAddAttributesattrsty.ttype)end|TComp(comp,attrs)->pp_tcomp_unfoldedfmtcompattrs|TEnum(enum,attrs)->pp_enum_unfoldedfmtenumattrs|_->Printer.pp_typfmttletpp_typfmttyp=matchtid_of_typtypwith|None->Format.fprintffmt"@{%a@}"Printer.pp_typtyp|Sometid->Format.fprintffmt"@{<link:typ%d>%a@}"tidPrinter.pp_typtyp(* Override the default printer to add <link> tags around types and
some l-values *)moduleLinkPrinter(X:Printer.PrinterClass)=structclassprinter=objectinheritX.printerassupermethod!typ?fundeclnameOptfmtt=matchtid_of_typtwith|None->Format.fprintffmt"@{%a@}"(super#typ?fundeclnameOpt)t|Sometid->Format.fprintffmt"@{<link:typ%d>%a@}"tid(super#typ?fundeclnameOpt)tmethod!varinfofmtvi=ResolveVid.replacevi.vidvi;Format.fprintffmt"@{<link:vid%d>%a@}"vi.vidsuper#varinfovimethod!locationfmtloc=letlid=lid_of_loclocinFormat.fprintffmt"@{<link:loc%d>%a@}"lidsuper#locationlocendendexceptionNoMatchletvarinfo_of_links=tryletvid=Scanf.sscanfs"vid%d"(funid->id)inResolveVid.findvidwithScanf.Scan_failure_|Not_found(* should not happen *)->raiseNoMatchlettyp_of_links=trylettid=Scanf.sscanfs"typ%d"(funid->id)inResolveTyp.findtidwithScanf.Scan_failure_|Not_found(* should not happen *)->raiseNoMatchletloc_of_links=trylettid=Scanf.sscanfs"loc%d"(funid->id)inResolveLoc.findtidwithScanf.Scan_failure_|Not_found(* should not happen *)->raiseNoMatch