Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion

6 files changed, 9 insertions, 10 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 0f2e3674..37527940 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -109,7 +109,7 @@ let atom_location a =
 
 let comp_env : composite_env ref = ref Maps.PTree.empty
 
-(** Hooks -- overriden in machine-dependent CPragmas module *)
+(** Hooks -- overridden in machine-dependent CPragmas module *)
 
 let process_pragma_hook = ref (fun (_: string) -> false)
 
@@ -703,12 +703,12 @@ let z_of_str hex str fst =
 
 let checkFloatOverflow f typ =
   match f with
-  | Fappli_IEEE.B754_finite _ -> ()
-  | Fappli_IEEE.B754_zero _ ->
+  | Binary.B754_finite _ -> ()
+  | Binary.B754_zero _ ->
       warning Diagnostics.Literal_range "magnitude of floating-point constant too small for type '%s'"  typ
-  | Fappli_IEEE.B754_infinity _ ->
+  | Binary.B754_infinity _ ->
       warning Diagnostics.Literal_range "magnitude of floating-point constant too large for type '%s'"  typ
-  | Fappli_IEEE.B754_nan _ ->
+  | Binary.B754_nan _ ->
       warning Diagnostics.Literal_range "floating-point converts converts to 'NaN'"
 
 let convertFloat f kind =
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 823d2542..7f5fe355 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -292,7 +292,6 @@ Remark check_assign_copy:
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
 Proof with try (right; intuition omega).
   intros. unfold assign_copy_ok.
-  assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto...
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto...
   assert (Y: {b' <> b \/
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 7a4c49a2..8ab29fe9 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -84,7 +84,7 @@ Definition typeof (e: expr) : type :=
 (** ** Statements *)
 
 (** Clight statements are similar to those of Compcert C, with the addition
-  of assigment (of a rvalue to a lvalue), assignment to a temporary,
+  of assignment (of a rvalue to a lvalue), assignment to a temporary,
   and function call (with assignment of the result to a temporary).
   The three C loops are replaced by a single infinite loop [Sloop s1
   s2] that executes [s1] then [s2] repeatedly.  A [continue] in [s1]
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ffafc5d2..5acb996d 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -923,7 +923,7 @@ Remark inj_offset_aligned_block:
   Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz.
 Proof.
   intros; red; intros.
-  apply Zdivides_trans with (block_alignment sz).
+  apply Z.divide_trans with (block_alignment sz).
   unfold align_chunk.  unfold block_alignment.
   generalize Z.divide_1_l; intro.
   generalize Z.divide_refl; intro.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 914328be..00565309 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -41,7 +41,7 @@ Inductive expr : Type :=
                                            (**r binary arithmetic operation *)
   | Ecast (r: expr) (ty: type)                        (**r type cast [(ty)r] *)
   | Eseqand (r1 r2: expr) (ty: type)       (**r sequential "and" [r1 && r2] *)
-  | Eseqor (r1 r2: expr) (ty: type)        (**r sequential "or" [r1 && r2] *)
+  | Eseqor (r1 r2: expr) (ty: type)        (**r sequential "or" [r1 || r2] *)
   | Econdition (r1 r2 r3: expr) (ty: type)  (**r conditional [r1 ? r2 : r3] *)
   | Esizeof (ty': type) (ty: type)                      (**r size of a type *)
   | Ealignof (ty': type) (ty: type)        (**r natural alignment of a type *)
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 26d3d347..2dd34389 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1055,7 +1055,7 @@ Proof.
   assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
     replace (sizeof tge ty) with (Z.of_nat (List.length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply nat_of_Z_eq. omega.
+    rewrite LEN. apply Z2Nat.id. omega.
   assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
   assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty).