C#: Remove clearsContent predicate from the framework code.

This commit is contained in:
Michael Nebel
2022-08-23 14:13:24 +02:00
parent 19da00a51a
commit ecce30ed5a

View File

@@ -226,15 +226,6 @@ module Public {
none() none()
} }
/**
* Holds if values stored inside `content` are cleared on objects passed as
* arguments at position `pos` to this callable.
*
* TODO: Remove once all languages support `WithoutContent` tokens.
*/
pragma[nomagic]
predicate clearsContent(ParameterPosition pos, ContentSet content) { none() }
/** /**
* Holds if the summary is auto generated. * Holds if the summary is auto generated.
*/ */
@@ -328,23 +319,6 @@ module Private {
SummaryComponentStack::singleton(TArgumentSummaryComponent(_))) and SummaryComponentStack::singleton(TArgumentSummaryComponent(_))) and
preservesValue = preservesValue1.booleanAnd(preservesValue2) preservesValue = preservesValue1.booleanAnd(preservesValue2)
) )
or
exists(ParameterPosition ppos, ContentSet cs |
c.clearsContent(ppos, cs) and
input = SummaryComponentStack::push(SummaryComponent::withoutContent(cs), output) and
output = SummaryComponentStack::argument(ppos) and
preservesValue = true
)
}
private class MkClearStack extends RequiredSummaryComponentStack {
override predicate required(SummaryComponent head, SummaryComponentStack tail) {
exists(SummarizedCallable sc, ParameterPosition ppos, ContentSet cs |
sc.clearsContent(ppos, cs) and
head = SummaryComponent::withoutContent(cs) and
tail = SummaryComponentStack::argument(ppos)
)
}
} }
/** /**
@@ -945,8 +919,7 @@ module Private {
AccessPath inSpec, AccessPath outSpec, string kind AccessPath inSpec, AccessPath outSpec, string kind
) { ) {
summaryElement(this, inSpec, outSpec, kind, true) and summaryElement(this, inSpec, outSpec, kind, true) and
not summaryElement(this, _, _, _, false) and not summaryElement(this, _, _, _, false)
not this.clearsContent(_, _)
} }
private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) { private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {