1 files changed, 15 insertions, 7 deletions
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index ecc758f..a71ead7 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -27,13 +27,6 @@ Require Import SelectOp.
 
 Open Local Scope cminorsel_scope.
 
-Section CMCONSTR.
-
-Variable ge: genv.
-Variable sp: val.
-Variable e: env.
-Variable m: mem.
-
 (** * Useful lemmas and tactics *)
 
 (** The following are trivial lemmas and custom tactics that help
@@ -81,6 +74,13 @@ Ltac TrivialExists :=
 
 (** * Correctness of the smart constructors *)
 
+Section CMCONSTR.
+
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
 (** We now show that the code generated by "smart constructor" functions
   such as [Selection.notint] behaves as expected.  Continuing the
   [notint] example, we show that if the expression [e]
@@ -172,6 +172,8 @@ Proof.
   subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
   subst. rewrite Val.add_commut. TrivialExists.
   subst. TrivialExists.
+  subst. TrivialExists. 
+  subst. rewrite Val.add_commut. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -325,6 +327,9 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero. 
   intros. exists (Vint Int.zero); split. EvalOp. 
   destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. exists x; split; auto. 
+  subst. destruct x; simpl; auto. rewrite Int.and_mone; auto.
   case (andimm_match a); intros.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
   InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. 
@@ -352,6 +357,9 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto.
   destruct x; simpl; auto. rewrite Int.or_zero; auto.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. exists (Vint Int.mone); split. EvalOp. 
+  destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
   destruct (orimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.or_commut; auto.
   subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.