- 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

1 files changed, 25 insertions, 0 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index ff6e9ae8..a79ea29c 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -18,6 +18,7 @@
     library. *)
 
 Require Export ZArith.
+Require Export Znumtheory.
 Require Export List.
 Require Export Bool.
 Require Import Wf_nat.
@@ -526,6 +527,25 @@ Proof.
   omega.
 Qed.
 
+(** Properties of divisibility. *)
+
+Lemma Zdivides_trans:
+  forall x y z, (x | y) -> (y | z) -> (x | z).
+Proof.
+  intros. inv H. inv H0. exists (q0 * q). ring.
+Qed.
+
+Definition Zdivide_dec:
+  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
+Proof.
+  intros. destruct (zeq (Zmod q p) 0).
+  left. exists (q / p). 
+  transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto.
+  transitivity (p * (q / p)). omega. ring.
+  right; red; intros. elim n. apply Z_div_exact_1; auto. 
+  inv H0. rewrite Z_div_mult; auto. ring.
+Qed.
+
 (** Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)
 
@@ -542,6 +562,11 @@ Proof.
   rewrite Zmult_comm. omega.
 Qed.
 
+Lemma align_divides: forall x y, y > 0 -> (y | align x y).
+Proof.
+  intros. unfold align. apply Zdivide_factor_l. 
+Qed.
+
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
 
 Set Implicit Arguments.