diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
| commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
| tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /common/Main.v | |
| parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
| download | compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.tar.gz compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.zip | |
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Main.v')
| -rw-r--r-- | common/Main.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/common/Main.v b/common/Main.v index 33bc7830..db159298 100644 --- a/common/Main.v +++ b/common/Main.v @@ -258,10 +258,10 @@ Proof. Qed. Theorem transf_cminor_program_correct: - forall p tp t n, + forall p tp beh, transf_cminor_program p = OK tp -> - Cminor.exec_program p t (Vint n) -> - PPC.exec_program tp (Terminates t n). + Cminor.exec_program p beh -> + PPC.exec_program tp beh. Proof. intros. unfold transf_cminor_program, transf_cminor_fundef in H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. @@ -276,12 +276,12 @@ Proof. Qed. Theorem transf_c_program_correct: - forall p tp t n, + forall p tp beh, transf_c_program p = OK tp -> - Csem.exec_program p t (Vint n) -> - PPC.exec_program tp (Terminates t n). + Csem.exec_program p beh -> + PPC.exec_program tp beh. Proof. - intros until n; unfold transf_c_program; simpl. + intros until beh; unfold transf_c_program; simpl. caseEq (Ctyping.typecheck_program p); try congruence; intro. caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. |