From 3334dc4b5bcc6f58e2c487a7f6d7c2aa6e09e797 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 22 Aug 2011 07:46:21 +0000 Subject: Harden proof script against empty destroyed_at_move git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1721 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RREproof.v | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/backend/RREproof.v b/backend/RREproof.v index da959ea5..d70a1fde 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -215,9 +215,8 @@ Lemma agree_regs: Proof. induction rl; intros; simpl. auto. - decEq. apply agree_reg with sm; auto. - destruct H0; auto. - right. eapply list_disjoint_notin; eauto with coqlib. + decEq. apply agree_reg with sm. auto. + destruct H0. auto. right. eapply list_disjoint_notin; eauto with coqlib. apply IHrl; auto. destruct H0; auto. right. eapply list_disjoint_cons_left; eauto. Qed. @@ -404,7 +403,7 @@ Opaque destroyed_at_move_regs. destruct sl; simpl in Heqb0; discriminate || auto. left; econstructor; split. constructor. repeat rewrite UGS. - apply match_states_regular with sm; auto. + apply match_states_regular with sm. auto. apply kill_loc_hold. apply kill_loc_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. apply agree_set. auto. tauto. @@ -419,7 +418,7 @@ Opaque destroyed_at_move_regs. assert (EQ1: rs' (S sl) = rs (S sl)) by (eapply agree_slot; eauto). assert (EQ2: rs' (R r) = rs (R r)) by (eapply agree_reg; eauto; tauto). rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same. - apply match_states_regular with sm; auto. tauto. + apply match_states_regular with sm; auto; tauto. (* found an equation *) destruct (find_reg_containing sl eqs) as [r'|]_eqn. exploit EQH. eapply find_reg_containing_sound; eauto. @@ -434,14 +433,14 @@ Opaque destroyed_at_move_regs. (* left as a getstack *) left; econstructor; split. constructor. repeat rewrite UGS. - apply match_states_regular with sm; auto. + apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. intuition congruence. (* no equation, left as a getstack *) left; econstructor; split. constructor. repeat rewrite UGS. - apply match_states_regular with sm; auto. + apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. tauto. -- cgit