Member predicate AbstractValues :: BooleanValue :: branch
Holds if the s
branch out of cfe
is taken iff e
has this value.
predicate
branch
(
ControlFlowElement
cfe
,
ConditionalSuccessor
s
,
Expr
e
)