Simpler, more robust emulation of calls to variadic functions:

- C function types and Cminor signatures annotated by calling conventions.
  esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
  more arguments than listed in the function prototype.  This is
  still undefined behavior according to the formal semantics,
  but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

20 files changed, 230 insertions, 235 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f12efa3..4cac92c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -143,39 +143,6 @@ let globals_for_strings globs =
     (fun s id l -> global_for_string s id :: l)
     stringTable globs
 
-(** ** Declaration of special external functions *)
-
-let special_externals_table : (string, fundef) Hashtbl.t = Hashtbl.create 47
-
-let register_special_external name ef targs tres =
-  if not (Hashtbl.mem special_externals_table name) then
-    Hashtbl.add special_externals_table name (External(ef, targs, tres))
-
-let declare_special_externals k =
-  Hashtbl.fold
-    (fun name fd k -> (intern_string name, Gfun fd) :: k)
-    special_externals_table k
-
-(** ** Handling of stubs for variadic functions *)
-
-let register_stub_function name tres targs =
-  let rec letters_of_type = function
-    | Tnil -> []
-    | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl
-    | Tcons(Tlong _, tl) -> "l" :: letters_of_type tl
-    | Tcons(_, tl) -> "i" :: letters_of_type tl in
-  let rec types_of_types = function
-    | Tnil -> Tnil
-    | Tcons(Tfloat _, tl) -> Tcons(Tfloat(F64, noattr), types_of_types tl)
-    | Tcons(Tlong _, tl) -> Tcons(Tlong(Signed, noattr), types_of_types tl)
-    | Tcons(_, tl) -> Tcons(Tpointer(Tvoid, noattr), types_of_types tl) in
-  let stub_name =
-    name ^ "$" ^ String.concat "" (letters_of_type targs) in
-  let targs = types_of_types targs in
-  let ef = EF_external(intern_string stub_name, signature_of_type targs tres) in
-  register_special_external stub_name ef targs tres;
-  (stub_name, Tfunction (targs, tres))
-
 (** ** Handling of inlined memcpy functions *)
 
 let make_builtin_memcpy args =
@@ -230,11 +197,16 @@ let mergeTypAttr ty a2 =
   | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2)
   | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2)
   | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2)
-  | Tfunction(targs, tres) -> ty
+  | Tfunction(targs, tres, cc) -> ty
   | Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2)
   | Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2)
   | Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2)
 
+let convertCallconv va attr =
+  let sr =
+    Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in
+  { cc_vararg = va; cc_structret = sr <> [] }
+
 (** Types *)
 
 let convertIkind = function
@@ -293,14 +265,15 @@ let convertTyp env t =
     | C.TArray(ty, Some sz, a) ->
         Tarray(convertTyp seen ty, convertInt sz, convertAttr a)
     | C.TFun(tres, targs, va, a) ->
-        if va then unsupported "variadic function type";
+        (* if va then unsupported "variadic function type"; *)
         if Cutil.is_composite_type env tres then
           unsupported "return type is a struct or union";
         Tfunction(begin match targs with
                   | None -> (*warning "un-prototyped function type";*) Tnil
                   | Some tl -> convertParams seen tl
                   end,
-                  convertTyp seen tres)
+                  convertTyp seen tres,
+                  convertCallconv va a)
     | C.TNamed _ ->
         assert false
     | C.TStruct(id, a) ->
@@ -347,9 +320,20 @@ let convertTyp env t =
 
   in convertTyp [] t
 
+(*
 let rec convertTypList env = function
   | [] -> Tnil
   | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
+*)
+
+let rec convertTypArgs env tl el =
+  match tl, el with
+  | _, [] -> Tnil
+  | [], e1 :: el ->
+      Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp),
+            convertTypArgs env [] el)
+  | (id, t1) :: tl, e1 :: el ->
+      Tcons(convertTyp env t1, convertTypArgs env tl el)
 
 let cacheCompositeDef env su id attr flds =
   let ty =
@@ -358,12 +342,6 @@ let cacheCompositeDef env su id attr flds =
     | C.Union  -> C.TUnion(id, attr) in
   Hashtbl.add compositeCache id (convertTyp env ty)
 
-let rec projFunType env ty =
-  match Cutil.unroll env ty with
-  | TFun(res, args, vararg, attr) -> Some(res, args, vararg)
-  | TPtr(ty', attr) -> projFunType env ty'
-  | _ -> None
-
 let string_of_type ty =
   let b = Buffer.create 20 in
   let fb = Format.formatter_of_buffer b in
@@ -544,10 +522,7 @@ let rec convertExpr env e =
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
-          let targs1 =
-            convertTypList env
-              (List.map (fun e -> Cutil.default_argument_conversion env e.etyp)
-                        args1) in
+          let targs1 = convertTypArgs env [] args1 in
           Ebuiltin(
             EF_annot(intern_string txt,
                      List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)),
@@ -575,36 +550,19 @@ let rec convertExpr env e =
   | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) ->
       Eunop(Oabsfloat, convertExpr env arg, ty)
 
+  | C.ECall({edesc = C.EVar {name = "printf"}}, args)
+    when !Clflags.option_interp ->
+      let targs =
+        convertTypArgs env [] args in
+      let sg =
+        signature_of_type targs ty {cc_vararg = true; cc_structret = false} in
+      Ebuiltin(EF_external(intern_string "printf", sg), 
+               targs, convertExprList env args, ty)
+ 
   | C.ECall(fn, args) ->
       if not (supported_return_type env e.etyp) then
         unsupported ("function returning a result of type " ^ string_of_type e.etyp);
-      match projFunType env fn.etyp with
-      | None ->
-          error "wrong type for function part of a call"; ezero
-      | Some(tres, targs, false) ->
-          (* Non-variadic function *)
-          if targs = None then
-            unsupported "call to non-prototyped function";
-          Ecall(convertExpr env fn, convertExprList env args, ty)
-      | Some(tres, targs, true) ->
-          (* Variadic function: generate a call to a stub function with
-             the appropriate number and types of arguments.  Works only if
-             the function expression e is a global variable. *)
-          let fun_name =
-            match fn with
-            | {edesc = C.EVar id} when !Clflags.option_fvararg_calls ->
-                (*warning "emulating call to variadic function"; *)
-                id.name
-            | _ ->
-                unsupported "call to variadic function";
-                "<error>" in
-          let targs = convertTypList env (List.map (fun e -> e.etyp) args) in
-          let tres = convertTyp env tres in
-          let (stub_fun_name, stub_fun_typ) =
-            register_stub_function fun_name tres targs in
-          Ecall(Evalof(Evar(intern_string stub_fun_name, stub_fun_typ),
-                       stub_fun_typ),
-                convertExprList env args, ty)
+      Ecall(convertExpr env fn, convertExprList env args, ty)
 
 and convertLvalue env e =
   let ty = convertTyp env e.etyp in
@@ -787,25 +745,28 @@ let convertFundef loc env fd =
       a_access = Sections.Access_default;
       a_inline = fd.fd_inline;
       a_loc = loc };
-  (id', Gfun(Internal {fn_return = ret; fn_params = params;
-                       fn_vars = vars; fn_body = body'}))
+  (id', Gfun(Internal {fn_return = ret;
+                       fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib;
+                       fn_params = params;
+                       fn_vars = vars;
+                       fn_body = body'}))
 
 (** External function declaration *)
 
 let convertFundecl env (sto, id, ty, optinit) =
-  let (args, res) =
+  let (args, res, cconv) =
     match convertTyp env ty with
-    | Tfunction(args, res) -> (args, res)
+    | Tfunction(args, res, cconv) -> (args, res, cconv)
     | _ -> assert false in
   let id' = intern_string id.name in
-  let sg = signature_of_type args res in
+  let sg = signature_of_type args res cconv in
   let ef =
     if id.name = "malloc" then EF_malloc else
     if id.name = "free" then EF_free else
     if List.mem_assoc id.name builtins.functions
     then EF_builtin(id', sg)
     else EF_external(id', sg) in
-  (id', Gfun(External(ef, args, res)))
+  (id', Gfun(External(ef, args, res, cconv)))
 
 (** Initializers *)
 
@@ -894,16 +855,13 @@ let rec convertGlobdecls env res gl =
       match g.gdesc with
       | C.Gdecl((sto, id, ty, optinit) as d) ->
           (* Prototyped functions become external declarations.
-             Variadic functions are skipped.
              Other types become variable declarations. *)
           begin match Cutil.unroll env ty with
-          | TFun(_, Some _, false, _) ->
+          | TFun(_, Some _, _, _) ->
               convertGlobdecls env (convertFundecl env d :: res) gl'
-          | TFun(_, None, false, _) ->
+          | TFun(_, None, _, _) ->
               unsupported ("'" ^ id.name ^ "' is declared without a function prototype");
               convertGlobdecls env res gl'
-          | TFun(_, _, true, _) ->
-              convertGlobdecls env res gl'
           | _ ->
               convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl'
           end
@@ -1002,15 +960,13 @@ let convertProgram p =
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear compositeCache;
-  Hashtbl.clear special_externals_table;
   let p = Builtins.declarations() @ p in
   try
     let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in
-    let gl2 = declare_special_externals gl1 in
-    let gl3 = globals_for_strings gl2 in
+    let gl2 = globals_for_strings gl1 in
     if !numErrors > 0
     then None
-    else Some { AST.prog_defs = gl3;
+    else Some { AST.prog_defs = gl2;
                 AST.prog_main = intern_string "main" }
   with Env.Error msg ->
     error (Env.error_message msg); None
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 79dd26f..9593afd 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -887,10 +887,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1, is_val_list rargs with
       | Some(vf, tyf), Some vtl =>
           match classify_fun tyf with
-          | fun_case_f tyargs tyres =>
+          | fun_case_f tyargs tyres cconv =>
               do fd <- Genv.find_funct ge vf;
               do vargs <- sem_cast_arguments vtl tyargs;
-              check type_eq (type_of_fundef fd) (Tfunction tyargs tyres);
+              check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
               topred (Callred fd vargs ty m)
           | _ => stuck
           end
@@ -1020,14 +1020,14 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists v, sem_cast v1 ty1 ty = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
-      exists tyargs, exists tyres, exists fd, exists vl,
-         classify_fun tyf = fun_case_f tyargs tyres
+      exists tyargs tyres cconv fd vl,
+         classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
       /\ cast_arguments rargs tyargs vl
-      /\ type_of_fundef fd = Tfunction tyargs tyres
+      /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
-      exists vargs, exists t, exists vres, exists m', exists w',
+      exists vargs t vres m' w',
          cast_arguments rargs tyargs vargs
       /\ external_call ef ge vargs m t vres m'
       /\ possible_trace w t w'
@@ -1069,7 +1069,7 @@ Lemma callred_invert:
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
-  intros. exists tyargs; exists tyres; exists fd; exists args; auto.
+  intros. exists tyargs, tyres, cconv, fd, args; auto.
 Qed.
 
 Scheme context_ind2 := Minimality for context Sort Prop
@@ -1513,10 +1513,10 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (is_val_list rargs) as [vtl | ] eqn:?. 
   rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
-  destruct (classify_fun tyf) as [tyargs tyres|] eqn:?...
+  destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
   destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
   destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
-  destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))...
+  destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
   apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. 
   eapply sem_cast_arguments_sound; eauto.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
@@ -2049,7 +2049,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
       let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
       do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs;
       ret (State f f.(fn_body) k e m2)
-  | Callstate (External ef _ _) vargs k m =>
+  | Callstate (External ef _ _ _) vargs k m =>
       match do_external ef w vargs m with
       | None => nil
       | Some(w',t,v,m') => (t, Returnstate v k m') :: nil
@@ -2215,7 +2215,7 @@ Definition do_initial_state (p: program): option (genv * state) :=
   do m0 <- Genv.init_mem p;
   do b <- Genv.find_symbol ge p.(prog_main);
   do f <- Genv.find_funct_ptr ge b;
-  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s));
+  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default));
   Some (ge, Callstate f nil Kstop m0).
 
 Definition at_final_state (S: state): option int :=
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 137decc..f402ac2 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -132,6 +132,7 @@ Definition Sfor (s1: statement) (e2: expr) (s3: statement) (s4: statement) :=
 
 Record function : Type := mkfunction {
   fn_return: type;
+  fn_callconv: calling_convention;
   fn_params: list (ident * type);
   fn_vars: list (ident * type);
   fn_temps: list (ident * type);
@@ -146,17 +147,17 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 
 Inductive fundef : Type :=
   | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> fundef.
+  | External: external_function -> typelist -> type -> calling_convention -> fundef.
 
 (** The type of a function definition. *)
 
 Definition type_of_function (f: function) : type :=
-  Tfunction (type_of_params (fn_params f)) (fn_return f).
+  Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
 
 Definition type_of_fundef (f: fundef) : type :=
   match f with
   | Internal fd => type_of_function fd
-  | External id args res => Tfunction args res
+  | External id args res cc => Tfunction args res cc
   end.
 
 (** ** Programs *)
@@ -556,12 +557,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sset id a) k e le m)
         E0 (State f Sskip k e (PTree.set id v le) m)
 
-  | step_call:   forall f optid a al k e le m tyargs tyres vf vargs fd,
-      classify_fun (typeof a) = fun_case_f tyargs tyres ->
+  | step_call:   forall f optid a al k e le m tyargs tyres cconv vf vargs fd,
+      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = Tfunction tyargs tyres ->
+      type_of_fundef fd = Tfunction tyargs tyres cconv ->
       step (State f (Scall optid a al) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
@@ -649,9 +650,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k e le m1)
 
-  | step_external_function: forall ef targs tres vargs k m vres t m',
+  | step_external_function: forall ef targs tres cconv vargs k m vres t m',
       external_call ef ge vargs m t vres m' ->
-      step (Callstate (External ef targs tres) vargs k m)
+      step (Callstate (External ef targs tres cconv) vargs k m)
          t (Returnstate vres k m')
 
   | step_returnstate: forall v optid f e le k m,
@@ -671,7 +672,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 4d10c62..f7a0e18 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -89,12 +89,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       eval_expr ge e le m a v ->
       exec_stmt e le m (Sset id a)
                E0 (PTree.set id v le) m Out_normal 
-  | exec_Scall:   forall e le m optid a al tyargs tyres vf vargs f t m' vres,
-      classify_fun (typeof a) = fun_case_f tyargs tyres ->
+  | exec_Scall:   forall e le m optid a al tyargs tyres cconv vf vargs f t m' vres,
+      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
       eval_expr ge e le m a vf ->
       eval_exprlist ge e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = Tfunction tyargs tyres ->
+      type_of_fundef f = Tfunction tyargs tyres cconv ->
       eval_funcall m f vargs t m' vres ->
       exec_stmt e le m (Scall optid a al)
                 t (set_opttemp optid vres le) m' Out_normal
@@ -170,9 +170,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       outcome_result_value out f.(fn_return) vres ->
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
-  | eval_funcall_external: forall m ef targs tres vargs t vres m',
+  | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
       external_call ef ge vargs m t vres m' ->
-      eval_funcall m (External ef targs tres) vargs t m' vres.
+      eval_funcall m (External ef targs tres cconv) vargs t m' vres.
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
   with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
@@ -186,12 +186,12 @@ Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2.
   trace of observable events performed during the execution. *)
 
 CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
-  | execinf_Scall:   forall e le m optid a al vf tyargs tyres vargs f t,
-      classify_fun (typeof a) = fun_case_f tyargs tyres ->
+  | execinf_Scall:   forall e le m optid a al vf tyargs tyres cconv vargs f t,
+      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
       eval_expr ge e le m a vf ->
       eval_exprlist ge e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = Tfunction tyargs tyres ->
+      type_of_fundef f = Tfunction tyargs tyres cconv ->
       evalinf_funcall m f vargs t ->
       execinf_stmt e le m (Scall optid a al) t
   | execinf_Sseq_1:   forall e le m s1 s2 t,
@@ -246,7 +246,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
@@ -256,7 +256,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.
 
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 31643a9..fec540b 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -92,14 +92,14 @@ Inductive classify_cast_cases : Type :=
 
 Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   match tto, tfrom with
-  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
   | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool
-  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool
+  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool
   | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
   | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2
   | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2
   | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2
-  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral
   | Tlong _ _, Tlong _ _ => cast_case_l2l
   | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
   | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
@@ -107,7 +107,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2
   | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2
   | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
-  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_i2l si2
+  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2
   | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
   | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
   | Tvoid, _ => cast_case_void
@@ -326,7 +326,7 @@ Proof.
   assert (A: classify_bool t =
     match t with
     | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p
+    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p
     | Tfloat _ _ => bool_case_f
     | Tlong _ _ => bool_case_l
     | _ => bool_default
@@ -833,13 +833,13 @@ Definition sem_cmp (c:comparison)
 (** ** Function applications *)
 
 Inductive classify_fun_cases : Type:=
-  | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *)
+  | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *)
   | fun_default.
 
 Definition classify_fun (ty: type) :=
   match ty with 
-  | Tfunction args res => fun_case_f args res
-  | Tpointer (Tfunction args res) _ => fun_case_f args res
+  | Tfunction args res cc => fun_case_f args res cc
+  | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc
   | _ => fun_default
   end.
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index be3ee4b..2eedbd8 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -322,11 +322,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
     (More exactly, identification of function calls that can reduce.) *)
 
 Inductive callred: expr -> fundef -> list val -> type -> Prop :=
-  | red_Ecall: forall vf tyf tyargs tyres el ty fd vargs,
+  | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs,
       Genv.find_funct ge vf = Some fd ->
       cast_arguments el tyargs vargs ->
-      type_of_fundef fd = Tfunction tyargs tyres ->
-      classify_fun tyf = fun_case_f tyargs tyres ->
+      type_of_fundef fd = Tfunction tyargs tyres cconv ->
+      classify_fun tyf = fun_case_f tyargs tyres cconv ->
       callred (Ecall (Eval vf tyf) el ty)
               fd vargs ty.
 
@@ -754,9 +754,9 @@ Inductive sstep: state -> trace -> state -> Prop :=
       sstep (Callstate (Internal f) vargs k m)
          E0 (State f f.(fn_body) k e m2)
 
-  | step_external_function: forall ef targs tres vargs k m vres t m',
+  | step_external_function: forall ef targs tres cc vargs k m vres t m',
       external_call ef  ge vargs m t vres m' ->
-      sstep (Callstate (External ef targs tres) vargs k m)
+      sstep (Callstate (External ef targs tres cc) vargs k m)
           t (Returnstate vres k m')
 
   | step_returnstate: forall v f e C ty k m,
@@ -781,7 +781,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 6ae33a6..4b2e915 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -475,7 +475,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      funsig f = mksignature nil (Some Tint) ->
+      funsig f = signature_main ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 0ed008f..1380695 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -443,10 +443,28 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist)
       do ta1' <- make_cast (typeof a1) ty1 ta1;
       do ta2 <- transl_arglist a2 ty2;      
       OK (ta1' :: ta2)
+  | a1 :: a2, Tnil =>
+      (* Tolerance for calls to K&R or variadic functions *)
+      do ta1 <- transl_expr a1;
+      do ta2 <- transl_arglist a2 Tnil;
+      OK (ta1 :: ta2)
   | _, _ =>
       Error(msg "Cshmgen.transl_arglist: arity mismatch")
   end.
 
+(** Compute the argument signature that corresponds to a function application. *)
+
+Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
+                            {struct al}: list AST.typ :=
+  match al, tyl with
+  | nil, _ => nil
+  | a1 :: a2, Tcons ty1 ty2 =>
+      typ_of_type ty1 :: typlist_of_arglist a2 ty2
+  | a1 :: a2, Tnil =>
+      (* Tolerance for calls to K&R or variadic functions *)
+      typ_of_type_default (typeof a1) :: typlist_of_arglist a2 Tnil
+  end.
+
 (** * Translation of statements *)
 
 (** [transl_statement nbrk ncnt s] returns a Csharpminor statement
@@ -487,10 +505,13 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
       OK(Sset x tb)
   | Clight.Scall x b cl =>
       match classify_fun (typeof b) with
-      | fun_case_f args res =>
+      | fun_case_f args res cconv =>
           do tb <- transl_expr b;
           do tcl <- transl_arglist cl args;
-          OK(Scall x (signature_of_type args res) tb tcl)
+          OK(Scall x {| sig_args := typlist_of_arglist cl args;
+                        sig_res  := opttyp_of_type res;
+                        sig_cc   := cconv |}
+                   tb tcl)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
   | Clight.Sbuiltin x ef tyargs bl =>
@@ -547,8 +568,9 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat)
 Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)).
 
 Definition signature_of_function (f: Clight.function) :=
-  mksignature (map typ_of_type (map snd (Clight.fn_params f)))
-              (opttyp_of_type (Clight.fn_return f)).
+  {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
+     sig_res  := opttyp_of_type (Clight.fn_return f);
+     sig_cc   := Clight.fn_callconv f |}.
 
 Definition transl_function (f: Clight.function) : res function :=
   do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
@@ -563,9 +585,8 @@ Definition transl_fundef (f: Clight.fundef) : res fundef :=
   match f with
   | Clight.Internal g => 
       do tg <- transl_function g; OK(AST.Internal tg)
-  | Clight.External ef args res =>
-      if list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist args)
-      && opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type res)
+  | Clight.External ef args res cconv =>
+      if signature_eq (ef_sig ef) (signature_of_type args res cconv)
       then OK(AST.External ef)
       else Error(msg "Cshmgen.transl_fundef: wrong external signature")
   end.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 220d907..d6e881e 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -40,28 +40,24 @@ Proof.
 Qed.
 
 Lemma transl_fundef_sig1:
-  forall f tf args res,
+  forall f tf args res cc,
   transl_fundef f = OK tf ->
-  classify_fun (type_of_fundef f) = fun_case_f args res ->
-  funsig tf = signature_of_type args res.
+  classify_fun (type_of_fundef f) = fun_case_f args res cc ->
+  funsig tf = signature_of_type args res cc.
 Proof.
   intros. destruct f; simpl in *. 
   monadInv H. monadInv EQ. simpl. inversion H0.    
   unfold signature_of_function, signature_of_type.
   f_equal. apply transl_params_types.
-  destruct (list_typ_eq (sig_args (ef_sig e)) (typlist_of_typelist t)); simpl in H.
-  destruct (opt_typ_eq (sig_res (ef_sig e)) (opttyp_of_type t0)); simpl in H.
-  inv H. simpl. destruct (ef_sig e); simpl in *. inv H0.
-  unfold signature_of_type. auto.
-  congruence.
-  congruence.
+  destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H.
+  simpl. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
-  forall f tf args res,
+  forall f tf args res cc,
   transl_fundef f = OK tf ->
-  type_of_fundef f = Tfunction args res ->
-  funsig tf = signature_of_type args res.
+  type_of_fundef f = Tfunction args res cc ->
+  funsig tf = signature_of_type args res cc.
 Proof.
   intros. eapply transl_fundef_sig1; eauto.
   rewrite H0; reflexivity.
@@ -982,6 +978,16 @@ Proof.
   eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. 
 Qed.
 
+Lemma typlist_of_arglist_eq:
+  forall al tyl vl,
+  Clight.eval_exprlist ge e le m al tyl vl ->
+  typlist_of_arglist al tyl = typlist_of_typelist tyl.
+Proof.
+  induction 1; simpl.
+  auto.
+  f_equal; auto.
+Qed.
+
 End EXPR.
 
 (** ** Semantic preservation for statements *)
@@ -1064,11 +1070,11 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
       match_states (Clight.State f s k e le m)
                    (State tf ts' tk' te le m)
   | match_callstate:
-      forall fd args k m tfd tk targs tres
+      forall fd args k m tfd tk targs tres cconv
           (TR: transl_fundef fd = OK tfd)
           (MK: match_cont Tvoid 0%nat 0%nat k tk)
           (ISCC: Clight.is_call_cont k)
-          (TY: type_of_fundef fd = Tfunction targs tres),
+          (TY: type_of_fundef fd = Tfunction targs tres cconv),
       match_states (Clight.Callstate fd args k m)
                    (Callstate tfd args tk m)
   | match_returnstate:
@@ -1232,13 +1238,14 @@ Proof.
 
 (* call *)
   revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
-  intros targs tres CF TR. monadInv TR. inv MTR. 
+  intros targs tres cc CF TR. monadInv TR. inv MTR. 
   exploit functions_translated; eauto. intros [tfd [FIND TFD]].
   rewrite H in CF. simpl in CF. inv CF.
   econstructor; split.
   apply plus_one. econstructor; eauto. 
   exploit transl_expr_correct; eauto.
   exploit transl_arglist_correct; eauto.
+  erewrite typlist_of_arglist_eq by eauto. 
   eapply transl_fundef_sig1; eauto.
   rewrite H3. auto.
   econstructor; eauto.  
@@ -1422,9 +1429,7 @@ Proof.
 
 (* external function *)
   simpl in TR. 
-  destruct (list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist targs) &&
-            opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type tres));
-  monadInv TR. 
+  destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. constructor. eauto. 
@@ -1451,7 +1456,7 @@ Proof.
     rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog).
     auto. symmetry. unfold transl_program in TRANSL. 
     eapply transform_partial_program2_main; eauto.
-  assert (funsig tf = signature_of_type Tnil type_int32s).
+  assert (funsig tf = signature_of_type Tnil type_int32s cc_default).
     eapply transl_fundef_sig2; eauto. 
   econstructor; split.
   econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. 
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 7988dfa..b1fbebe 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -359,13 +359,13 @@ Inductive estep: state -> trace -> state -> Prop :=
       estep (ExprState f (C (Eparen r ty)) k e m)
          E0 (ExprState f (C (Eval v ty)) k e m)
 
-  | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd,
+  | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd,
       leftcontext RV RV C ->
-      classify_fun (typeof rf) = fun_case_f targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres cconv ->
       eval_simple_rvalue e m rf vf ->
       eval_simple_list e m rargs targs vargs ->
       Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = Tfunction targs tres ->
+      type_of_fundef fd = Tfunction targs tres cconv ->
       estep (ExprState f (C (Ecall rf rargs ty)) k e m)
          E0 (Callstate fd vargs (Kcall f e C ty k) m)
 
@@ -562,11 +562,11 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists v, sem_cast v1 ty1 ty = Some v
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
-      exists tyargs, exists tyres, exists fd, exists vl,
-         classify_fun tyf = fun_case_f tyargs tyres
+      exists tyargs tyres cconv fd vl,
+         classify_fun tyf = fun_case_f tyargs tyres cconv
       /\ Genv.find_funct ge vf = Some fd
       /\ cast_arguments rargs tyargs vl
-      /\ type_of_fundef fd = Tfunction tyargs tyres
+      /\ type_of_fundef fd = Tfunction tyargs tyres cconv
   | Ebuiltin ef tyargs rargs ty =>
       exprlist_all_values rargs ->
       exists vargs, exists t, exists vres, exists m',
@@ -610,7 +610,7 @@ Lemma callred_invert:
   invert_expr_prop r m.
 Proof.
   intros. inv H. simpl.
-  intros. exists tyargs; exists tyres; exists fd; exists args; auto.
+  intros. exists tyargs, tyres, cconv, fd, args; auto.
 Qed.
 
 Scheme context_ind2 := Minimality for context Sort Prop
@@ -1369,7 +1369,7 @@ Proof.
   eapply safe_steps. eexact S1.
   apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto.
   simpl. intros X. exploit X. eapply rval_list_all_values. 
