diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:37:07 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2021-06-01 14:37:07 +0200 |
commit | 5a632954c85e8b2b5afea124e4fc83f39c5d3598 (patch) | |
tree | d53323083adec47d3338a04b516265c634806bea /common/Globalenvs.v | |
parent | a298e55fdc51cce92a8b39280643b623d7d991a8 (diff) | |
download | compcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.tar.gz compcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.zip |
[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml
Diffstat (limited to 'common/Globalenvs.v')
-rw-r--r-- | common/Globalenvs.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 40496044..4c9e7889 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -887,7 +888,7 @@ Qed. Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := forall p n, ofs <= p -> p + Z.of_nat n <= ofs + len -> - Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)). + Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n). Lemma store_zeros_loadbytes: forall m b p n m', @@ -901,8 +902,8 @@ Proof. + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia. rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia. - change (list_repeat (S n0) (Byte Byte.zero)) - with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). + change (List.repeat (Byte Byte.zero) (S n0)) + with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). eapply store_zeros_unchanged; eauto. intros; lia. @@ -924,11 +925,11 @@ Definition bytes_of_init_data (i: init_data): list memval := | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n)) | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) - | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero) + | Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n) | Init_addrof id ofs => match find_symbol ge id with | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs) - | None => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef + | None => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat) end end. @@ -1020,7 +1021,7 @@ Lemma store_zeros_read_as_zero: read_as_zero m' b p n. Proof. intros; red; intros. - transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). + transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))). apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. |