From f440208c6b6159fd83dd6c365e194fe39b30d794 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 18 Jul 2015 16:09:30 +0200 Subject: Missing cases in ValueDomain.vnormalize, causing overapproximation. --- backend/ValueDomain.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/ValueDomain.v') 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. -- cgit