diff options
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: |