From 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 18 Aug 2011 15:28:46 +0000 Subject: 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 --- ia32/Asmgenproof.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 5b98d27..e8c6757 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -455,6 +455,8 @@ Remark transl_op_label: Proof. unfold transl_op; intros. destruct op; ArgsInv; auto. eapply mk_mov_label; eauto. + destruct (Int.eq_dec i Int.zero); auto. + destruct (Float.eq_dec f Float.zero); auto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. -- cgit v1.2.3