C#: Fix CFG for assertions with multiple assertion arguments

This commit is contained in:
Tom Hvitved
2020-10-28 15:52:13 +01:00
parent 5cd707f17e
commit 51f71d4e1d
12 changed files with 340 additions and 174 deletions

View File

@@ -9,43 +9,114 @@ private import ControlFlow::BasicBlocks
/** An assertion method. */
abstract class AssertMethod extends Method {
/**
* DEPRECATED: renamed to `getAnAssertionIndex`.
*
* Gets the index of a parameter being asserted.
*/
deprecated int getAssertionIndex() { result = getAnAssertionIndex() }
/** Gets the index of a parameter being asserted. */
abstract int getAnAssertionIndex();
/**
* DEPRECATED: renamed to `getAnAssertedParameter`.
* DEPRECATED: Use `getAnAssertionIndex()` instead.
*
* Gets the index of a parameter being asserted.
*/
deprecated final int getAssertionIndex() { result = getAnAssertionIndex() }
/** Gets the parameter at position `i` being asserted. */
final Parameter getAssertedParameter(int i) {
result = this.getParameter(i) and
i = this.getAnAssertionIndex()
}
/**
* DEPRECATED: Use `getAssertedParameter(_)` instead.
*
* Gets a parameter being asserted.
*/
deprecated Parameter getAssertedParameter() { result = getAnAssertedParameter() }
deprecated final Parameter getAssertedParameter() { result = getAssertedParameter(_) }
/** Gets a parameter being asserted. */
final Parameter getAnAssertedParameter() {
result = this.getParameter(this.getAnAssertionIndex())
}
/** Gets the exception being thrown if the assertion fails for argument `i`, if any. */
abstract Class getExceptionClass(int i);
/** Gets the exception being thrown if the assertion fails, if any. */
abstract Class getExceptionClass();
/**
* DEPRECATED: Use `getExceptionClass(_)` instead.
*
* Gets the exception being thrown if the assertion fails, if any.
*/
deprecated final Class getExceptionClass() { result = this.getExceptionClass(_) }
}
/** A Boolean assertion method. */
abstract class BooleanAssertMethod extends AssertMethod {
/** Gets the index of a parameter asserted to have value `b`. */
abstract int getAnAssertionIndex(boolean b);
override int getAnAssertionIndex() { result = this.getAnAssertionIndex(_) }
}
/** A positive assertion method. */
abstract class AssertTrueMethod extends AssertMethod { }
deprecated class AssertTrueMethod extends AssertMethod {
private BooleanAssertMethod m;
AssertTrueMethod() {
this = m and
exists(m.getAnAssertionIndex(true))
}
final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
}
/** A negated assertion method. */
abstract class AssertFalseMethod extends AssertMethod { }
deprecated class AssertFalseMethod extends AssertMethod {
private BooleanAssertMethod m;
AssertFalseMethod() {
this = m and
exists(m.getAnAssertionIndex(false))
}
final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
}
/** A nullness assertion method. */
abstract class NullnessAssertMethod extends AssertMethod {
/**
* Gets the index of a parameter asserted to be `null` (`b = true`)
* or non-`null` (`b = false`).
*/
abstract int getAnAssertionIndex(boolean b);
override int getAnAssertionIndex() { result = this.getAnAssertionIndex(_) }
}
/** A `null` assertion method. */
abstract class AssertNullMethod extends AssertMethod { }
deprecated class AssertNullMethod extends AssertMethod {
private NullnessAssertMethod m;
AssertNullMethod() {
this = m and
exists(m.getAnAssertionIndex(true))
}
final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
}
/** A non-`null` assertion method. */
abstract class AssertNonNullMethod extends AssertMethod { }
deprecated class AssertNonNullMethod extends AssertMethod {
private NullnessAssertMethod m;
AssertNonNullMethod() {
this = m and
exists(m.getAnAssertionIndex(false))
}
final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
}
/** An assertion, that is, a call to an assertion method. */
class Assertion extends MethodCall {
@@ -56,15 +127,21 @@ class Assertion extends MethodCall {
/** Gets the assertion method targeted by this assertion. */
AssertMethod getAssertMethod() { result = target }
/** Gets an expression at argument position `i` that this assertion pertains to. */
Expr getExpr(int i) {
i = target.getAnAssertionIndex() and
exists(Parameter p |
p = target.getParameter(i) and
result = this.getArgumentForParameter(p)
)
}
/**
* DEPRECATED: renamed to `getAnExpr`.
* DEPRECATED: Use `getExpr(_)` instead.
*
* Gets an expression that this assertion pertains to.
*/
deprecated Expr getExpr() { result = this.getAnExpr() }
/** Gets an expression that this assertion pertains to. */
Expr getAnExpr() { result = this.getArgumentForParameter(target.getAnAssertedParameter()) }
deprecated Expr getExpr() { result = this.getExpr(_) }
/**
* Holds if basic block `succ` is immediately dominated by this assertion.
@@ -164,31 +241,37 @@ class Assertion extends MethodCall {
/** A trivially failing assertion, for example `Debug.Assert(false)`. */
class FailingAssertion extends Assertion {
private int i;
FailingAssertion() {
exists(AssertMethod am, Expr e |
exists(BooleanAssertMethod am, Expr e, boolean b |
am = this.getAssertMethod() and
e = this.getAnExpr()
e = this.getExpr(i) and
i = am.getAnAssertionIndex(b)
|
am instanceof AssertTrueMethod and
b = true and
e.getValue() = "false"
or
am instanceof AssertFalseMethod and
b = false and
e.getValue() = "true"
)
}
/** Gets the exception being thrown by this failing assertion, if any. */
Class getExceptionClass() { result = this.getAssertMethod().getExceptionClass(i) }
}
/**
* A `System.Diagnostics.Debug` assertion method.
*/
class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
class SystemDiagnosticsDebugAssertTrueMethod extends BooleanAssertMethod {
SystemDiagnosticsDebugAssertTrueMethod() {
this = any(SystemDiagnosticsDebugClass c).getAssertMethod()
}
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = true }
override Class getExceptionClass() {
override Class getExceptionClass(int i) {
// A failing assertion generates a message box, see
// https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.debug.assert
none()
@@ -198,7 +281,7 @@ class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
/**
* A `System.Diagnostics.Contracts.Contract` assertion method.
*/
class SystemDiagnosticsContractAssertTrueMethod extends AssertTrueMethod {
class SystemDiagnosticsContractAssertTrueMethod extends BooleanAssertMethod {
SystemDiagnosticsContractAssertTrueMethod() {
exists(SystemDiagnosticsContractsContractClass c |
this = c.getAnAssertMethod()
@@ -209,9 +292,9 @@ class SystemDiagnosticsContractAssertTrueMethod extends AssertTrueMethod {
)
}
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = true }
override Class getExceptionClass() {
override Class getExceptionClass(int i) {
// A failing assertion generates a message box, see
// https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.contracts.contract.assert
none()
@@ -229,79 +312,82 @@ private predicate isDoesNotReturnIfAttributeParameter(Parameter p, boolean value
* A method with a parameter that is annotated with
* `System.Diagnostics.CodeAnalysis.DoesNotReturnIfAttribute(false)`.
*/
class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod extends AssertTrueMethod {
private int i;
class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod extends BooleanAssertMethod {
private int i_;
SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod() {
isDoesNotReturnIfAttributeParameter(this.getParameter(i), false)
isDoesNotReturnIfAttributeParameter(this.getParameter(i_), false)
}
override int getAnAssertionIndex() { result = i }
override int getAnAssertionIndex(boolean b) { result = i_ and b = true }
override SystemExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = i_ and result instanceof SystemExceptionClass }
}
/**
* A method with a parameter that is annotated with
* `System.Diagnostics.CodeAnalysis.DoesNotReturnIfAttribute(true)`.
*/
class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod extends AssertFalseMethod {
private int i;
class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod extends BooleanAssertMethod {
private int i_;
SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod() {
isDoesNotReturnIfAttributeParameter(this.getParameter(i), true)
isDoesNotReturnIfAttributeParameter(this.getParameter(i_), true)
}
override int getAnAssertionIndex() { result = i }
override int getAnAssertionIndex(boolean b) {
result = i_ and
b = false
}
override SystemExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = i_ and result instanceof SystemExceptionClass }
}
/** A Visual Studio assertion method. */
class VSTestAssertTrueMethod extends AssertTrueMethod {
class VSTestAssertTrueMethod extends BooleanAssertMethod {
VSTestAssertTrueMethod() { this = any(VSTestAssertClass c).getIsTrueMethod() }
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = true }
override AssertFailedExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
}
/** A Visual Studio negated assertion method. */
class VSTestAssertFalseMethod extends AssertFalseMethod {
class VSTestAssertFalseMethod extends BooleanAssertMethod {
VSTestAssertFalseMethod() { this = any(VSTestAssertClass c).getIsFalseMethod() }
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = false }
override AssertFailedExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
}
/** A Visual Studio `null` assertion method. */
class VSTestAssertNullMethod extends AssertNullMethod {
class VSTestAssertNullMethod extends NullnessAssertMethod {
VSTestAssertNullMethod() { this = any(VSTestAssertClass c).getIsNullMethod() }
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = true }
override AssertFailedExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
}
/** A Visual Studio non-`null` assertion method. */
class VSTestAssertNonNullMethod extends AssertNonNullMethod {
class VSTestAssertNonNullMethod extends NullnessAssertMethod {
VSTestAssertNonNullMethod() { this = any(VSTestAssertClass c).getIsNotNullMethod() }
override int getAnAssertionIndex() { result = 0 }
override int getAnAssertionIndex(boolean b) { result = 0 and b = false }
override AssertFailedExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
}
/** An NUnit assertion method. */
abstract class NUnitAssertMethod extends AssertMethod {
override int getAnAssertionIndex() { result = 0 }
override AssertionExceptionClass getExceptionClass() { any() }
override Class getExceptionClass(int i) { i = 0 and result instanceof AssertionExceptionClass }
}
/** An NUnit assertion method. */
class NUnitAssertTrueMethod extends AssertTrueMethod, NUnitAssertMethod {
class NUnitAssertTrueMethod extends BooleanAssertMethod, NUnitAssertMethod {
NUnitAssertTrueMethod() {
exists(NUnitAssertClass c |
this = c.getATrueMethod()
@@ -312,56 +398,77 @@ class NUnitAssertTrueMethod extends AssertTrueMethod, NUnitAssertMethod {
this.getParameter(0).getType() instanceof BoolType
)
}
override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = true }
}
/** An NUnit negated assertion method. */
class NUnitAssertFalseMethod extends AssertFalseMethod, NUnitAssertMethod {
class NUnitAssertFalseMethod extends BooleanAssertMethod, NUnitAssertMethod {
NUnitAssertFalseMethod() {
exists(NUnitAssertClass c |
this = c.getAFalseMethod() or
this = c.getAnIsFalseMethod()
)
}
override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = false }
}
/** An NUnit `null` assertion method. */
class NUnitAssertNullMethod extends AssertNullMethod, NUnitAssertMethod {
class NUnitAssertNullMethod extends NullnessAssertMethod, NUnitAssertMethod {
NUnitAssertNullMethod() {
exists(NUnitAssertClass c |
this = c.getANullMethod() or
this = c.getAnIsNullMethod()
)
}
override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = true }
}
/** An NUnit non-`null` assertion method. */
class NUnitAssertNonNullMethod extends AssertNonNullMethod, NUnitAssertMethod {
class NUnitAssertNonNullMethod extends NullnessAssertMethod, NUnitAssertMethod {
NUnitAssertNonNullMethod() {
exists(NUnitAssertClass c |
this = c.getANotNullMethod() or
this = c.getAnIsNotNullMethod()
)
}
override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = false }
}
/** A method that forwards to another assertion method. */
class ForwarderAssertMethod extends AssertMethod {
Assertion a;
Parameter p;
private Assertion a;
private Parameter p;
private int forwarderIndex;
ForwarderAssertMethod() {
p = this.getAParameter() and
strictcount(AssignableDefinition def | def.getTarget() = p) = 1 and
forex(ControlFlowElement body | body = this.getBody() |
bodyAsserts(this, body, a) and
a.getAnExpr() = p.getAnAccess()
a.getExpr(forwarderIndex) = p.getAnAccess()
)
}
override int getAnAssertionIndex() { result = p.getPosition() }
override Class getExceptionClass() {
result = this.getUnderlyingAssertMethod().getExceptionClass()
/** Gets the assertion index of the forwarded assertion, for assertion index `i`. */
int getAForwarderAssertionIndex(int i) { i = p.getPosition() and result = forwarderIndex }
override Class getExceptionClass(int i) {
i = p.getPosition() and
result = this.getUnderlyingAssertMethod().getExceptionClass(forwarderIndex)
}
/** Gets the underlying assertion method that is being forwarded to. */
@@ -386,25 +493,63 @@ private Stmt getAnAssertingStmt(Assertion a) {
result.(BlockStmt).getFirstStmt() = getAnAssertingElement(a)
}
/** A method that forwards to a Boolean assertion method. */
class ForwarderBooleanAssertMethod extends BooleanAssertMethod {
private ForwarderAssertMethod forwarder;
private BooleanAssertMethod underlying;
ForwarderBooleanAssertMethod() {
forwarder = this and
underlying = forwarder.getUnderlyingAssertMethod()
}
override int getAnAssertionIndex(boolean b) {
forwarder.getAForwarderAssertionIndex(result) = underlying.getAnAssertionIndex(b)
}
override Class getExceptionClass(int i) {
result = underlying.getExceptionClass(forwarder.getAForwarderAssertionIndex(i))
}
}
/** A method that forwards to a positive assertion method. */
class ForwarderAssertTrueMethod extends ForwarderAssertMethod, AssertTrueMethod {
ForwarderAssertTrueMethod() { this.getUnderlyingAssertMethod() instanceof AssertTrueMethod }
deprecated class ForwarderAssertTrueMethod extends ForwarderBooleanAssertMethod {
ForwarderAssertTrueMethod() { exists(this.getAnAssertionIndex(true)) }
}
/** A method that forwards to a negated assertion method. */
class ForwarderAssertFalseMethod extends ForwarderAssertMethod, AssertFalseMethod {
ForwarderAssertFalseMethod() { this.getUnderlyingAssertMethod() instanceof AssertFalseMethod }
deprecated class ForwarderAssertFalseMethod extends ForwarderBooleanAssertMethod {
ForwarderAssertFalseMethod() { exists(this.getAnAssertionIndex(false)) }
}
/** A method that forwards to a nullness assertion method. */
class ForwarderNullnessAssertMethod extends NullnessAssertMethod {
private ForwarderAssertMethod forwarder;
private NullnessAssertMethod underlying;
ForwarderNullnessAssertMethod() {
forwarder = this and
underlying = forwarder.getUnderlyingAssertMethod()
}
override int getAnAssertionIndex(boolean b) {
forwarder.getAForwarderAssertionIndex(result) = underlying.getAnAssertionIndex(b)
}
override Class getExceptionClass(int i) {
result = underlying.getExceptionClass(forwarder.getAForwarderAssertionIndex(i))
}
}
/** A method that forwards to a `null` assertion method. */
class ForwarderAssertNullMethod extends ForwarderAssertMethod, AssertNullMethod {
ForwarderAssertNullMethod() { this.getUnderlyingAssertMethod() instanceof AssertNullMethod }
deprecated class ForwarderAssertNullMethod extends ForwarderNullnessAssertMethod {
ForwarderAssertNullMethod() { exists(this.getAnAssertionIndex(true)) }
}
/** A method that forwards to a non-`null` assertion method. */
class ForwarderAssertNonNullMethod extends ForwarderAssertMethod, AssertNonNullMethod {
ForwarderAssertNonNullMethod() { this.getUnderlyingAssertMethod() instanceof AssertNonNullMethod }
deprecated class ForwarderAssertNonNullMethod extends ForwarderNullnessAssertMethod {
ForwarderAssertNonNullMethod() { exists(this.getAnAssertionIndex(false)) }
}
/** Holds if expression `e` appears in an assertion. */
predicate isExprInAssertion(Expr e) { e = any(Assertion a).getAnExpr().getAChildExpr*() }
predicate isExprInAssertion(Expr e) { e = any(Assertion a).getExpr(_).getAChildExpr*() }

View File

@@ -99,12 +99,7 @@ class Completion extends TCompletion {
cfe instanceof ThrowElement and
this = TThrowCompletion(cfe.(ThrowElement).getThrownExceptionType())
or
exists(AssertMethod m | assertion(cfe, m, _) |
this = TThrowCompletion(m.getExceptionClass())
or
not exists(m.getExceptionClass()) and
this = TExitCompletion()
)
this = assertionCompletion(cfe, _)
or
completionIsValidForStmt(cfe, this)
or
@@ -390,11 +385,22 @@ private predicate invalidCastCandidate(CastExpr ce) {
ce.getType() = ce.getExpr().getType().(ValueOrRefType).getASubType+()
}
private predicate assertion(Assertion a, AssertMethod am, Expr e) {
e = a.getAnExpr() and
private predicate assertion(Assertion a, int i, AssertMethod am, Expr e) {
e = a.getExpr(i) and
am = a.getAssertMethod()
}
/** Gets a valid completion when argument `i` fails in assertion `a`. */
Completion assertionCompletion(Assertion a, int i) {
exists(AssertMethod am | am = a.getAssertMethod() |
result = TThrowCompletion(am.getExceptionClass(i))
or
i = am.getAnAssertionIndex() and
not exists(am.getExceptionClass(i)) and
result = TExitCompletion()
)
}
/**
* Holds if a normal completion of `e` must be a Boolean completion.
*/
@@ -422,8 +428,11 @@ private predicate inBooleanContext(Expr e, boolean isBooleanCompletionForParent)
or
exists(SpecificCatchClause scc | scc.getFilterClause() = e | isBooleanCompletionForParent = false)
or
assertion(_, [any(AssertTrueMethod m).(AssertMethod), any(AssertFalseMethod m)], e) and
isBooleanCompletionForParent = false
exists(BooleanAssertMethod m, int i |
assertion(_, i, m, e) and
i = m.getAnAssertionIndex(_) and
isBooleanCompletionForParent = false
)
or
exists(LogicalNotExpr lne | lne.getAnOperand() = e |
inBooleanContext(lne, _) and
@@ -495,8 +504,11 @@ private predicate inNullnessContext(Expr e, boolean isNullnessCompletionForParen
isNullnessCompletionForParent = false
)
or
assertion(_, [any(AssertNullMethod m).(AssertMethod), any(AssertNonNullMethod m)], e) and
isNullnessCompletionForParent = false
exists(NullnessAssertMethod m, int i |
assertion(_, i, m, e) and
i = m.getAnAssertionIndex(_) and
isNullnessCompletionForParent = false
)
or
exists(ConditionalExpr ce | inNullnessContext(ce, _) |
(e = ce.getThen() or e = ce.getElse()) and

View File

@@ -23,9 +23,7 @@ private class ExitingCall extends NonReturningCall {
ExitingCall() {
this.getTarget() instanceof ExitingCallable
or
exists(AssertMethod m | m = this.(FailingAssertion).getAssertMethod() |
not exists(m.getExceptionClass())
)
this = any(FailingAssertion fa | not exists(fa.getExceptionClass()))
}
override ExitCompletion getACompletion() { not result instanceof NestedCompletion }
@@ -39,9 +37,7 @@ private class ThrowingCall extends NonReturningCall {
(
c = this.getTarget().(ThrowingCallable).getACallCompletion()
or
exists(AssertMethod m | m = this.(FailingAssertion).getAssertMethod() |
c.getExceptionClass() = m.getExceptionClass()
)
c.getExceptionClass() = this.(FailingAssertion).getExceptionClass()
or
exists(CIL::Method m, CIL::Type ex |
this.getTarget().matchesHandle(m) and

View File

@@ -36,14 +36,17 @@ private module Cached {
cached
newtype TSplit =
TInitializerSplit(Constructor c) { InitializerSplitting::constructorInitializes(c, _) } or
TAssertionSplit(AssertionSplitting::Assertion a, boolean success) { success = [true, false] } or
TAssertionSplit(AssertionSplitting::Assertion a, int i, boolean success) {
exists(a.getExpr(i)) and
success in [false, true]
} or
TFinallySplit(FinallySplitting::FinallySplitType type, int nestLevel) {
nestLevel = FinallySplitting::nestLevel(_)
} or
TExceptionHandlerSplit(ExceptionClass ec) or
TBooleanSplit(BooleanSplitting::BooleanSplitSubKind kind, boolean branch) {
kind.startsSplit(_) and
(branch = true or branch = false)
branch in [false, true]
} or
TLoopSplit(LoopSplitting::AnalyzableLoopStmt loop)
@@ -414,8 +417,9 @@ module AssertionSplitting {
class AssertionSplitImpl extends SplitImpl, TAssertionSplit {
Assertion a;
boolean success;
int i;
AssertionSplitImpl() { this = TAssertionSplit(a, success) }
AssertionSplitImpl() { this = TAssertionSplit(a, i, success) }
/** Gets the assertion. */
Assertion getAssertion() { result = a }
@@ -445,37 +449,29 @@ module AssertionSplitting {
override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
exists(AssertMethod m |
pred = last(a.getAnExpr(), c) and
pred = last(a.getExpr(i), c) and
succ = succ(pred, c) and
this.getAssertion() = a and
m = a.getAssertMethod()
m = a.getAssertMethod() and
// The assertion only succeeds when all asserted arguments succeeded, so
// we only enter a "success" state after the last argument has succeeded.
//
// The split is only entered if we are not already in a "failing" state
// for one of the previous arguments, which ensures that the "success"
// state is only entered when all arguments succeed. This also means
// that if multiple arguments fail, then the first failing argument
// will determine the exception being thrown by the assertion.
if success = true then i = max(int j | exists(a.getExpr(j))) else any()
|
m instanceof AssertTrueMethod and
(
c instanceof TrueCompletion and success = true
exists(boolean b | i = m.(BooleanAssertMethod).getAnAssertionIndex(b) |
c instanceof TrueCompletion and success = b
or
c instanceof FalseCompletion and success = false
c instanceof FalseCompletion and success = b.booleanNot()
)
or
m instanceof AssertFalseMethod and
(
c instanceof TrueCompletion and success = false
exists(boolean b | i = m.(NullnessAssertMethod).getAnAssertionIndex(b) |
c.(NullnessCompletion).isNull() and success = b
or
c instanceof FalseCompletion and success = true
)
or
m instanceof AssertNullMethod and
(
c.(NullnessCompletion).isNull() and success = true
or
c.(NullnessCompletion).isNonNull() and success = false
)
or
m instanceof AssertNonNullMethod and
(
c.(NullnessCompletion).isNull() and success = false
or
c.(NullnessCompletion).isNonNull() and success = true
c.(NullnessCompletion).isNonNull() and success = b.booleanNot()
)
)
}
@@ -491,7 +487,7 @@ module AssertionSplitting {
c instanceof NormalCompletion
or
success = false and
not c instanceof NormalCompletion
c = assertionCompletion(a, i)
)
}
@@ -504,7 +500,7 @@ module AssertionSplitting {
c instanceof NormalCompletion
or
success = false and
not c instanceof NormalCompletion
c = assertionCompletion(a, i)
)
}
@@ -1604,7 +1600,7 @@ private module SuccSplits {
/**
* Holds if `succSplits` should not inherit a split of kind `sk` from
* `predSplits, except possibly because of a split in `except`.
* `predSplits`, except possibly because of a split in `except`.
*
* The predicate is written using explicit recursion, as opposed to a `forall`,
* to avoid negative recursion.

View File

@@ -2,21 +2,29 @@ import csharp
import semmle.code.csharp.commons.Assertions
query predicate assertTrue(Assertion a, Expr e) {
a.getAnExpr() = e and
a.getTarget() instanceof AssertTrueMethod
exists(int i |
a.getExpr(i) = e and
i = a.getTarget().(BooleanAssertMethod).getAnAssertionIndex(true)
)
}
query predicate assertFalse(Assertion a, Expr e) {
a.getAnExpr() = e and
a.getTarget() instanceof AssertFalseMethod
exists(int i |
a.getExpr(i) = e and
i = a.getTarget().(BooleanAssertMethod).getAnAssertionIndex(false)
)
}
query predicate assertNull(Assertion a, Expr e) {
a.getAnExpr() = e and
a.getTarget() instanceof AssertNullMethod
exists(int i |
a.getExpr(i) = e and
i = a.getTarget().(NullnessAssertMethod).getAnAssertionIndex(true)
)
}
query predicate assertNonNull(Assertion a, Expr e) {
a.getAnExpr() = e and
a.getTarget() instanceof AssertNonNullMethod
exists(int i |
a.getExpr(i) = e and
i = a.getTarget().(NullnessAssertMethod).getAnAssertionIndex(false)
)
}

View File

@@ -138,7 +138,9 @@
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:25:140:26 | access to parameter b1 | 5 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 | 1 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | 3 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:141:9:141:15 | return ...; | 4 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 | 1 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | 2 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:141:9:141:15 | return ...; | 3 |
| Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | exit M | 33 |
| Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | exit (...) => ... | 3 |
| Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | exit + | 5 |

View File

@@ -295,9 +295,11 @@ conditionBlock
| Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | true |
| Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:37:127:38 | [b (line 84): true] !... | false |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | false |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | true |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | false |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | true |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | access to parameter b2 | true |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | false |
| BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | BreakInTry.cs:7:26:7:28 | String arg | false |
| BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | BreakInTry.cs:10:21:10:26 | break; | false |
| BreakInTry.cs:7:26:7:28 | String arg | BreakInTry.cs:10:21:10:26 | break; | true |
@@ -1212,13 +1214,11 @@ conditionFlow
| Assert.cs:127:24:127:32 | [b (line 84): true] ... != ... | Assert.cs:127:37:127:38 | [b (line 84): true] !... | false |
| Assert.cs:127:38:127:38 | [b (line 84): true] access to parameter b | Assert.cs:127:9:127:39 | [assertion success] call to method IsFalse | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 | true |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | false |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | false |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | false |
| BreakInTry.cs:9:21:9:31 | ... == ... | BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | false |
| BreakInTry.cs:9:21:9:31 | ... == ... | BreakInTry.cs:10:21:10:26 | break; | true |
| BreakInTry.cs:15:17:15:28 | ... == ... | BreakInTry.cs:3:10:3:11 | exit M1 | false |

View File

@@ -3,20 +3,10 @@ nonUniqueSetRepresentation
breakInvariant2
breakInvariant3
breakInvariant4
| Assert.cs:140:25:140:26 | access to parameter b1 | | Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | assertion success | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | | Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | assertion success | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | | Assert.cs:140:29:140:30 | access to parameter b2 | assertion success | assertion failure | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | | Assert.cs:140:29:140:30 | access to parameter b2 | assertion success | assertion failure | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | Assert.cs:140:33:140:34 | access to parameter b3 | assertion failure | assertion failure | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | Assert.cs:140:33:140:34 | access to parameter b3 | assertion failure | assertion success | false |
| Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | Assert.cs:140:33:140:34 | access to parameter b3 | assertion failure | assertion success | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | assertion success | Assert.cs:140:33:140:34 | access to parameter b3 | assertion success | assertion failure | false |
| Assert.cs:140:29:140:30 | access to parameter b2 | assertion success | Assert.cs:140:33:140:34 | access to parameter b3 | assertion success | assertion failure | true |
breakInvariant5
multipleSuccessors
| Assert.cs:140:25:140:26 | access to parameter b1 | false | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:25:140:26 | access to parameter b1 | false | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:140:25:140:26 | access to parameter b1 | true | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:25:140:26 | access to parameter b1 | true | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| ConditionalAccess.cs:30:28:30:32 | ... = ... | successor | ConditionalAccess.cs:1:7:1:23 | exit ConditionalAccess |
| ConditionalAccess.cs:30:28:30:32 | ... = ... | successor | ConditionalAccess.cs:30:10:30:12 | exit Out |
| MultiImplementationA.cs:6:22:6:31 | enter get_P1 | successor | MultiImplementationA.cs:6:28:6:31 | null |

View File

@@ -809,9 +809,11 @@ dominance
| Assert.cs:140:9:140:35 | this access | Assert.cs:140:25:140:26 | access to parameter b1 |
| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | this access |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse |
| Assignments.cs:3:10:3:10 | enter M | Assignments.cs:4:5:15:5 | {...} |
@@ -4550,15 +4552,16 @@ postDominance
| Assert.cs:131:18:131:32 | exit AssertTrueFalse | Assert.cs:135:5:136:5 | {...} |
| Assert.cs:135:5:136:5 | {...} | Assert.cs:131:18:131:32 | enter AssertTrueFalse |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:141:9:141:15 | return ...; |
| Assert.cs:139:5:142:5 | {...} | Assert.cs:138:10:138:12 | enter M13 |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:140:9:140:35 | this access | Assert.cs:140:9:140:36 | ...; |
| Assert.cs:140:9:140:36 | ...; | Assert.cs:139:5:142:5 | {...} |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:9:140:35 | this access |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:141:9:141:15 | return ...; | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse |
| Assignments.cs:3:10:3:10 | exit M | Assignments.cs:14:9:14:35 | ... += ... |
| Assignments.cs:4:5:15:5 | {...} | Assignments.cs:3:10:3:10 | enter M |
@@ -7910,10 +7913,16 @@ blockDominance
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | enter M13 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | exit M13 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | access to parameter b2 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | enter M |
| Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | enter (...) => ... |
| Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | enter + |
@@ -10667,9 +10676,13 @@ postBlockDominance
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | enter M13 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:29:140:30 | access to parameter b2 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
| Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | enter M |
| Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | enter (...) => ... |
| Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | enter + |

View File

@@ -860,12 +860,14 @@ nodeEnclosing
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:139:5:142:5 | {...} | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:9:140:35 | this access | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:9:140:36 | ...; | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:141:9:141:15 | return ...; | Assert.cs:138:10:138:12 | M13 |
@@ -4358,7 +4360,9 @@ blockEnclosing
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
| Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | M |
| Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | (...) => ... |
| Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | + |

View File

@@ -874,17 +874,17 @@
| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:139:5:142:5 | {...} | semmle.label | successor |
| Assert.cs:139:5:142:5 | {...} | Assert.cs:140:9:140:36 | ...; | semmle.label | successor |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | exit M13 | semmle.label | exception(Exception) |
| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | exit M13 | semmle.label | exception(Exception) |
| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:141:9:141:15 | return ...; | semmle.label | successor |
| Assert.cs:140:9:140:35 | this access | Assert.cs:140:25:140:26 | access to parameter b1 | semmle.label | successor |
| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | this access | semmle.label | successor |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | semmle.label | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | semmle.label | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | semmle.label | false |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | semmle.label | true |
| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 | semmle.label | true |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | false |
| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | true |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | semmle.label | false |
| Assert.cs:140:29:140:30 | [assertion success] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | semmle.label | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | true |
| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | semmle.label | false |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | semmle.label | successor |
| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | semmle.label | successor |
| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | semmle.label | successor |
| Assert.cs:141:9:141:15 | return ...; | Assert.cs:138:10:138:12 | exit M13 | semmle.label | return |

View File

@@ -1,18 +1,18 @@
import csharp
import semmle.code.csharp.commons.Assertions
query predicate assertTrue(AssertTrueMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
query predicate assertTrue(BooleanAssertMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(true))
}
query predicate assertFalse(AssertFalseMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
query predicate assertFalse(BooleanAssertMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(false))
}
query predicate assertNull(AssertNullMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
query predicate assertNull(NullnessAssertMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(true))
}
query predicate assertNonNull(AssertNonNullMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
query predicate assertNonNull(NullnessAssertMethod m, Parameter p) {
m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(false))
}