Dataflow: qldoc fix.

This commit is contained in:
Anders Schack-Mulligen
2021-06-01 10:49:47 +02:00
parent 4f9a6c151b
commit 5d21c64247
24 changed files with 72 additions and 24 deletions

View File

@@ -532,7 +532,9 @@ private module Stage1 {
}
/**
* Holds if an output from `call` is reached in the flow covered by `revFlow`.
* Holds if an output from `call` is reached in the flow covered by `revFlow`
* and data might flow through the target callable resulting in reverse flow
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn, Configuration config) {

View File

@@ -532,7 +532,9 @@ private module Stage1 {
}
/**
* Holds if an output from `call` is reached in the flow covered by `revFlow`.
* Holds if an output from `call` is reached in the flow covered by `revFlow`
* and data might flow through the target callable resulting in reverse flow
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn, Configuration config) {

View File

@@ -532,7 +532,9 @@ private module Stage1 {
}
/**
* Holds if an output from `call` is reached in the flow covered by `revFlow`.
* Holds if an output from `call` is reached in the flow covered by `revFlow`
* and data might flow through the target callable resulting in reverse flow
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn, Configuration config) {

View File

@@ -532,7 +532,9 @@ private module Stage1 {
}
/**
* Holds if an output from `call` is reached in the flow covered by `revFlow`.
* Holds if an output from `call` is reached in the flow covered by `revFlow`
* and data might flow through the target callable resulting in reverse flow
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn, Configuration config) {

View File

@@ -532,7 +532,9 @@ private module Stage1 {
}
/**
* Holds if an output from `call` is reached in the flow covered by `revFlow`.
* Holds if an output from `call` is reached in the flow covered by `revFlow`
* and data might flow through the target callable resulting in reverse flow
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn, Configuration config) {