From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 28 Aug 2007 12:57:58 +0000 Subject: 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 --- common/Main.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'common/Main.v') 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. -- cgit