diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-05 14:05:34 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-05 14:05:34 +0200 |
| commit | 028aaefc44b8ed8bafd8b8896fedb53f6e68df3c (patch) | |
| tree | d7f9325da52050a64e5c9ced1017a4f57c674ff3 /common/Globalenvs.v | |
| parent | 4ac759d0bceef49d16197e3bb8c9767ece693c5e (diff) | |
| download | compcert-kvx-028aaefc44b8ed8bafd8b8896fedb53f6e68df3c.tar.gz compcert-kvx-028aaefc44b8ed8bafd8b8896fedb53f6e68df3c.zip | |
Implement support for big endian arm targets.
Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418
Diffstat (limited to 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a8d0512c..2a8d6d97 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -864,11 +864,12 @@ Proof. with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). - eapply store_zeros_unchanged; eauto. intros; omega. + eapply store_zeros_unchanged; eauto. intros; omega. intros; omega. - change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). + replace (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). change 1 with (size_chunk Mint8unsigned). eapply Mem.loadbytes_store_same; eauto. + unfold encode_val; unfold encode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. eapply IHo; eauto. omega. omega. omega. omega. + eapply IHo; eauto. omega. omega. - discriminate. @@ -973,7 +974,7 @@ Proof. transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. - f_equal. destruct chunk; reflexivity. + f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. Qed. Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop := |