diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
commit | be43363d309cea62731e04ad10dddf3ecafcacd1 (patch) | |
tree | f66c346d51df74d6b6ee34f654178a44250a33c8 /cfrontend/Cshmgenproof3.v | |
parent | 5e8237152cad0cf08d3eea0d5de8cd8bc499df69 (diff) | |
download | compcert-be43363d309cea62731e04ad10dddf3ecafcacd1.tar.gz compcert-be43363d309cea62731e04ad10dddf3ecafcacd1.zip |
Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure compilation de exit_if_false.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof3.v')
-rw-r--r-- | cfrontend/Cshmgenproof3.v | 26 |
1 files changed, 10 insertions, 16 deletions
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 5b4146bf..497286b3 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -725,11 +725,11 @@ Qed. Lemma transl_Efield_struct_correct: (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident) + (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) (ty : type) (delta : Z), eval_lvalue ge e m a t m1 l ofs -> eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tstruct fList -> + typeof a = Tstruct id fList -> field_offset i fList = Some delta -> eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l (Int.add ofs (Int.repr delta))). @@ -743,11 +743,11 @@ Qed. Lemma transl_Efield_union_correct: (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident) + (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) (ty : type), eval_lvalue ge e m a t m1 l ofs -> eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tunion fList -> + typeof a = Tunion id fList -> eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l ofs). Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -925,13 +925,9 @@ Lemma exit_if_false_true: exec_stmt tprog te m1 ts t m2 Out_normal. Proof. intros. monadInv H. rewrite <- H5. - eapply exec_Sifthenelse_false with (v1 := Vfalse). - eapply make_notbool_correct with (va := v); eauto. - inversion H3; subst; simpl; auto. - rewrite Int.eq_false; auto. - rewrite Int.eq_false; auto. - rewrite Float.eq_zero_false; auto. - simpl; auto. + exploit make_boolean_correct_true. eapply H0; eauto. eauto. + intros [vb [EVAL ISTRUE]]. + eapply exec_Sifthenelse_true with (v1 := vb); eauto. constructor. traceEq. Qed. @@ -945,11 +941,9 @@ Lemma exit_if_false_false: exec_stmt tprog te m1 ts t m2 (Out_exit 0). Proof. intros. monadInv H. rewrite <- H5. - eapply exec_Sifthenelse_true with (v1 := Vtrue). - eapply make_notbool_correct with (va := v); eauto. - inversion H3; subst; simpl; auto. - rewrite Float.eq_zero_true; auto. - simpl; apply Int.one_not_zero. + exploit make_boolean_correct_false. eapply H0; eauto. eauto. + intros [vb [EVAL ISFALSE]]. + eapply exec_Sifthenelse_false with (v1 := vb); eauto. constructor. traceEq. Qed. |