From ad46e191c60e4817f48d5c87894826d98d849697 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Sat, 8 Aug 2020 22:16:20 -0700 Subject: [PATCH] Update for addition of badBehaviorMap implicit for LLVM annotations. See https://github.com/GaloisInc/crucible/pull/453 --- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 07578d55..8d6f8181 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -117,6 +117,7 @@ import Control.Monad.IO.Class ( MonadIO, liftIO ) import qualified Data.BitVector.Sized as BV import qualified Data.ByteString as BS import qualified Data.Foldable as F +import Data.IORef ( newIORef ) import qualified Data.IntervalMap.Strict as IM import qualified Data.Parameterized.NatRepr as PN @@ -222,6 +223,8 @@ newGlobalMemory proxy sym endian mmc mem = do memImpl1 sizeBV CLD.noAlignment (symArray2, tbl) <- populateMemory proxy sym mmc mem symArray1 + bbmap <- liftIO $ newIORef mempty + let ?badBehaviorMap = bbmap memImpl3 <- liftIO $ CL.doArrayStore sym memImpl2 ptr CLD.noAlignment symArray2 sizeBV let ptrTable = MemPtrTable { memPtrTable = tbl, memPtr = ptr, memRepr = ?ptrWidth } @@ -479,6 +482,7 @@ mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do mapRegionPointers :: ( MC.MemWidth w , 16 <= w , CB.IsSymInterface sym + , CL.HasLLVMAnn sym ) => MemPtrTable sym w -> MS.GlobalMap sym CL.Mem w