mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 00:59:09 +03:00
minor improvement to jump bounds abstract interpretation
This commit is contained in:
parent
024e393e8e
commit
e3d7c26b8c
@ -170,6 +170,7 @@ assertPred (AssignedValue a) isTrue bnds =
|
|||||||
EvalApp (AndApp l r) | isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
|
EvalApp (AndApp l r) | isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
|
||||||
-- Given not (x || y), assert not x, then assert not y
|
-- Given not (x || y), assert not x, then assert not y
|
||||||
EvalApp (OrApp l r) | not isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
|
EvalApp (OrApp l r) | not isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
|
||||||
|
EvalApp (NotApp p) -> assertPred p (not isTrue) bnds
|
||||||
_ -> Right bnds
|
_ -> Right bnds
|
||||||
assertPred _ _ bnds = Right bnds
|
assertPred _ _ bnds = Right bnds
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user