diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 11:13:23 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 11:13:23 +0200 |
| commit | ef16a51223a4b73eed74c40ce9938248ab6b4b8a (patch) | |
| tree | 12a81f7818a01eab08b71b253320c11ebb364447 /cfrontend/Ctyping.v | |
| parent | 5dd1544021c608060d8ee5ba052cc82132fff741 (diff) | |
| download | compcert-kvx-ef16a51223a4b73eed74c40ce9938248ab6b4b8a.tar.gz compcert-kvx-ef16a51223a4b73eed74c40ce9938248ab6b4b8a.zip | |
In AST.calling_conventions, record whether the original C function was "old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
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)) |