Shared: use a module as input to 'KindValidation'

This commit is contained in:
Jami Cogswell
2023-06-09 14:35:37 -04:00
parent bcba1f3a4d
commit 9abe3e3da4
8 changed files with 63 additions and 85 deletions

View File

@@ -266,20 +266,17 @@ module ModelValidation {
)
}
/** Holds if a summary model exists for the given `kind`. */
private predicate summaryKind(string kind) { summaryModel(_, _, _, _, _, _, _, _, kind, _) }
private module KindValConfig implements SharedModelVal::KindValidationConfigSig {
predicate summaryKind(string kind) { summaryModel(_, _, _, _, _, _, _, _, kind, _) }
/** Holds if a sink model exists for the given `kind`. */
private predicate sinkKind(string kind) { sinkModel(_, _, _, _, _, _, _, kind, _) }
predicate sinkKind(string kind) { sinkModel(_, _, _, _, _, _, _, kind, _) }
/** Holds if a source model exists for the given `kind`. */
private predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _) }
predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _) }
/** Holds if a neutral model exists for the given `kind`. */
private predicate neutralKind(string kind) { neutralModel(_, _, _, _, kind, _) }
predicate neutralKind(string kind) { neutralModel(_, _, _, _, kind, _) }
}
private module KindVal =
SharedModelVal::KindValidation<summaryKind/1, sinkKind/1, sourceKind/1, neutralKind/1>;
private module KindVal = SharedModelVal::KindValidation<KindValConfig>;
private string getInvalidModelSignature() {
exists(