diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
| commit | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (patch) | |
| tree | 05a5bcfc207c67f58575fa7b61787c0c9dbe8215 /arm/Asmgenproof1.v | |
| parent | f1ceca440c0322001abe6c5de79bd4bc309fc002 (diff) | |
| download | compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.tar.gz compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.zip | |
Pointers one past
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgenproof1.v')
| -rw-r--r-- | arm/Asmgenproof1.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 19edcd9d..658fc981 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -480,10 +480,10 @@ Lemma decompose_int_rec_or: forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n. Proof. induction N; intros; simpl. - destruct (Int.eq_dec n Int.zero); simpl. + predSpec Int.eq Int.eq_spec n Int.zero; simpl. subst n. rewrite Int.or_zero. auto. auto. - destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero. auto. simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib. rewrite Int.or_not_self. apply Int.and_mone. @@ -493,10 +493,10 @@ Lemma decompose_int_rec_xor: forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n. Proof. induction N; intros; simpl. - destruct (Int.eq_dec n Int.zero); simpl. + predSpec Int.eq Int.eq_spec n Int.zero; simpl. subst n. rewrite Int.xor_zero. auto. auto. - destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero. auto. simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib. rewrite Int.xor_not_self. apply Int.and_mone. @@ -506,10 +506,10 @@ Lemma decompose_int_rec_add: forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n. Proof. induction N; intros; simpl. - destruct (Int.eq_dec n Int.zero); simpl. + predSpec Int.eq Int.eq_spec n Int.zero; simpl. subst n. rewrite Int.add_zero. auto. auto. - destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero. auto. simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self. @@ -647,7 +647,7 @@ Lemma loadimm_correct: /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold loadimm. - destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))). + destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))). (* mov - orr* *) replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). apply iterate_op_correct. @@ -672,7 +672,7 @@ Lemma addimm_correct: /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold addimm. - destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))). + destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). (* add - add* *) replace (Val.add (rs r2) (Vint n)) with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)). |