Java: add hasProvenance predicate, remove isManuallyGenerated and isBothAutoAndManuallyGenerated

This commit is contained in:
Jami Cogswell
2022-12-12 11:23:46 -05:00
parent 270e38d753
commit 623068c4b9
7 changed files with 20 additions and 104 deletions

View File

@@ -246,14 +246,10 @@ module Public {
predicate isAutoGenerated() { none() }
/**
* Holds if the summary is manually generated and not auto generated.
* Holds if the summary has the given provenance where `true` is
* `generated` and `false` is `manual`.
*/
predicate isManuallyGenerated() { none() }
/**
* Holds if the summary is both auto generated and manually generated.
*/
predicate isBothAutoAndManuallyGenerated() { none() }
predicate hasProvenance(boolean generated) { summaryElement(this, _, _, _, generated) }
}
/** A callable with a flow summary stating there is no flow via the callable. */
@@ -1022,16 +1018,6 @@ module Private {
}
override predicate isAutoGenerated() { this.relevantSummaryElementGenerated(_, _, _) }
override predicate isManuallyGenerated() {
summaryElement(this, _, _, _, false) and
not summaryElement(this, _, _, _, true)
}
override predicate isBothAutoAndManuallyGenerated() {
summaryElement(this, _, _, _, true) and
summaryElement(this, _, _, _, false)
}
}
/** Holds if component `c` of specification `spec` cannot be parsed. */