DataFlow: Introduce 'revSinkNode'.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-04 11:09:08 +02:00
parent 50f5c4d5f6
commit 981f67531c

View File

@@ -4003,13 +4003,22 @@ module MakeImpl<DataFlowParameter Lang> {
private predicate relevantState(FlowState state) {
sourceNode(_, state) or
sinkNodeWithState(_, state) or
revSinkNode(_, state) or
additionalLocalStateStep(_, state, _, _) or
additionalLocalStateStep(_, _, _, state) or
additionalJumpStateStep(_, state, _, _) or
additionalJumpStateStep(_, _, _, state)
}
private predicate revSinkNode(NodeEx node, FlowState state) {
sinkNodeWithState(node, state)
or
Config::isSink(node.asNode()) and
relevantState(state) and
not fullBarrier(node) and
not stateBarrier(node, state)
}
private newtype TSummaryCtx1 =
TSummaryCtx1None() or
TSummaryCtx1Param(ParamNodeEx p)