From ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 19 Nov 2009 13:32:09 +0000 Subject: Revised lib/Integers.v to make it parametric w.r.t. word size. Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/ConstpropOpproof.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'arm/ConstpropOpproof.v') diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index bb9caffb..b718fc26 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -130,13 +130,13 @@ Proof. replace n2 with i0. destruct (Int.eq i0 Int.zero). discriminate. injection H0; intro; subst v. simpl. congruence. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. @@ -284,7 +284,7 @@ Proof. with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H2). - change (Z_of_nat wordsize) with 32. intro. rewrite H3. + change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3. destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H2). auto. simpl List.map. rewrite H. auto. Qed. @@ -400,7 +400,7 @@ Proof. with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). apply make_shruimm_correct. simpl. destruct rs#r1; auto. - change 32 with (Z_of_nat wordsize). + change 32 with (Z_of_nat Int.wordsize). rewrite (Int.is_power2_range _ _ H0). generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros. subst i. discriminate. @@ -474,19 +474,19 @@ Proof. assumption. (* Oshl *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shlimm_correct. assumption. assumption. (* Oshr *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shrimm_correct. assumption. assumption. (* Oshru *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shruimm_correct. assumption. assumption. -- cgit