From eb7c8587f462adca878088ef5f610c81734efc70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 19 Sep 2006 15:13:42 +0000 Subject: Meilleure compilation de la negation booleenne git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index f700f82..93eb99d 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -888,6 +888,13 @@ Proof. change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr. change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr. change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr. + replace (Int.eq i Int.zero) with (negb (negb (Int.eq i Int.zero))). + eapply eval_notbool. eauto. + generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro; simpl. + rewrite H1; constructor. constructor; auto. + apply negb_elim. + unfold Vfalse; TrivialOp. change (Vint Int.zero) with (Val.of_bool (negb true)). + eapply eval_notbool. eauto. constructor. change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr. (* Binary operations *) inversion H1; clear H1; subst. inversion H11; clear H11; subst. -- cgit v1.2.3