cond_valid_pointer_eq

1 files changed, 10 insertions, 0 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 762c3a02..9e98d517 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -872,6 +872,16 @@ Proof.
   unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+ 
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->