mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-26 09:22:20 +03:00
Use pointer addition, only when the value is not a bit-vector.
The other version was getting confusing by the NULL pointer.
This commit is contained in:
parent
4fa262a14c
commit
32710829f6
@ -135,12 +135,12 @@ doPtrAdd = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
|
|||||||
, ptr_bits ~>
|
, ptr_bits ~>
|
||||||
do r <- ptrAdd sym w x (asBits y)
|
do r <- ptrAdd sym w x (asBits y)
|
||||||
ok <- let ?ptrWidth = w in isValidPointer sym r mem
|
ok <- let ?ptrWidth = w in isValidPointer sym r mem
|
||||||
endCaseCheck ok "Invalid result" r
|
endCaseCheck ok "Invalid result (ptr_bits)" r
|
||||||
|
|
||||||
, bits_ptr ~>
|
, bits_ptr ~>
|
||||||
do r <- ptrAdd sym w y (asBits x)
|
do r <- ptrAdd sym w y (asBits x)
|
||||||
ok <- let ?ptrWidth = w in isValidPointer sym r mem
|
ok <- let ?ptrWidth = w in isValidPointer sym r mem
|
||||||
endCaseCheck ok "Invalid result" r
|
endCaseCheck ok "Invalid result (bits_ptr)" r
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|
||||||
@ -345,10 +345,13 @@ ptrOp k st mvar w x0 y0 =
|
|||||||
let sym = stateSymInterface st
|
let sym = stateSymInterface st
|
||||||
x = regValue x0
|
x = regValue x0
|
||||||
y = regValue y0
|
y = regValue y0
|
||||||
xPtr <- let ?ptrWidth = w in isValidPointer sym x mem
|
-- xPtr <- let ?ptrWidth = w in isValidPointer sym x mem
|
||||||
yPtr <- let ?ptrWidth = w in isValidPointer sym y mem
|
-- yPtr <- let ?ptrWidth = w in isValidPointer sym y mem
|
||||||
xBits <- isBitVec sym x
|
xBits <- isBitVec sym x
|
||||||
yBits <- isBitVec sym y
|
yBits <- isBitVec sym y
|
||||||
|
|
||||||
|
xPtr <- notPred sym xBits
|
||||||
|
yPtr <- notPred sym yBits
|
||||||
a <- k sym mem w xPtr xBits yPtr yBits x y
|
a <- k sym mem w xPtr xBits yPtr yBits x y
|
||||||
return (a,st)
|
return (a,st)
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user