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.

4 files changed, 28 insertions, 23 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index a0e6b259..71328c71 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -437,10 +437,10 @@ let convertAttr a =
       let n = Cutil.alignas_attribute a in
       if n > 0 then Some (N.of_int (log2 n)) else None }
 
-let convertCallconv va attr =
+let convertCallconv va unproto attr =
   let sr =
     Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
-  { cc_vararg = va; cc_structret = sr <> [] }
+  { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] }
 
 (** Types *)
 
@@ -494,7 +494,7 @@ let rec convertTyp env t =
                 | Some tl -> convertParams env tl
                 end,
                 convertTyp env tres,
-                convertCallconv va a)
+                convertCallconv va (targs = None) a)
   | C.TNamed _ ->
       convertTyp env (Cutil.unroll env t)
   | C.TStruct(id, a) ->
@@ -796,7 +796,8 @@ let rec convertExpr env e =
       let targs = convertTypArgs env [] args
       and tres = convertTyp env e.etyp in
       let sg =
-        signature_of_type targs tres {cc_vararg = true; cc_structret = false} in
+        signature_of_type targs tres
+           {cc_vararg = true; cc_unproto = false; cc_structret = false} in
       Ebuiltin(EF_external(intern_string "printf", sg), 
                targs, convertExprList env args, tres)
  
@@ -1031,11 +1032,12 @@ let convertFundef loc env fd =
       a_access = Sections.Access_default;
       a_inline = fd.fd_inline && not fd.fd_vararg;  (* PR#15 *)
       a_loc = loc };
-  (id', Gfun(Internal {fn_return = ret;
-                       fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib;
-                       fn_params = params;
-                       fn_vars = vars;
-                       fn_body = body'}))
+  (id', Gfun(Internal
+          {fn_return = ret;
+           fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib;
+           fn_params = params;
+           fn_vars = vars;
+           fn_body = body'}))
 
 (** External function declaration *)
 
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))
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bde61cc7..d890c820 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -123,7 +123,7 @@ let rec name_cdecl id ty =
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl "" t1);
           add_args false tl in
-      add_args true args;
+      if not cconv.cc_unproto then add_args true args;
       Buffer.add_char b ')';
       name_cdecl (Buffer.contents b) res
   | Tstruct(name, a) ->
diff --git a/common/AST.v b/common/AST.v
index 08a19789..387eb6b2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -100,12 +100,13 @@ These signatures are used in particular to determine appropriate
 calling conventions for the function. *)
 
 Record calling_convention : Type := mkcallconv {
-  cc_vararg: bool;
-  cc_structret: bool
+  cc_vararg: bool;                      (**r variable-arity function *)
+  cc_unproto: bool;                     (**r old-style unprototyped function *)
+  cc_structret: bool                    (**r function returning a struct  *)
 }.
 
 Definition cc_default :=
-  {| cc_vararg := false; cc_structret := false |}.
+  {| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
 
 Record signature : Type := mksignature {
   sig_args: list typ;