GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

Add support for forcing allocation of fresh bits (as opposed to pointer/bits)

Browse Source
This commit is contained in:
Iavor Diatchki 2018-03-22 13:11:22 -07:00
parent cf34388d41
commit 79a4cdf39e
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -350,13 +350,13 @@ freshValue ::
(IsSymInterface sym, 1 <= ptrW) =>
sym ->
String {- ^ Name for fresh value -} ->
NatRepr ptrW {- ^ Width of pointers -} ->
Maybe (NatRepr ptrW) {- ^ Width of pointers; if nothing, allocate as bits -} ->
M.TypeRepr tp {- ^ Type of value -} ->
IO (C.RegValue sym (ToCrucibleType tp))
freshValue sym str w ty =
case ty of
M.BVTypeRepr y ->
case testEquality y w of
case testEquality y =<< w of
Just Refl ->
do nm_base <- symName (str ++ "_base")

2
x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View File

@ -171,7 +171,7 @@ updateX86Reg r upd asgn =
freshX86Reg :: C.IsSymInterface sym =>
sym -> M.X86Reg t -> IO (RegValue' sym (ToCrucibleType t))
freshX86Reg sym r =
RV <$> freshValue sym (show r) (C.knownNat @64) (M.typeRepr r)
RV <$> freshValue sym (show r) (Just (C.knownNat @64)) (M.typeRepr r)
------------------------------------------------------------------------