diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 16:09:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 16:09:30 +0200 |
| commit | f440208c6b6159fd83dd6c365e194fe39b30d794 (patch) | |
| tree | 283cf408af9a0106b160094e78a46b497f700038 /backend/ValueDomain.v | |
| parent | c85b6a585073f3fc7c8e34fbd78c613bf619cbeb (diff) | |
| download | compcert-kvx-f440208c6b6159fd83dd6c365e194fe39b30d794.tar.gz compcert-kvx-f440208c6b6159fd83dd6c365e194fe39b30d794.zip | |
Missing cases in ValueDomain.vnormalize, causing overapproximation.
Diffstat (limited to 'backend/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 0de17745..dbdc6352 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2267,12 +2267,12 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) := | Mint16unsigned, I i => I (Int.zero_ext 16 i) | Mint16unsigned, Uns n => Uns (Z.min n 16) | Mint16unsigned, _ => Uns 16 - | Mint32, (I _ | Ptr _ | Ifptr _) => v + | Mint32, (I _ | Uns _ | Sgn _ | Ptr _ | Ifptr _) => v | Mint64, L _ => v | Mint64, (Ptr p | Ifptr p) => Ifptr (if va_strict tt then Pbot else p) | Mfloat32, FS f => v | Mfloat64, F f => v - | Many32, (I _ | Ptr _ | Ifptr _ | FS _) => v + | Many32, (I _ | Uns _ | Sgn _ | Ptr _ | Ifptr _ | FS _) => v | Many64, _ => v | _, _ => Ifptr Pbot end. |