-  intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]].
+  intros [tyargs [tyres [cconv [fd [vargs [P [Q [U V]]]]]]]].
   econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. 
 (* builtin *)
   pose (C' := fun x => C(Ebuiltin ef tyargs x ty)).
@@ -1756,13 +1756,13 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       ty = typeof r2 ->
       eval_expr e m RV (Ecomma r1 r2 ty) (t1**t2) m2 r2'
   | eval_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs
-                      targs tres fd t3 m3 vres,
+                      targs tres cconv fd t3 m3 vres,
       eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
       eval_simple_rvalue ge e m2 rf' vf ->
       eval_simple_list ge e m2 rargs' targs vargs ->
-      classify_fun (typeof rf) = fun_case_f targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres cconv ->
       Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = Tfunction targs tres ->
+      type_of_fundef fd = Tfunction targs tres cconv ->
       eval_funcall m2 fd vargs t3 m3 vres ->
       eval_expr e m RV (Ecall rf rargs ty) (t1**t2**t3) m3 (Eval vres ty)
 
@@ -1901,9 +1901,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       outcome_result_value out f.(fn_return) vres ->
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
-  | eval_funcall_external: forall m ef targs tres vargs t vres m',
+  | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
       external_call ef ge vargs m t vres m' ->
-      eval_funcall m (External ef targs tres) vargs t m' vres.
+      eval_funcall m (External ef targs tres cconv) vargs t m' vres.
 
 Scheme eval_expression_ind5 := Minimality for eval_expression Sort Prop
   with eval_expr_ind5 := Minimality for eval_expr Sort Prop
@@ -1999,13 +1999,13 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop :=
       evalinf_exprlist e m1 a2 t2 ->
       evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2)
   | evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs
-                      targs tres fd t3,
+                      targs tres cconv fd t3,
       eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
       eval_simple_rvalue ge e m2 rf' vf ->
       eval_simple_list ge e m2 rargs' targs vargs ->
-      classify_fun (typeof rf) = fun_case_f targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres cconv ->
       Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = Tfunction targs tres ->
+      type_of_fundef fd = Tfunction targs tres cconv ->
       evalinf_funcall m2 fd vargs t3 ->
       evalinf_expr e m RV (Ecall rf rargs ty) (t1***t2***t3)
 
@@ -3034,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
@@ -3044,7 +3044,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
+      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.
 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 8b98556..ea1bd86 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -177,6 +177,7 @@ with labeled_statements : Type :=            (**r cases of a [switch] *)
 
 Record function : Type := mkfunction {
   fn_return: type;
+  fn_callconv: calling_convention;
   fn_params: list (ident * type);
   fn_vars: list (ident * type);
   fn_body: statement
@@ -190,17 +191,17 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 
 Inductive fundef : Type :=
   | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> fundef.
+  | External: external_function -> typelist -> type -> calling_convention -> fundef.
 
 (** The type of a function definition. *)
 
 Definition type_of_function (f: function) : type :=
-  Tfunction (type_of_params (fn_params f)) (fn_return f).
+  Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
 
 Definition type_of_fundef (f: fundef) : type :=
   match f with
   | Internal fd => type_of_function fd
-  | External id args res => Tfunction args res
+  | External id args res cc => Tfunction args res cc
   end.
 
 (** ** Programs *)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index c9ef996..2b409ab 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -97,7 +97,7 @@ Inductive type : Type :=
   | Tfloat: floatsize -> attr -> type              (**r floating-point types *)
   | Tpointer: type -> attr -> type                 (**r pointer types ([*ty]) *)
   | Tarray: type -> Z -> attr -> type              (**r array types ([ty[len]]) *)
-  | Tfunction: typelist -> type -> type            (**r function types *)
+  | Tfunction: typelist -> type -> calling_convention -> type    (**r function types *)
   | Tstruct: ident -> fieldlist -> attr -> type    (**r struct types *)
   | Tunion: ident -> fieldlist -> attr -> type     (**r union types *)
   | Tcomp_ptr: ident -> attr -> type               (**r pointer to named struct or union *)
@@ -119,11 +119,11 @@ Proof.
   assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
   assert (forall (x y: attr), {x=y} + {x<>y}).
   { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
-  generalize ident_eq zeq. intros E1 E2. 
+  generalize ident_eq zeq bool_dec. intros E1 E2 E3.
   decide equality.
   decide equality.
-  generalize ident_eq. intros E1.
   decide equality.
+  generalize ident_eq. intros E1. decide equality.
 Defined.
 
 Opaque type_eq typelist_eq fieldlist_eq.
@@ -138,7 +138,7 @@ Definition attr_of_type (ty: type) :=
   | Tfloat sz a => a
   | Tpointer elt a => a
   | Tarray elt sz a => a
-  | Tfunction args res => noattr
+  | Tfunction args res cc => noattr
   | Tstruct id fld a => a
   | Tunion id fld a => a
   | Tcomp_ptr id a => a
@@ -154,7 +154,7 @@ Definition typeconv (ty: type) : type :=
   match ty with
   | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a
   | Tarray t sz a       => Tpointer t a
-  | Tfunction _ _       => Tpointer ty noattr
+  | Tfunction _ _ _     => Tpointer ty noattr
   | _                   => ty
   end.
 
@@ -177,7 +177,7 @@ Fixpoint alignof (t: type) : Z :=
       | Tfloat F64 _ => 8
       | Tpointer _ _ => 4
       | Tarray t' _ _ => alignof t'
-      | Tfunction _ _ => 1
+      | Tfunction _ _ _ => 1
       | Tstruct _ fld _ => alignof_fields fld
       | Tunion _ fld _ => alignof_fields fld
       | Tcomp_ptr _ _ => 4
@@ -252,7 +252,7 @@ Fixpoint sizeof (t: type) : Z :=
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
   | Tarray t' n _ => sizeof t' * Zmax 1 n
-  | Tfunction _ _ => 1
+  | Tfunction _ _ _ => 1
   | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
   | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t)
   | Tcomp_ptr _ _ => 4
@@ -302,7 +302,7 @@ Fixpoint naturally_aligned (t: type) : Prop :=
       attr_alignas a = None
   | Tarray t' _ a =>
       attr_alignas a = None /\ naturally_aligned t'
-  | Tvoid | Tfunction _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
+  | Tvoid | Tfunction _ _ _ | Tstruct _ _ _ | Tunion _ _ _ =>
       True
   end.
 
@@ -478,7 +478,7 @@ Definition access_mode (ty: type) : mode :=
   | Tvoid => By_nothing
   | Tpointer _ _ => By_value Mint32
   | Tarray _ _ _ => By_reference
-  | Tfunction _ _ => By_reference
+  | Tfunction _ _ _ => By_reference
   | Tstruct _ _ _ => By_copy
   | Tunion _ _ _ => By_copy
   | Tcomp_ptr _ _ => By_nothing
@@ -510,7 +510,7 @@ Fixpoint unroll_composite (ty: type) : type :=
   | Tfloat _ _ => ty
   | Tpointer t1 a => Tpointer (unroll_composite t1) a
   | Tarray t1 sz a => Tarray (unroll_composite t1) sz a
-  | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2)
+  | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a
   | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a
   | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a
   | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty
