diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 11:33:38 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 11:33:38 +0000 |
| commit | 2eee425909832e0501e088feaa1fbc8573e877b0 (patch) | |
| tree | 1b4b82b9260b26b30739d026af4fd39e8581eaee /common | |
| parent | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (diff) | |
Update "read_as_zeros" property.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2538 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
| -rw-r--r-- | common/Globalenvs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a34a05d..e4772e2 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -761,7 +761,9 @@ Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop := Some (match chunk with | Mint8unsigned | Mint8signed | Mint16unsigned | Mint16signed | Mint32 => Vint Int.zero | Mint64 => Vlong Int64.zero - | Mfloat32 | Mfloat64 => Vfloat Float.zero + | Mfloat32 => Vsingle Float32.zero + | Mfloat64 => Vfloat Float.zero + | Many32 | Many64 => Vundef end). Remark store_zeros_loadbytes: |