Dataflow: Add missing qldoc and sync.

This commit is contained in:
Anders Schack-Mulligen
2020-11-03 09:21:48 +01:00
parent 7eb64aa998
commit 2971784f9c
23 changed files with 748 additions and 70 deletions

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

View File

@@ -3231,8 +3231,10 @@ private module FlowExploration {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}