C#: Define extensible predicates.

This commit is contained in:
Michael Nebel
2022-10-14 10:43:05 +02:00
parent eb27e8acc5
commit 7be79290e8

View File

@@ -189,6 +189,14 @@ private predicate negativeSummaryModelInternal(string row) {
any(NegativeSummaryModelCsv s).row(row)
}
/**
* Holds if a source model exists for the given parameters.
*/
extensible predicate extSourceModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
string output, string kind, string provenance
);
/** Holds if a source model exists for the given parameters. */
predicate sourceModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
@@ -207,6 +215,8 @@ predicate sourceModel(
row.splitAt(";", 7) = kind and
row.splitAt(";", 8) = provenance
)
or
extSourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance)
}
/** Holds if `row` is a source model. */
@@ -229,6 +239,12 @@ predicate sourceModel(string row) {
)
}
/** Holds if a sink model exists for the given parameters. */
extensible predicate extSinkModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
string input, string kind, string provenance
);
/** Holds if a sink model exists for the given parameters. */
predicate sinkModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
@@ -247,6 +263,8 @@ predicate sinkModel(
row.splitAt(";", 7) = kind and
row.splitAt(";", 8) = provenance
)
or
extSinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance)
}
/** Holds if `row` is a sink model. */
@@ -269,6 +287,12 @@ predicate sinkModel(string row) {
)
}
/** Holds if a summary model exists for the given parameters. */
extensible predicate extSummaryModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
string input, string output, string kind, string provenance
);
/** Holds if a summary model exists for the given parameters. */
predicate summaryModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
@@ -288,6 +312,8 @@ predicate summaryModel(
row.splitAt(";", 8) = kind and
row.splitAt(";", 9) = provenance
)
or
extSummaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, provenance)
}
/** Holds if `row` is a summary model. */
@@ -311,6 +337,11 @@ predicate summaryModel(string row) {
)
}
/** Holds if a summary model exists indicating there is no flow for the given parameters. */
extensible predicate extNegativeSummaryModel(
string namespace, string type, string name, string signature, string provenance
);
/** Holds if a summary model exists indicating there is no flow for the given parameters. */
predicate negativeSummaryModel(
string namespace, string type, string name, string signature, string provenance
@@ -323,6 +354,8 @@ predicate negativeSummaryModel(
row.splitAt(";", 3) = signature and
row.splitAt(";", 4) = provenance
)
or
extNegativeSummaryModel(namespace, type, name, signature, provenance)
}
/** Holds if `row` is a negative summary model. */