summaryrefslogtreecommitdiff
path: root/caml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-17 12:52:16 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-17 12:52:16 +0000
commit623c0ad32146f29707067db2fa9549c6d4515885 (patch)
tree82e05441296ec0319dec6368c33fec40221ed811 /caml
parent2ec5b3fb2ccb0120be641e077089f3da5e53d8a3 (diff)
Type unrolling in struct and union fields
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@105 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r--caml/Cil2Csyntax.ml35
1 files changed, 30 insertions, 5 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index afd5077..1c796ea 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -39,6 +39,32 @@ let stringTable = Hashtbl.create 47
(** ** Functions related to [struct]s and [union]s *)
+(* Unroll recursion in struct or union types:
+ substitute [Tcomp_ptr id] by [Tpointer compty] in [ty]. *)
+
+let unrollType id compty ty =
+ let rec unrType ty =
+ match ty with
+ | Tvoid -> ty
+ | Tint(sz, sg) -> ty
+ | Tfloat sz -> ty
+ | Tpointer ty -> Tpointer (unrType ty)
+ | Tarray(ty, sz) -> Tarray (unrType ty, sz)
+ | Tfunction(args, res) -> Tfunction(unrTypelist args, unrType res)
+ | Tstruct(id', fld) ->
+ if id' = id then ty else Tstruct(id', unrFieldlist fld)
+ | Tunion(id', fld) ->
+ if id' = id then ty else Tunion(id', unrFieldlist fld)
+ | Tcomp_ptr id' ->
+ if id' = id then Tpointer compty else ty
+ and unrTypelist = function
+ | Tnil -> Tnil
+ | Tcons(hd, tl) -> Tcons(unrType hd, unrTypelist tl)
+ and unrFieldlist = function
+ | Fnil -> Fnil
+ | Fcons(id, ty, tl) -> Fcons(id, unrType ty, unrFieldlist tl)
+ in unrType ty
+
(* Return the type of a [struct] field *)
let rec getFieldType f = function
| Fnil -> raise Not_found
@@ -345,18 +371,18 @@ and convertLval lv =
| NoOffset -> e
| Field (f, ofs) ->
begin match t with
- | Tstruct(_, fList) ->
+ | Tstruct(id, fList) ->
begin try
let idf = intern_string f.fname in
- let t' = getFieldType idf fList in
+ let t' = unrollType id t (getFieldType idf fList) in
processOffset (Expr (Efield (e, idf), t')) ofs
with Not_found ->
internal_error "processOffset: no such struct field"
end
- | Tunion(_, fList) ->
+ | Tunion(id, fList) ->
begin try
let idf = intern_string f.fname in
- let t' = getFieldType idf fList in
+ let t' = unrollType id t (getFieldType idf fList) in
processOffset (Expr (Efield (e, idf), t')) ofs
with Not_found ->
internal_error "processOffset: no such union field"
@@ -685,7 +711,6 @@ let convertGFun fdec =
(intern_string v.vname,
Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
-
(** Auxiliary for [convertInit] *)
let rec initDataLen accu = function