aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cminorgenproof.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-12-29 12:47:56 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-12-29 12:47:56 +0000
commit12421d717405aa7964e437fc1167a23699b61ecc (patch)
tree99b975380440ad4e91074f918ee781ec6383f0ce /cfrontend/Cminorgenproof.v
parentdc4bed2cf06f46687225275131f411c86c773598 (diff)
downloadcompcert-12421d717405aa7964e437fc1167a23699b61ecc.tar.gz
compcert-12421d717405aa7964e437fc1167a23699b61ecc.zip
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
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
-rw-r--r--cfrontend/Cminorgenproof.v16
1 files changed, 8 insertions, 8 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9dfb5732..e1224bd1 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.