Java: Disregard heap parameter in any-argument and any-parameter specs.

This commit is contained in:
Anders Schack-Mulligen
2023-06-19 10:55:20 +02:00
parent 9a4de208ef
commit a23e77ca58
12 changed files with 90 additions and 18 deletions

View File

@@ -1222,14 +1222,18 @@ module Private {
node.asNode().(PostUpdateNode).getPreUpdateNode().(ArgNode).argumentOf(mid.asCall(), apos) and
parameterMatch(ppos, apos)
|
c = "Argument" or parseArg(c, ppos)
c = "Argument" and not heapParameter(ppos)
or
parseArg(c, ppos)
)
or
exists(ArgumentPosition apos, ParameterPosition ppos |
node.asNode().(ParamNode).isParameterOf(mid.asCallable(), ppos) and
parameterMatch(ppos, apos)
|
c = "Parameter" or parseParam(c, apos)
c = "Parameter" and not heapParameter(ppos)
or
parseParam(c, apos)
)
or
c = "ReturnValue" and
@@ -1259,7 +1263,9 @@ module Private {
node.asNode().(ArgNode).argumentOf(mid.asCall(), apos) and
parameterMatch(ppos, apos)
|
c = "Argument" or parseArg(c, ppos)
c = "Argument" and not heapParameter(ppos)
or
parseArg(c, ppos)
)
or
exists(ReturnNodeExt ret |

View File

@@ -319,6 +319,12 @@ predicate interpretInputSpecific(string c, InterpretNode mid, InterpretNode n) {
)
}
/**
* Holds if `pos` is the position of the `heap` parameter, and thus should not
* be included by models that specify "any argument" or "any parameter".
*/
predicate heapParameter(ParameterPosition pos) { pos = -2 }
/** Gets the argument position obtained by parsing `X` in `Parameter[X]`. */
bindingset[s]
ArgumentPosition parseParamBody(string s) {