aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-17 14:36:18 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-17 14:36:18 +0000
commitc29871c2d5c7860c6c6c53e8d5c8a9fe434742d2 (patch)
tree9e002b414d3fb3a899deb43f9f6e14d02507121a /powerpc/Asmgenproof.v
parent26bb5772c75efe1e4617fb9c4f2b8522989fac6d (diff)
downloadcompcert-c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2.tar.gz
compcert-c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2.zip
powerpc/: new unary operation "addsymbol"
Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenproof.v')
-rw-r--r--powerpc/Asmgenproof.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 869fab3d..990d35d2 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -243,6 +243,8 @@ Opaque Int.eq.
unfold transl_op; intros; destruct op; TailNoLabel.
destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
destruct (symbol_is_small_data i i0); TailNoLabel.
+ destruct (symbol_is_small_data i i0); TailNoLabel.
+ destruct (symbol_is_rel_data i i0); TailNoLabel.
destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
eapply transl_cond_op_label; eauto.
@@ -259,6 +261,8 @@ Proof.
unfold transl_memory_access; intros; destruct addr; TailNoLabel.
destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
destruct (symbol_is_small_data i i0); TailNoLabel.
+ destruct (symbol_is_small_data i i0); TailNoLabel.
+ destruct (symbol_is_rel_data i i0); TailNoLabel.
destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
Qed.