Shared: Move shared logic into FlowSummaryImpl.qll

This commit is contained in:
Tom Hvitved
2024-11-27 14:50:46 +01:00
parent 395901b8e0
commit fbeb6f3940
5 changed files with 16 additions and 20 deletions

View File

@@ -1207,6 +1207,11 @@ module Make<
)
}
/** Holds if the value of `succ` is uniquely determined by the value of `pred`. */
predicate summaryLocalMustFlowStep(SummaryNode pred, SummaryNode succ) {
pred = unique(SummaryNode n1 | summaryLocalStep(n1, succ, true, _))
}
/**
* Holds if there is a read step of content `c` from `pred` to `succ`, which
* is synthesized from a flow summary.