diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
commit | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch) | |
tree | 3efa5cb51e9bb3edc935f42dbd630fce9a170804 /lib/Integers.v | |
parent | cd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff) |
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of
comparisons, so that evaluation of expressions is independent of
memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index a9644bc..ff29d2a 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2252,59 +2252,6 @@ Proof. rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p. decEq. omega. omega. omega. Qed. -(* -Lemma zero_ext_charact: - forall x y, - zero_ext n x = y <-> - 0 <= unsigned y < two_p n /\ eqmod (two_p n) (unsigned x) (unsigned y). -Proof. - intros. unfold zero_ext. set (x' := unsigned x). split; intros. - subst y. - assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos. - rewrite unsigned_repr. split. auto. - apply eqmod_mod. apply two_p_n_pos. - generalize two_p_n_range. omega. - destruct H. destruct H0 as [k EQ]. - assert (x' mod two_p n = unsigned y). - apply Zmod_unique with k; auto. - rewrite H0. apply repr_unsigned. -Qed. - -Lemma sign_ext_charact: - forall x y, - sign_ext n x = y <-> - -(two_p (n-1)) <= signed y < two_p (n-1) - /\ eqmod (two_p n) (unsigned x) (signed y). -Proof. - intros. unfold sign_ext. set (x' := unsigned x). split; intros. - assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos. - destruct (zlt (x' mod two_p n) (two_p (n - 1))); subst y. - rewrite signed_repr. split. omega. - apply eqmod_mod. apply two_p_n_pos. - assert (min_signed < 0). vm_compute; auto. - generalize two_p_n_range'. omega. - rewrite signed_repr. split. - assert (two_p n = 2 * two_p (n-1)). rewrite <- two_p_S. decEq. omega. omega. - omega. - apply eqmod_trans with (x' - 0). apply eqmod_refl2. omega. - apply eqmod_sub. apply eqmod_mod. apply two_p_n_pos. - exists (-1). ring. - split. generalize two_p_n_range'. - change (max_signed + 1) with (- min_signed). omega. - generalize two_p_n_range'. omega. - - destruct H. destruct H0 as [k EQ]. - assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega. - assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1. - assert (x' mod two_p n = signed y). - apply Zmod_unique with k; auto. omega. - rewrite zlt_true. rewrite H2. apply repr_signed. omega. - assert (x' mod two_p n = signed y + two_p n). - apply Zmod_unique with (k-1). rewrite EQ. ring. omega. - rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed. - omega. -Qed. -*) Lemma sign_ext_charact: forall x y, |