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