This bumps the `crucible` submodule to bring in the changes from
GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to
a handful of additional functions. This requires adding constraints to
some functions in `macaw-symbolic` to accommodate, as well as bumping the
`semmc` submodule to bring in analogous changes from GaloisInc/semmc#76.
This commit is contained in:
Ryan Scott 2022-06-09 10:57:52 -04:00 committed by Ryan Scott
parent 6a4f406c68
commit 2791b1050f
4 changed files with 7 additions and 5 deletions

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit 1d2d95d232eb2aae076d68021e1d75d322968595
Subproject commit 994b4f944630c561b9390f2a5f8d53d40f7318e5

2
deps/semmc vendored

@ -1 +1 @@
Subproject commit a3b8b89b9e88c94aab2ec6e06f993edcc9126cea
Subproject commit fd3568642e1ffc0c31dab172f4f430c3c009286c

View File

@ -34,4 +34,6 @@
- `addExtraBlock`
- `freshValueIndex`
- `Data.Macaw.Symbolic.Memory.newGlobalMemory` now has a `?memOpts :: MemOptions` constraint.
- The following functions now have a `?memOpts :: MemOptions` constraint:
- `Data.Macaw.Symbolic.Memory.newGlobalMemory`
- `Data.Macaw.Symbolic.MemOps.{doWriteMem,doCondWriteMem}`

View File

@ -1073,7 +1073,7 @@ doCondReadMem bak mem ptrWidth memRep cond ptr def = hasPtrClass ptrWidth $
-- arg5 : Address to write to
-- arg6 : Value to write
doWriteMem ::
(IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
(IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
bak ->
MemImpl sym ->
M.AddrWidthRepr ptrW ->
@ -1104,7 +1104,7 @@ doWriteMem bak mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $
-- arg6 : Address to write to
-- arg7 : Value to write
doCondWriteMem ::
(IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
(IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
bak ->
MemImpl sym ->
M.AddrWidthRepr ptrW ->