@@ -586,7 +586,7 @@ Fixpoint alignof_blockcopy (t: type) : Z :=
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
   | Tarray t' _ _ => alignof_blockcopy t'
-  | Tfunction _ _ => 1
+  | Tfunction _ _ _ => 1
   | Tstruct _ fld _ => Zmin 8 (alignof t)
   | Tunion _ fld _ => Zmin 8 (alignof t)
   | Tcomp_ptr _ _ => 4
@@ -681,5 +681,15 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
   | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl
   end.
 
-Definition signature_of_type (args: typelist) (res: type) : signature :=
-  mksignature (typlist_of_typelist args) (opttyp_of_type res).
+Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
+  mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
+
+(** Like [typ_of_type], but apply default argument promotion. *)
+
+Definition typ_of_type_default (t: type) : AST.typ :=
+  match t with
+  | Tfloat _ _ => AST.Tfloat
+  | Tlong _ _ => AST.Tlong
+  | _ => AST.Tint
+  end.
+
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 5db4718..b6fc728 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -680,7 +680,7 @@ Qed.
 
 (** A semantics for general initializers *)
 
-Definition dummy_function := mkfunction Tvoid nil nil Sskip.
+Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip.
 
 Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) :=
   match fl with
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 78ab7fc..376707a 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -229,7 +229,7 @@ and print_stmt_for p s =
 let print_function p id f =
   fprintf p "%s@ "
             (name_cdecl (name_function_parameters (extern_atom id)
-                                                  f.fn_params)
+                                                  f.fn_params f.fn_callconv)
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
@@ -245,10 +245,10 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res) ->
+  | External(EF_external(_,_), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
-                (name_cdecl (extern_atom id) (Tfunction(args, res)))
-  | External(_, _, _) ->
+                (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
+  | External(_, _, _, _) ->
       ()
   | Internal f ->
       print_function p id f
@@ -309,7 +309,7 @@ let collect_function f =
 
 let collect_globdef (id, gd) =
   match gd with
-  | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+  | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
   | Gfun(Internal f) -> collect_function f
   | Gvar v -> collect_type v.gvar_info
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 4db8976..758323e 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -88,11 +88,6 @@ let attributes a =
 let name_optid id =
   if id = "" then "" else " " ^ id
 
-(*
-let parenthesize_if_pointer id =
-  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
-*)
-
 let rec name_cdecl id ty =
   match ty with
   | Tvoid ->
@@ -111,24 +106,26 @@ let rec name_cdecl id ty =
       name_cdecl id' t
   | Tarray(t, n, a) ->
       name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t
-  | Tfunction(args, res) ->
+  | Tfunction(args, res, cconv) ->
       let b = Buffer.create 20 in
       if id = ""
       then Buffer.add_string b "(*)"
       else Buffer.add_string b id;
       Buffer.add_char b '(';
-      begin match args with
+      let rec add_args first = function
       | Tnil ->
-          Buffer.add_string b "void"
-      | _ ->
-          let rec add_args first = function
-          | Tnil -> ()
-          | Tcons(t1, tl) ->
-              if not first then Buffer.add_string b ", ";
-              Buffer.add_string b (name_cdecl "" t1);
-              add_args false tl in
-          add_args true args
-      end;
+          if first then
+            Buffer.add_string b
+               (if cconv.cc_vararg then "..." else "void")
+          else if cconv.cc_vararg then
+            Buffer.add_string b ", ..."
+          else
+            ()
+      | Tcons(t1, tl) ->
+          if not first then Buffer.add_string b ", ";
+          Buffer.add_string b (name_cdecl "" t1);
+          add_args false tl in
+      add_args true args;
       Buffer.add_char b ')';
       name_cdecl (Buffer.contents b) res
   | Tstruct(name, fld, a) ->
@@ -351,16 +348,17 @@ and print_stmt_for p s =
   | _ ->
       fprintf p "({ %a })" print_stmt s
 
-let name_function_parameters fun_name params =
+let name_function_parameters fun_name params cconv =
   let b = Buffer.create 20 in
   Buffer.add_string b fun_name;
   Buffer.add_char b '(';
   begin match params with
   | [] ->
-      Buffer.add_string b "void"
+      Buffer.add_string b (if cconv.cc_vararg then "..." else "void")
   | _ ->
       let rec add_params first = function
-      | [] -> ()
+      | [] ->
+          if cconv.cc_vararg then Buffer.add_string b "..."
       | (id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl (extern_atom id) ty);
@@ -373,7 +371,7 @@ let name_function_parameters fun_name params =
 let print_function p id f =
   fprintf p "%s@ "
             (name_cdecl (name_function_parameters (extern_atom id)
-                                                  f.fn_params)
+                                                  f.fn_params f.fn_callconv)
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
@@ -385,10 +383,10 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res) ->
+  | External(EF_external(_,_), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
-                (name_cdecl (extern_atom id) (Tfunction(args, res)))
-  | External(_, _, _) ->
+                (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
+  | External(_, _, _, _) ->
       ()
   | Internal f ->
       print_function p id f
@@ -474,7 +472,7 @@ let rec collect_type = function
   | Tlong _ -> ()
   | Tpointer(t, _) -> collect_type t
   | Tarray(t, _, _) -> collect_type t
-  | Tfunction(args, res) -> collect_type_list args; collect_type res
+  | Tfunction(args, res, _) -> collect_type_list args; collect_type res
   | Tstruct(id, fld, _) | Tunion(id, fld, _) ->
       let s = extern_atom id in
       if not (StructUnion.mem s !struct_unions) then begin
@@ -552,7 +550,7 @@ let collect_function f =
 
 let collect_globdef (id, gd) =
   match gd with
-  | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res
+  | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
   | Gfun(Internal f) -> collect_function f
   | Gvar v -> collect_type v.gvar_info
 
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 1ead0ae..01f304e 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -504,6 +504,7 @@ Definition transl_function (f: Csyntax.function) : mon function :=
   do temps <- get_trail;
   ret (mkfunction
               f.(Csyntax.fn_return)
+              f.(Csyntax.fn_callconv)
               f.(Csyntax.fn_params)
               f.(Csyntax.fn_vars)
               temps
@@ -513,8 +514,8 @@ Definition transl_fundef (fd: Csyntax.fundef) : mon fundef :=
   match fd with
   | Csyntax.Internal f =>
       do tf <- transl_function f; ret (Internal tf)
-  | Csyntax.External ef targs tres =>
-      ret (External ef targs tres)
+  | Csyntax.External ef targs tres cconv =>
+      ret (External ef targs tres cconv)
   end.
 
 Local Open Scope error_monad_scope.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index b3c861e..9134e11 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -2166,9 +2166,9 @@ Proof.
   inv H7. inversion H3; subst.
   econstructor; split.
   left; apply plus_one. eapply step_internal_function. econstructor.
-  rewrite H5; rewrite H6; auto.
-  rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto.
-  rewrite H5. eapply bind_parameters_preserved; eauto.
+  rewrite H6; rewrite H7; auto.
+  rewrite H6; rewrite H7. eapply alloc_variables_preserved; eauto.
+  rewrite H6. eapply bind_parameters_preserved; eauto.
   eauto. 
   constructor; auto. 
 
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 9dfa42e..3dae7ab 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -1090,6 +1090,7 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
   | tr_function_intro: forall f tf,
       tr_stmt f.(Csyntax.fn_body) tf.(fn_body) ->
       fn_return tf = Csyntax.fn_return f ->
+      fn_callconv tf = Csyntax.fn_callconv f ->
       fn_params tf = Csyntax.fn_params f ->
       fn_vars tf = Csyntax.fn_vars f ->
       tr_function f tf.
@@ -1098,8 +1099,8 @@ Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
   | tr_internal: forall f tf,
       tr_function f tf ->
       tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
-  | tr_external: forall ef targs tres,
-      tr_fundef (Csyntax.External ef targs tres) (External ef targs tres).
+  | tr_external: forall ef targs tres cconv,
+      tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
 
 Lemma transl_function_spec:
   forall f tf g g' i,
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 95ff9ed..2956508 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -229,6 +229,7 @@ Definition transf_function (f: function) : res function :=
   assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
   do body' <- simpl_stmt cenv f.(fn_body);
   OK {| fn_return := f.(fn_return);
+        fn_callconv := f.(fn_callconv);
         fn_params := f.(fn_params);
         fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars));
         fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps);
@@ -239,7 +240,7 @@ Definition transf_function (f: function) : res function :=
 Definition transf_fundef (fd: fundef) : res fundef :=
   match fd with
   | Internal f => do tf <- transf_function f; OK (Internal tf)
-  | External ef targs tres => OK (External ef targs tres)
+  | External ef targs tres cconv => OK (External ef targs tres cconv)
   end.
 
 Definition transf_program (p: program) : res program :=
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 552c991..ae98130 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1710,12 +1710,12 @@ Inductive match_states: state -> state -> Prop :=
       match_states (State f s k e le m)
                    (State tf ts tk te tle tm)
   | match_call_state:
-      forall fd vargs k m tfd tvargs tk tm j targs tres
+      forall fd vargs k m tfd tvargs tk tm j targs tres cconv
         (TRFD: transf_fundef fd = OK tfd)
         (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
         (MINJ: Mem.inject j m tm)
         (AINJ: val_list_inject j vargs tvargs)
-        (FUNTY: type_of_fundef fd = Tfunction targs tres)
+        (FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
         (ANORM: val_casted_list vargs targs),
       match_states (Callstate fd vargs k m)
                    (Callstate tfd tvargs tk tm)