Merge pull request #12556 from michaelnebel/java/argumentthis

Java: Argument[-1] -> Argument[this]
This commit is contained in:
Michael Nebel
2023-03-20 15:59:59 +01:00
committed by GitHub
194 changed files with 7682 additions and 7584 deletions

View File

@@ -39,7 +39,7 @@
* "Argument[n]", "Argument[n1..n2]", or "ReturnValue":
* - "": Selects a write to the selected element in case this is a field or property.
* - "Argument[n]": Selects an argument in a call to the selected element.
* The arguments are zero-indexed, and `-1` specifies the qualifier.
* The arguments are zero-indexed, and `this` specifies the qualifier.
* - "Argument[n1..n2]": Similar to "Argument[n]" but select any argument in
* the given range. The range is inclusive at both ends.
* - "ReturnValue": Selects a value being returned by the selected element.
@@ -50,14 +50,14 @@
* - "": Selects a read of a selected field, property, or parameter.
* - "Argument[n]": Selects the post-update value of an argument in a call to the
* selected element. That is, the value of the argument after the call returns.
* The arguments are zero-indexed, and `-1` specifies the qualifier.
* The arguments are zero-indexed, and `this` specifies the qualifier.
* - "Argument[n1..n2]": Similar to "Argument[n]" but select any argument in
* the given range. The range is inclusive at both ends.
* - "Parameter": Selects the value of a parameter of the selected element.
* "Parameter" is also allowed in case the selected element is already a
* parameter itself.
* - "Parameter[n]": Similar to "Parameter" but restricted to a specific
* numbered parameter (zero-indexed, and `-1` specifies the value of `this`).
* numbered parameter (zero-indexed, and `this` specifies the value of `this`).
* - "Parameter[n1..n2]": Similar to "Parameter[n]" but selects any parameter
* in the given range. The range is inclusive at both ends.
* - "ReturnValue": Selects the return value of a call to the selected element.
@@ -173,6 +173,8 @@ module ModelValidation {
or
part = input.getToken(_) and
parseParam(part, _)
or
invalidIndexComponent(input, part)
) and
result = "Unrecognized input specification \"" + part + "\" in " + pred + " model."
)
@@ -184,9 +186,13 @@ module ModelValidation {
or
summaryModel(_, _, _, _, _, _, _, output, _, _) and pred = "summary"
|
invalidSpecComponent(output, part) and
not part = "" and
not (part = ["Argument", "Parameter"] and pred = "source") and
(
invalidSpecComponent(output, part) and
not part = "" and
not (part = ["Argument", "Parameter"] and pred = "source")
or
invalidIndexComponent(output, part)
) and
result = "Unrecognized output specification \"" + part + "\" in " + pred + " model."
)
}

View File

@@ -1050,6 +1050,16 @@ module Private {
not exists(interpretComponent(c))
}
/**
* Holds if token `part` of specification `spec` has an invalid index.
* E.g., `Argument[-1]`.
*/
predicate invalidIndexComponent(AccessPath spec, AccessPathToken part) {
part = spec.getToken(_) and
part.getName() = ["Parameter", "Argument"] and
AccessPath::parseInt(part.getArgumentList()) < 0
}
private predicate inputNeedsReference(AccessPathToken c) {
c.getName() = "Argument" or
inputNeedsReferenceSpecific(c)