Revise ExternalFlow and FlowSummaryImpl API used for test generation

This commit is contained in:
Chris Smowton
2021-06-21 19:38:51 +01:00
parent b1af90991d
commit c49d5253f0
2 changed files with 27 additions and 14 deletions

View File

@@ -415,19 +415,25 @@ predicate summaryModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
string input, string output, string kind
) {
exists(string row |
summaryModel(row) and
row.splitAt(";", 0) = namespace and
row.splitAt(";", 1) = type and
row.splitAt(";", 2) = subtypes.toString() and
subtypes = [true, false] and
row.splitAt(";", 3) = name and
row.splitAt(";", 4) = signature and
row.splitAt(";", 5) = ext and
row.splitAt(";", 6) = input and
row.splitAt(";", 7) = output and
row.splitAt(";", 8) = kind
)
summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, _)
}
/** Holds if a summary model `row` exists for the given parameters. */
predicate summaryModel(
string namespace, string type, boolean subtypes, string name, string signature, string ext,
string input, string output, string kind, string row
) {
summaryModel(row) and
row.splitAt(";", 0) = namespace and
row.splitAt(";", 1) = type and
row.splitAt(";", 2) = subtypes.toString() and
subtypes = [true, false] and
row.splitAt(";", 3) = name and
row.splitAt(";", 4) = signature and
row.splitAt(";", 5) = ext and
row.splitAt(";", 6) = input and
row.splitAt(";", 7) = output and
row.splitAt(";", 8) = kind
}
private predicate relevantPackage(string package) {

View File

@@ -643,7 +643,14 @@ module Private {
)
}
private predicate interpretSpec(string spec, int idx, SummaryComponentStack stack) {
/**
* Holds if `spec` specifies summary component stack `stack`.
*/
predicate interpretSpec(string spec, SummaryComponentStack stack) {
interpretSpec(spec, 0, stack)
}
predicate interpretSpec(string spec, int idx, SummaryComponentStack stack) {
exists(string c |
relevantSpec(spec) and
specLength(spec, idx + 1) and