diff --git a/deps/crucible b/deps/crucible index f7fa4d20..f7a994dd 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit f7fa4d20ce1248861a41b4e758b49ea9cbc99fdc +Subproject commit f7a994dd0cddfdf4bdbe5590a8e345e8e69926d6 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index bea158b7..24dc69a4 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit bea158b759d7315cdb4f4c4a364c9fd2c2f9b5a4 +Subproject commit 24dc69a4e718193d65874d84466a7daecf8d8356 diff --git a/deps/semmc b/deps/semmc index 87782b4d..5acea2bd 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 87782b4d9f21ec24b576170bd0892cdee11a89bc +Subproject commit 5acea2bdc757d2aabf3b167abb78a701a2427360 diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs index 412692cf..4b129a5d 100644 --- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs +++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs @@ -508,6 +508,7 @@ initializeMemory :: forall arch sym m proxy , CB.IsSymInterface sym , LLVM.HasLLVMAnn sym , MonadIO m + , ?memOpts :: LLVM.MemOptions ) => proxy arch -> sym diff --git a/symbolic/ChangeLog.md b/symbolic/ChangeLog.md index b189998a..07efa9f3 100644 --- a/symbolic/ChangeLog.md +++ b/symbolic/ChangeLog.md @@ -19,3 +19,5 @@ - `setMachineRegs` - `addExtraBlock` - `freshValueIndex` + +- `Data.Macaw.Symbolic.Memory.newGlobalMemory` now has a `?memOpts :: MemOptions` constraint. diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index a7f79ad9..f7b69847 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -197,6 +197,7 @@ newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch , CB.IsSymInterface sym , CL.HasLLVMAnn sym , MonadIO m + , ?memOpts :: CL.MemOptions ) => proxy arch -- ^ A proxy to fix the architecture