From 2eee425909832e0501e088feaa1fbc8573e877b0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 11:33:38 +0000 Subject: Update "read_as_zeros" property. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2538 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'common') 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: -- cgit v1.2.3