diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
| commit | eb7c8587f462adca878088ef5f610c81734efc70 (patch) | |
| tree | 6771c5be9d0d6048357be99c663ec64981ad63dd /cfrontend/Cminorgenproof.v | |
| parent | 165407527b1be7df6a376791719321c788e55149 (diff) | |
Meilleure compilation de la negation booleenne
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |