diff options
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index d726a525..cde9ad11 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -179,8 +179,13 @@ Proof. decide equality. Defined. Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}. Proof. decide equality. Defined. -Definition callconv_eq: forall (x y: calling_convention), {x=y} + {x<>y}. -Proof. decide equality; apply bool_dec. Defined. +Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention := + if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + OK {| cc_vararg := cc1.(cc_vararg); + cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); + cc_structret := cc1.(cc_structret) |} + else + Error (msg "incompatible calling conventions"). Fixpoint type_combine (ty1 ty2: type) : res type := match ty1, ty2 with @@ -207,14 +212,11 @@ Fixpoint type_combine (ty1 ty2: type) : res type := | Tfunction args1 res1 cc1, Tfunction args2 res2 cc2 => do res <- type_combine res1 res2; do args <- - match args1, args2 with - | Tnil, _ => OK args2 (* tolerance for unprototyped functions *) - | _, Tnil => OK args1 - | _, _ => typelist_combine args1 args2 - end; - if callconv_eq cc1 cc2 - then OK (Tfunction args res cc1) - else Error (msg "incompatible function types") + (if cc1.(cc_unproto) then OK args2 else + if cc2.(cc_unproto) then OK args1 else + typelist_combine args1 args2); + do cc <- callconv_combine cc1 cc2; + OK (Tfunction args res cc) | Tstruct id1 a1, Tstruct id2 a2 => if ident_eq id1 id2 then OK (Tstruct id1 (attr_combine a1 a2)) |