mirror of
https://github.com/github/codeql.git
synced 2025-12-21 19:26:31 +01:00
Dataflow: Sync.
This commit is contained in:
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
|
|||||||
/**
|
/**
|
||||||
* Gets the number of `AccessPath`s that correspond to `apa`.
|
* Gets the number of `AccessPath`s that correspond to `apa`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countAps(AccessPathApprox apa, Configuration config) {
|
private int countAps(AccessPathApprox apa, Configuration config) {
|
||||||
evalUnfold(apa, false, config) and
|
evalUnfold(apa, false, config) and
|
||||||
result = 1 and
|
result = 1 and
|
||||||
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
|
|||||||
* that it is expanded to a precise head-tail representation.
|
* that it is expanded to a precise head-tail representation.
|
||||||
*/
|
*/
|
||||||
language[monotonicAggregates]
|
language[monotonicAggregates]
|
||||||
|
pragma[assume_small_delta]
|
||||||
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
private int countPotentialAps(AccessPathApprox apa, Configuration config) {
|
||||||
apa instanceof AccessPathApproxNil and result = 1
|
apa instanceof AccessPathApproxNil and result = 1
|
||||||
or
|
or
|
||||||
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
|
|||||||
}
|
}
|
||||||
|
|
||||||
private newtype TPathNode =
|
private newtype TPathNode =
|
||||||
|
pragma[assume_small_delta]
|
||||||
TPathNodeMid(
|
TPathNodeMid(
|
||||||
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config
|
||||||
) {
|
) {
|
||||||
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
|
|
||||||
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
override AccessPathFrontHead getFront() { result = TFrontHead(head) }
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override AccessPathApproxCons getApprox() {
|
override AccessPathApproxCons getApprox() {
|
||||||
result = TConsNil(head, tail.(AccessPathNil).getType())
|
result = TConsNil(head, tail.(AccessPathNil).getType())
|
||||||
or
|
or
|
||||||
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
|
|||||||
result = TCons1(head, this.length())
|
result = TCons1(head, this.length())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
override int length() { result = 1 + tail.length() }
|
override int length() { result = 1 + tail.length() }
|
||||||
|
|
||||||
private string toStringImpl(boolean needsSuffix) {
|
private string toStringImpl(boolean needsSuffix) {
|
||||||
@@ -3155,6 +3160,7 @@ private predicate pathNode(
|
|||||||
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
* Holds if data may flow from `mid` to `node`. The last step in or out of
|
||||||
* a callable is recorded by `cc`.
|
* a callable is recorded by `cc`.
|
||||||
*/
|
*/
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate pathStep(
|
private predicate pathStep(
|
||||||
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap
|
||||||
|
|||||||
Reference in New Issue
Block a user