Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.

lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.


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

2 files changed, 12 insertions, 12 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9dfb573..e1224bd 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -962,16 +962,16 @@ Lemma make_cast_correct:
 Proof.
   intros. destruct chunk; simpl make_cast.
 
-  exists (Val.cast8signed tv). 
+  exists (Val.sign_ext 8 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast8unsigned tv). 
+  exists (Val.zero_ext 8 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast16signed tv). 
+  exists (Val.sign_ext 16 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast16unsigned tv). 
+  exists (Val.zero_ext 16 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
   exists tv.
@@ -1025,10 +1025,10 @@ Proof.
   inv H; simpl in H6; inv H6;
   econstructor; (split; [eauto|idtac]);
   destruct v1; simpl in H0; inv H0; try (constructor; constructor).
-  apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem.
-  apply val_content_inject_8; auto. apply Int.cast8_unsigned_signed. 
-  apply val_content_inject_16; auto. apply Int.cast16_unsigned_idem. 
-  apply val_content_inject_16; auto. apply Int.cast16_unsigned_signed. 
+  apply val_content_inject_8. auto. apply Int.zero_ext_idem. compute; auto.
+  apply val_content_inject_8; auto. apply Int.zero_ext_sign_ext. compute; auto.
+  apply val_content_inject_16; auto. apply Int.zero_ext_idem. compute; auto.
+  apply val_content_inject_16; auto. apply Int.zero_ext_sign_ext. compute; auto.
   apply val_content_inject_32. apply Float.singleoffloat_idem. 
 Qed.
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 2213912..14b8053 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -351,10 +351,10 @@ Definition sem_binary_operation
 
 Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   match sz, sg with
-  | I8, Signed => Int.cast8signed i
-  | I8, Unsigned => Int.cast8unsigned i
-  | I16, Signed => Int.cast16signed i
-  | I16, Unsigned => Int.cast16unsigned i 
+  | I8, Signed => Int.sign_ext 8 i
+  | I8, Unsigned => Int.zero_ext 8 i
+  | I16, Signed => Int.sign_ext 16 i
+  | I16, Unsigned => Int.zero_ext 16 i 
   | I32 , _ => i
   end.