diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-06 19:44:10 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-06 19:44:10 +0000 |
| commit | 708cd2c7767b497b9ac3dae1ce51973195d00acc (patch) | |
| tree | adb042e3603452fc7702db0c6eb55825864e0ded /cfrontend/Ctyping.v | |
| parent | e231ac08558e959f2ea2664082c62ced9e485c1b (diff) | |
| download | compcert-kvx-708cd2c7767b497b9ac3dae1ce51973195d00acc.tar.gz compcert-kvx-708cd2c7767b497b9ac3dae1ce51973195d00acc.zip | |
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
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 13 |
1 files changed, 9 insertions, 4 deletions
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. |