Update for addition of badBehaviorMap implicit for LLVM annotations.

See https://github.com/GaloisInc/crucible/pull/453
This commit is contained in:
Kevin Quick 2020-08-08 22:16:20 -07:00
parent cd4dd31343
commit ad46e191c6
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21

View File

@ -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