From 708cd2c7767b497b9ac3dae1ce51973195d00acc Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 6 Sep 2006 19:44:10 +0000 Subject: 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 --- cfrontend/Ctyping.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'cfrontend/Ctyping.v') 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. -- cgit