From 40653a485d26e94b57a01250623182f0f5358e10 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 2 Jan 2014 20:24:50 +0000
Subject: Updated neededness analysis for IA32.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/NeedDomain.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 99d70a8..47f6975 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -603,7 +603,7 @@ Proof.
 - destruct v; auto with na.
 Qed.
 
-(** Modular arithmetic operations: add, mul.  
+(** Modular arithmetic operations: add, mul, opposite.  
     (But not subtraction because of the pointer - pointer case. *)
 
 Definition modarith (x: nval) :=
@@ -642,6 +642,19 @@ Proof.
 - inv H; auto. inv H0; auto. destruct w1; auto. 
 Qed.
 
+Lemma neg_sound:
+  forall v w x,
+  vagree v w (modarith x) ->
+  vagree (Val.neg v) (Val.neg w) x.
+Proof.
+  intros; destruct x; simpl in *.
+- auto.
+- unfold Val.neg; InvAgree. 
+  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. 
+- destruct v, w; simpl; auto. 
+- inv H; simpl; auto.
+Qed.
+
 (** Conversions: zero extension, sign extension, single-of-float *)
 
 Definition zero_ext (n: Z) (x: nval) :=
-- 
cgit v1.2.3