Skip to content

Commit

Permalink
Fix non-struct typsig pretty in MemoRoot
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Aug 15, 2023
1 parent 7297241 commit 48884b3
Show file tree
Hide file tree
Showing 2 changed files with 97 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/domains/access.ml
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ struct
match vt with
| `Var v -> CilType.Varinfo.pretty () v
| `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name
| `Type t -> Pretty.dprintf "(%a)" CilType.Typsig.pretty t (* TODO: fix TSBase printing *)
| `Type t -> Pretty.dprintf "(%a)" Cilfacade.pretty_typsig_like_typ t

include Printable.SimplePretty (
struct
Expand All @@ -116,7 +116,7 @@ struct
match vt with
| `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o
| `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o
| `Type t -> Pretty.dprintf "(%a)%a" CilType.Typsig.pretty t Offset.Unit.pretty o (* TODO: fix TSBase printing *)
| `Type t -> Pretty.dprintf "(%a)%a" Cilfacade.pretty_typsig_like_typ t Offset.Unit.pretty o

include Printable.SimplePretty (
struct
Expand Down
95 changes: 95 additions & 0 deletions src/util/cilfacade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -359,6 +359,101 @@ let split_anoncomp_name name =
else
invalid_arg "Cilfacade.split_anoncomp_name"

(** Pretty-print typsig like typ, because
{!d_typsig} prints with CIL constructors. *)
let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
(* Copied & modified from Cil.defaultCilPrinterClass#pType. *)
let open Pretty in
let name = match nameOpt with None -> nil | Some d -> d in
let printAttributes (a: attributes) =
let pa = d_attrlist () a in
match nameOpt with
| None when not !print_CIL_Input ->
(* Cannot print the attributes in this case because gcc does not
like them here, except if we are printing for CIL. *)
if pa = nil then nil else
text "/*" ++ pa ++ text "*/"
| _ -> pa
in
match ts with
| TSBase t -> dn_type () t
| TSComp (cstruct, cname, a) ->
let su = if cstruct then "struct" else "union" in
text (su ^ " " ^ cname ^ " ")
++ d_attrlist () a
++ name
| TSEnum (ename, a) ->
text ("enum " ^ ename ^ " ")
++ d_attrlist () a
++ name
| TSPtr (bt, a) ->
(* Parenthesize the ( * attr name) if a pointer to a function or an
array. *)
let (paren: doc option), (bt': typsig) =
match bt with
| TSFun _ | TSArray _ -> Some (text "("), bt
| _ -> None, bt
in
let name' = text "*" ++ printAttributes a ++ name in
let name'' = (* Put the parenthesis *)
match paren with
Some p -> p ++ name' ++ text ")"
| _ -> name'
in
pretty_typsig_like_typ
(Some name'')
()
bt'

| TSArray (elemt, lo, a) ->
(* ignore the const attribute for arrays *)
let a' = dropAttributes [ "pconst" ] a in
let name' =
if a' == [] then name else
if nameOpt == None then printAttributes a' else
text "(" ++ printAttributes a' ++ name ++ text ")"
in
pretty_typsig_like_typ
(Some (name'
++ text "["
++ (match lo with None -> nil | Some e -> text (Z.to_string e))
++ text "]"))
()
elemt

| TSFun (restyp, args, isvararg, a) ->
let name' =
if a == [] then name else
if nameOpt == None then printAttributes a else
text "(" ++ printAttributes a ++ name ++ text ")"
in
pretty_typsig_like_typ
(Some
(name'
++ text "("
++ (align
++
(if args = Some [] && isvararg then
text "..."
else
(if args = None then nil
else if args = Some [] then text "void"
else
let pArg atype =
(pretty_typsig_like_typ None () atype)
in
(docList ~sep:(chr ',' ++ break) pArg) ()
(match args with None -> [] | Some args -> args))
++ (if isvararg then break ++ text ", ..." else nil))
++ unalign)
++ text ")"))
()
restyp

(** Pretty-print typsig like typ, because
{!d_typsig} prints with CIL constructors. *)
let pretty_typsig_like_typ = pretty_typsig_like_typ None

(** HashSet of line numbers *)
let locs = Hashtbl.create 200

Expand Down

0 comments on commit 48884b3

Please sign in to comment.