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/common/Events.v b/common/Events.v
index 24c03dce..cf576504 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -764,7 +764,7 @@ Qed.
 Lemma volatile_load_ok:
   forall chunk,
   extcall_properties (volatile_load_sem chunk) 
-                     (mksignature (Tint :: nil) (Some (type_of_chunk chunk))).
+                     (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -826,7 +826,7 @@ Qed.
 Lemma volatile_load_global_ok:
   forall chunk id ofs,
   extcall_properties (volatile_load_global_sem chunk id ofs) 
-                     (mksignature nil (Some (type_of_chunk chunk))).
+                     (mksignature nil (Some (type_of_chunk chunk)) cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -967,7 +967,7 @@ Qed.
 Lemma volatile_store_ok:
   forall chunk,
   extcall_properties (volatile_store_sem chunk) 
-                     (mksignature (Tint :: type_of_chunk chunk :: nil) None).
+                     (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -1022,7 +1022,7 @@ Qed.
 Lemma volatile_store_global_ok:
   forall chunk id ofs,
   extcall_properties (volatile_store_global_sem chunk id ofs) 
-                     (mksignature (type_of_chunk chunk :: nil) None).
+                     (mksignature (type_of_chunk chunk :: nil) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -1070,7 +1070,7 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V):
 
 Lemma extcall_malloc_ok:
   extcall_properties extcall_malloc_sem 
-                     (mksignature (Tint :: nil) (Some Tint)).
+                     (mksignature (Tint :: nil) (Some Tint) cc_default).
 Proof.
   assert (UNCHANGED:
     forall (P: block -> Z -> Prop) m n m' b m'',
@@ -1145,7 +1145,7 @@ Inductive extcall_free_sem  (F V: Type) (ge: Genv.t F V):
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem 
-                     (mksignature (Tint :: nil) None).
+                     (mksignature (Tint :: nil) None cc_default).
 Proof.
   constructor; intros.
 (* well typed *)
@@ -1241,7 +1241,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -
 
 Lemma extcall_memcpy_ok:
   forall sz al,
-  extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None).
+  extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default).
 Proof.
   intros. constructor.
 (* return type *)
@@ -1337,7 +1337,7 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g
 
 Lemma extcall_annot_ok:
   forall text targs,
-  extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None).
+  extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -1381,7 +1381,7 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv.
 
 Lemma extcall_annot_val_ok:
   forall text targ,
-  extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)).
+  extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -1433,7 +1433,7 @@ Axiom external_functions_properties:
 Parameter inline_assembly_sem: ident -> extcall_sem.
 
 Axiom inline_assembly_properties:
-  forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None).
+  forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default).
 
 (** ** Combined semantics of external calls *)