diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-18 15:28:46 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-18 15:28:46 +0000 |
commit | 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e (patch) | |
tree | fd315fb086acb9e81882a2bc1b255b9562d8940d /ia32/Asmgenproof1.v | |
parent | 50ee6bdf639ffba989968abb9c24a57126ab35a4 (diff) | |
download | compcert-5b73a4f223a0cadb7df3f1320fed86cde0d67d6e.tar.gz compcert-5b73a4f223a0cadb7df3f1320fed86cde0d67d6e.zip |
More careful treatment of 'load immediate 0' as 'xor self'
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenproof1.v')
-rw-r--r-- | ia32/Asmgenproof1.v | 26 |
1 files changed, 4 insertions, 22 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 27bc9013..c00332ed 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1429,28 +1429,6 @@ Qed. (** Translation of arithmetic operations. *) -(* -Ltac TranslOpSimpl := - match goal with - | |- exists rs' : regset, - exec_straight ?c ?rs ?m ?k rs' ?m /\ - agree (Regmap.set ?res ?v ?ms) ?sp rs' => - (exists (nextinstr (rs#(ireg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - end. -*) - Ltac ArgsInv := match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -1484,6 +1462,10 @@ Proof. (* move *) exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. exists rs2. split. eauto. split. simpl. auto. intros. destruct H; auto. +(* intconst *) + inv EV. destruct (Int.eq_dec i Int.zero). subst i. TranslOp. TranslOp. +(* floatconst *) + inv EV. destruct (Float.eq_dec f Float.zero). subst f. TranslOp. TranslOp. (* cast8signed *) eapply mk_intconv_correct; eauto. (* cast8unsigned *) |