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

1 files changed, 10 insertions, 10 deletions

diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 4d10c622..f7a0e189 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.