diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-12 14:07:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-12 14:07:58 +0000 |
| commit | 76e7f701c10e517737ae095a0293b68f5205be90 (patch) | |
| tree | 4b4dc7cfa22cb30962ac4b78005660317a1138b3 /backend | |
| parent | eafbaf41e528cc9825a503c66739a66a92ca65a8 (diff) | |
Simplify LPMap by smashing bottoms.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Constpropproof.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dcab6f6..328f724 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -80,10 +80,10 @@ Lemma regs_match_approx_update: regs_match_approx ra rs -> regs_match_approx (D.set r a ra) (rs#r <- v). Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. + intros; red; intros. + rewrite D.gsspec. rewrite Regmap.gsspec. destruct (peq r0 r); auto. + red; intros; subst ra. specialize (H0 xH). rewrite D.get_bot in H0. inv H0. + unfold Approx.eq. red; intros; subst a. inv H. Qed. Lemma approx_regs_val_list: @@ -103,9 +103,10 @@ Lemma regs_match_approx_forget: Proof. induction rl; simpl; intros. auto. - apply IHrl. red; intros. destruct (peq r a). - subst a. rewrite D.gss. constructor. - rewrite D.gso; auto. + apply IHrl. + red; intros. rewrite D.gsspec. destruct (peq r a). constructor. auto. + red; intros; subst ra. specialize (H xH). inv H. + unfold Approx.eq, Approx.bot. congruence. Qed. (** The correctness of the static analysis follows from the results |