Java: refactor isManuallyGenerated and isBothAutoAndManuallyGenerated

This commit is contained in:
Jami Cogswell
2022-12-09 18:37:50 -05:00
parent 0b2f2a3f88
commit 6854845b75
6 changed files with 36 additions and 96 deletions

View File

@@ -1001,20 +1001,6 @@ module Private {
not summaryElement(this, _, _, _, false)
}
private predicate relevantSummaryElementManual(
AccessPath inSpec, AccessPath outSpec, string kind
) {
summaryElement(this, inSpec, outSpec, kind, false) and
not summaryElement(this, _, _, _, true)
}
private predicate relevantSummaryElementBothGeneratedAndManual(
AccessPath inSpec, AccessPath outSpec, string kind
) {
summaryElement(this, inSpec, outSpec, kind, true) and
summaryElement(this, inSpec, outSpec, kind, false)
}
private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {
summaryElement(this, inSpec, outSpec, kind, false)
or
@@ -1037,10 +1023,14 @@ module Private {
override predicate isAutoGenerated() { this.relevantSummaryElementGenerated(_, _, _) }
override predicate isManuallyGenerated() { this.relevantSummaryElementManual(_, _, _) }
override predicate isManuallyGenerated() {
summaryElement(this, _, _, _, false) and
not summaryElement(this, _, _, _, true)
}
override predicate isBothAutoAndManuallyGenerated() {
this.relevantSummaryElementBothGeneratedAndManual(_, _, _)
summaryElement(this, _, _, _, true) and
summaryElement(this, _, _, _, false)
}
}