macaw-symbolic: Fix interval bounds in mkGlobalPointerValidityPred

Fixes #279.
GaloisInc · Jan 24, 2024 · 7e1694b · 7e1694b
1 parent c6c48b6
commit 7e1694b
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory/Common.hs b/symbolic/src/Data/Macaw/Symbolic/Memory/Common.hs
@@ -136,26 +136,26 @@ mkGlobalPointerValidityPredCommon tbl = \sym puse mcond ptr -> do
             IM.IntervalCO lo hi -> do
               lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
               hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
-              lob <- WI.bvUlt sym lobv off
-              hib <- WI.bvUle sym off hibv
+              lob <- WI.bvUle sym lobv off
+              hib <- WI.bvUlt sym off hibv
               WI.andPred sym lob hib
             IM.ClosedInterval lo hi -> do
               lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
               hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
-              lob <- WI.bvUlt sym lobv off
-              hib <- WI.bvUlt sym off hibv
+              lob <- WI.bvUle sym lobv off
+              hib <- WI.bvUle sym off hibv
               WI.andPred sym lob hib
             IM.OpenInterval lo hi -> do
               lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
               hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
-              lob <- WI.bvUle sym lobv off
-              hib <- WI.bvUle sym off hibv
+              lob <- WI.bvUlt sym lobv off
+              hib <- WI.bvUlt sym off hibv
               WI.andPred sym lob hib
             IM.IntervalOC lo hi -> do
               lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo))
               hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi))
-              lob <- WI.bvUle sym lobv off
-              hib <- WI.bvUlt sym off hibv
+              lob <- WI.bvUlt sym lobv off
+              hib <- WI.bvUle sym off hibv
               WI.andPred sym lob hib
 
   let mkPred off = do