|
|
@ -92,17 +92,23 @@ let rec get_typ t tenv : Typ.t option =
|
|
|
|
match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None )
|
|
|
|
match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None )
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let may_pp_typ fmt typ =
|
|
|
|
|
|
|
|
if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let rec pp fmt = function
|
|
|
|
let rec pp fmt = function
|
|
|
|
| Base (pvar, _) ->
|
|
|
|
| Base (pvar, typ) ->
|
|
|
|
Var.pp fmt pvar
|
|
|
|
Var.pp fmt pvar ; may_pp_typ fmt typ
|
|
|
|
| FieldOffset (Dereference ae, fld) ->
|
|
|
|
| FieldOffset (Dereference ae, fld) ->
|
|
|
|
F.fprintf fmt "%a->%a" pp ae Typ.Fieldname.pp fld
|
|
|
|
F.fprintf fmt "%a->%a" pp ae Typ.Fieldname.pp fld
|
|
|
|
| FieldOffset (ae, fld) ->
|
|
|
|
| FieldOffset (ae, fld) ->
|
|
|
|
F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld
|
|
|
|
F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld
|
|
|
|
| ArrayOffset (ae, _, []) ->
|
|
|
|
| ArrayOffset (ae, typ, []) ->
|
|
|
|
F.fprintf fmt "%a[_]" pp ae
|
|
|
|
F.fprintf fmt "%a[_]%a" pp ae may_pp_typ typ
|
|
|
|
| ArrayOffset (ae, _, index_aes) ->
|
|
|
|
| ArrayOffset (ae, typ, index_aes) ->
|
|
|
|
F.fprintf fmt "%a[%a]" pp ae (PrettyPrintable.pp_collection ~pp_item:pp) index_aes
|
|
|
|
F.fprintf fmt "%a[%a]%a" pp ae
|
|
|
|
|
|
|
|
(PrettyPrintable.pp_collection ~pp_item:pp)
|
|
|
|
|
|
|
|
index_aes may_pp_typ typ
|
|
|
|
| AddressOf ae ->
|
|
|
|
| AddressOf ae ->
|
|
|
|
F.fprintf fmt "&(%a)" pp ae
|
|
|
|
F.fprintf fmt "&(%a)" pp ae
|
|
|
|
| Dereference ae ->
|
|
|
|
| Dereference ae ->
|
|
|
|