Back from Oregon commit.

powerpc/*: better compilation of some comparisons; revised asmgenproof1.
common/*: added Mem.storebytes; used to give semantics to memcpy builtin.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 24 insertions, 0 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 4fc922b..f4d50e8 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -606,6 +606,13 @@ Definition nat_of_Z (z: Z) : nat :=
   | Zneg p => O
   end.
 
+Lemma nat_of_Z_of_nat:
+  forall n, nat_of_Z (Z_of_nat n) = n.
+Proof.
+  intros. unfold Z_of_nat. destruct n. auto.
+  simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto.
+Qed.
+
 Lemma nat_of_Z_max:
   forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.
 Proof.
@@ -1133,6 +1140,13 @@ Proof.
   induction 1; intros; simpl. auto. constructor; auto. 
 Qed.
 
+Lemma list_forall2_length:
+  forall l1 l2,
+  list_forall2 l1 l2 -> length l1 = length l2.
+Proof.
+  induction 1; simpl; congruence.
+Qed.
+
 End FORALL2.
 
 Lemma list_forall2_imply:
diff --git a/lib/Integers.v b/lib/Integers.v
index 30f692a..6e7a6cb 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -167,6 +167,11 @@ Definition divu (x y: int) : int :=
 Definition modu (x y: int) : int :=
   repr (Zmod (unsigned x) (unsigned y)).
 
+Definition add_carry (x y cin: int): int :=
+  if zlt (unsigned x + unsigned y + unsigned cin) modulus
+  then zero
+  else one.
+
 (** For bitwise operations, we need to convert between Coq integers [Z]
   and their bit-level representations.  Bit-level representations are
   represented as characteristic functions, that is, functions [f]
@@ -746,6 +751,11 @@ Proof.
   rewrite Zplus_0_r. apply repr_unsigned.
 Qed.
 
+Theorem add_zero_l: forall x, add zero x = x.
+Proof.
+  intros. rewrite add_commut. apply add_zero.
+Qed.
+
 Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
 Proof.
   intros; unfold add.