Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)

Ctyping: relaxation de l'hypothese de typage sur main
Cshmgenproof3: adaptation a ces changements.


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

3 files changed, 21 insertions, 10 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index ed5a1b4c..a76dcb49 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -742,5 +742,4 @@ Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
   exists b, exists f, exists m1,
   Genv.find_symbol ge p.(prog_main) = Some b /\
   Genv.find_funct_ptr ge b = Some f /\
-  type_of_fundef f = Tfunction Tnil (Tint I32 Signed) /\
   eval_funcall ge m0 f nil t m1 r.
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 5037d43f..5b4146bf 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1478,12 +1478,19 @@ Theorem transl_program_correct:
   Csem.exec_program prog t r ->
   Csharpminor.exec_program tprog t r.
 Proof.
-  intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF [TYP EVAL]]]]]].
+  intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF EVAL]]]]].
   inversion WT; subst.
-  
-  assert (type_of_fundef f = Tfunction Tnil (Tint I32 Signed)).
+
+  assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)).
     apply wt_program_main.
     eapply Genv.find_funct_ptr_symbol_inversion; eauto. 
+  elim H; clear H; intros targs TYP.
+  assert (targs = Tnil).
+    inversion EVAL; subst; simpl in TYP.
+    inversion H0; subst. injection TYP. rewrite <- H6. simpl; auto.
+    inversion TYP; subst targs0 tres. inversion H. simpl in H0. 
+    inversion H0. destruct targs; simpl in H8; congruence.
+  subst targs.
   exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]].
   exists b; exists tf; exists m1.
   split. 
@@ -1491,10 +1498,10 @@ Proof.
     rewrite (transform_partial_program2_main transl_fundef transl_globvar prog TRANSL). auto.
   split. auto.
   split. 
-    generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD H). simpl; auto.
+    generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto.
   rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL).
   generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL).
-  intro. eapply H0. 
+  intro. eapply H. 
   eapply function_ptr_well_typed; eauto.
   auto.
 Qed.
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 7c6a3790..797033dc 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -162,7 +162,7 @@ Record wt_program (p: program) : Prop :=  mk_wt_program {
   wt_program_main:
     forall fd,
     In (p.(prog_main), fd) p.(prog_funct) ->
-    type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)
+    exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)
 }.
 
 (** ** Type-checking algorithm *)
@@ -386,14 +386,18 @@ Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef)
   | External _ _ _ => true
   end &&
   if ident_eq id main
-  then eq_type (type_of_fundef fd) (Tfunction Tnil (Tint I32 Signed))
+  then match type_of_fundef fd with
+       | Tfunction targs tres => eq_type tres (Tint I32 Signed)
+       | _ => false
+       end
   else true.
 
 Lemma typecheck_fundef_correct:
   forall main env id fd,
   typecheck_fundef main env (id, fd) = true ->
   wt_fundef env fd /\
-  (id = main -> type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)).
+  (id = main ->
+   exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)).
 Proof.
   intros. unfold typecheck_fundef in H; TrueInv.
   split. 
@@ -401,7 +405,8 @@ Proof.
     constructor. apply typecheck_function_correct; auto. 
     constructor.
   intro. destruct (ident_eq id main). 
-  apply eq_type_correct; auto.
+  destruct (type_of_fundef fd); try discriminate. 
+  exists t; decEq; auto. apply eq_type_correct; auto.
   congruence.
 Qed.