Sync files.

This commit is contained in:
Michael Nebel
2022-12-16 13:12:11 +01:00
parent 7422029e49
commit ea173f9516
5 changed files with 85 additions and 80 deletions

View File

@@ -241,15 +241,19 @@ module Public {
}
/**
* Holds if the summary is auto generated and not manually generated.
* Holds if the summaries that apply to `this` are auto generated and not manually generated.
*/
predicate isAutoGenerated() { none() }
final predicate isAutoGenerated() { this.hasProvenance("generated") and not this.isManual() }
/**
* Holds if the summary has the given provenance where `true` is
* `generated` and `false` is `manual`.
* Holds if there exists a manual summary that applies to `this`.
*/
predicate hasProvenance(boolean generated) { none() }
final predicate isManual() { this.hasProvenance("manual") }
/**
* Holds if there exists a summary that applies to `this` that has provenance `provenance`.
*/
predicate hasProvenance(string provenance) { none() }
}
/** A callable where there is no flow via the callable. */
@@ -259,13 +263,12 @@ module Public {
/**
* Holds if the neutral is auto generated.
*/
predicate isAutoGenerated() { neutralElement(this, true) }
predicate isAutoGenerated() { neutralElement(this, "generated") }
/**
* Holds if the neutral has the given provenance where `true` is
* `generated` and `false` is `manual`.
* Holds if the neutral has provenance `provenance`.
*/
predicate hasProvenance(boolean generated) { neutralElement(this, generated) }
predicate hasProvenance(string provenance) { neutralElement(this, provenance) }
}
}
@@ -997,12 +1000,12 @@ module Private {
private predicate relevantSummaryElementGenerated(
AccessPath inSpec, AccessPath outSpec, string kind
) {
summaryElement(this, inSpec, outSpec, kind, true) and
not summaryElement(this, _, _, _, false)
summaryElement(this, inSpec, outSpec, kind, "generated") and
not summaryElement(this, _, _, _, "manual")
}
private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {
summaryElement(this, inSpec, outSpec, kind, false)
summaryElement(this, inSpec, outSpec, kind, "manual")
or
this.relevantSummaryElementGenerated(inSpec, outSpec, kind)
}
@@ -1021,10 +1024,8 @@ module Private {
)
}
override predicate isAutoGenerated() { this.relevantSummaryElementGenerated(_, _, _) }
override predicate hasProvenance(boolean generated) {
summaryElement(this, _, _, _, generated)
override predicate hasProvenance(string provenance) {
summaryElement(this, _, _, _, provenance)
}
}