C#: Make guards library work with CFG splitting

This commit is contained in:
Tom Hvitved
2018-11-22 20:44:17 +01:00
parent 228189db5a
commit 03e69e9945
11 changed files with 282 additions and 102 deletions

View File

@@ -2,6 +2,8 @@
private import semmle.code.csharp.frameworks.system.Diagnostics
private import semmle.code.csharp.frameworks.test.VisualStudio
private import semmle.code.csharp.frameworks.System
private import ControlFlow
private import ControlFlow::BasicBlocks
/** An assertion method. */
abstract class AssertMethod extends Method {
@@ -46,6 +48,49 @@ class Assertion extends MethodCall {
Expr getExpr() {
result = this.getArgumentForParameter(target.getAssertedParameter())
}
pragma[nomagic]
private JoinBlockPredecessor getAPossiblyDominatedPredecessor(JoinBlock jb) {
exists(BasicBlock bb |
bb = this.getAControlFlowNode().getBasicBlock() |
result = bb.getASuccessor*()
) and
result.getASuccessor() = jb
}
pragma[nomagic]
private predicate isPossiblyDominatedJoinBlock(JoinBlock jb) {
exists(this.getAPossiblyDominatedPredecessor(jb)) and
forall(BasicBlock pred |
pred = jb.getAPredecessor() |
pred = this.getAPossiblyDominatedPredecessor(jb)
)
}
/**
* Holds if this assertion strictly dominates basic block `bb`. That is, `bb`
* can only be reached from the callable entry point by going via *some* basic
* block containing this element.
*
* This predicate is different from
* `this.getAControlFlowNode().getBasicBlock().strictlyDominates(bb)`
* in that it takes control flow splitting into account.
*/
pragma[nomagic]
predicate strictlyDominates(BasicBlock bb) {
this.getAControlFlowNode().getBasicBlock().immediatelyDominates(bb)
or
if bb instanceof JoinBlock then
this.isPossiblyDominatedJoinBlock(bb) and
forall(BasicBlock pred |
pred = this.getAPossiblyDominatedPredecessor(bb) |
this.strictlyDominates(pred)
or
this.getAControlFlowNode().getBasicBlock() = pred
)
else
this.strictlyDominates(bb.getAPredecessor())
}
}
/** A trivially failing assertion, for example `Debug.Assert(false)`. */

View File

@@ -15,7 +15,7 @@ class BasicBlock extends TBasicBlockStart {
result.getFirstNode() = getLastNode().getASuccessor()
}
/** Gets an immediate successor of this basic block of a given flow type, if any. */
/** Gets an immediate successor of this basic block of a given type, if any. */
BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) {
result.getFirstNode() = this.getLastNode().getASuccessorByType(t)
}
@@ -25,6 +25,11 @@ class BasicBlock extends TBasicBlockStart {
result.getASuccessor() = this
}
/** Gets an immediate predecessor of this basic block of a given type, if any. */
BasicBlock getAPredecessorByType(ControlFlow::SuccessorType t) {
result.getASuccessorByType(t) = this
}
/**
* Gets an immediate `true` successor, if any.
*
@@ -134,6 +139,31 @@ class BasicBlock extends TBasicBlockStart {
result = strictcount(getANode())
}
/**
* Holds if this basic block immediately dominates basic block `bb`.
*
* That is, all paths reaching basic block `bb` from some entry point
* basic block must go through this basic block (which is an immediate
* predecessor of `bb`).
*
* Example:
*
* ```
* int M(string s) {
* if (s == null)
* throw new ArgumentNullException(nameof(s));
* return s.Length;
* }
* ```
*
* The basic block starting on line 2 strictly dominates the
* basic block on line 4 (all paths from the entry point of `M`
* to `return s.Length;` must go through the null check).
*/
predicate immediatelyDominates(BasicBlock bb) {
bbIDominates(this, bb)
}
/**
* Holds if this basic block strictly dominates basic block `bb`.
*
@@ -419,24 +449,42 @@ private predicate exitBB(BasicBlock bb) {
bb.getLastNode() instanceof ControlFlow::Nodes::ExitNode
}
/**
* A basic block with more than one predecessor.
*/
/** A basic block with more than one predecessor. */
class JoinBlock extends BasicBlock {
JoinBlock() { getFirstNode().isJoin() }
}
/** A basic block that is an immediate predecessor of a join block. */
class JoinBlockPredecessor extends BasicBlock {
JoinBlockPredecessor() {
this.getASuccessor() instanceof JoinBlock
}
}
/** A basic block that terminates in a condition, splitting the subsequent control flow. */
class ConditionBlock extends BasicBlock {
ConditionBlock() {
this.getLastNode().isCondition()
}
/**
* Holds if basic block `succ` is immediately controlled by this basic
* block with conditional value `s`. That is, `succ` is an immediate
* successor of this block, and `succ` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
succ = this.getASuccessorByType(s) and
forall(BasicBlock pred |
pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}
/**
* Holds if basic block `controlled` is controlled by this basic block with
* Boolean value `testIsTrue`. That is, `controlled` can only be reached from
* the callable entry point by going via the true edge (`testIsTrue = true`)
* or false edge (`testIsTrue = false`) out of this basic block.
* conditional value `s`. That is, `controlled` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
/*
@@ -473,7 +521,7 @@ class ConditionBlock extends BasicBlock {
* directly.
*/
exists(BasicBlock succ |
isCandidateSuccessor(succ, s) |
this.immediatelyControls(succ, s) |
succ.dominates(controlled)
)
}
@@ -529,14 +577,6 @@ class ConditionBlock extends BasicBlock {
impliesSub(getLastNode().getElement(), cond, testIsTrue, condIsTrue) and
controls(controlled, any(BooleanSuccessor s | s.getValue() = testIsTrue))
}
private predicate isCandidateSuccessor(BasicBlock succ, ConditionalSuccessor s) {
succ = this.getASuccessorByType(s) and
forall(BasicBlock pred |
pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}
}
/**

View File

@@ -1,7 +1,10 @@
/** Provides the class `ControlFlowElement`. */
import csharp
import csharp
private import semmle.code.csharp.ExprOrStmtParent
private import ControlFlow
private import ControlFlow::BasicBlocks
private import SuccessorTypes
/**
* A program element that can possess control flow. That is, either a statement or
@@ -25,21 +28,21 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
* several `ControlFlow::Node`s, for example to represent the continuation
* flow in a `try/catch/finally` construction.
*/
ControlFlow::Node getAControlFlowNode() {
Node getAControlFlowNode() {
result.getElement() = this
}
/**
* Gets a first control flow node executed within this element.
*/
ControlFlow::Node getAControlFlowEntryNode() {
Node getAControlFlowEntryNode() {
result = ControlFlowGraph::Internal::getAControlFlowEntryNode(this).getAControlFlowNode()
}
/**
* Gets a potential last control flow node executed within this element.
*/
ControlFlow::Node getAControlFlowExitNode() {
Node getAControlFlowExitNode() {
result = ControlFlowGraph::Internal::getAControlFlowExitNode(this).getAControlFlowNode()
}
@@ -59,7 +62,7 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
/** Gets an element that is reachable from this element. */
ControlFlowElement getAReachableElement() {
// Reachable in same basic block
exists(ControlFlow::BasicBlock bb, int i, int j |
exists(BasicBlock bb, int i, int j |
bb.getNode(i) = getAControlFlowNode() and
bb.getNode(j) = result.getAControlFlowNode() and
i < j
@@ -68,4 +71,91 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
// Reachable in different basic blocks
getAControlFlowNode().getBasicBlock().getASuccessor+().getANode() = result.getAControlFlowNode()
}
/**
* Holds if basic block `succ` is immediately controlled by this control flow
* element with conditional value `s`. That is, `succ` can only be reached from
* the callable entry point by going via the `s` edge out of *some* basic block
* `pred` ending with this element, and `pred` is an immediate predecessor
* of `succ`.
*
* This predicate is different from
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).immediatelyControls(succ, s)`
* in that it takes control flow splitting into account.
*/
pragma[nomagic]
private predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
exists(ConditionBlock cb |
cb.getLastNode() = this.getAControlFlowNode() |
succ = cb.getASuccessorByType(s) and
forall(BasicBlock pred, SuccessorType t |
pred = succ.getAPredecessorByType(t) and pred != cb |
succ.dominates(pred)
or
// `pred` might be another split of `cfe`
pred.getLastNode().getElement() = this and
pred.getASuccessorByType(t) = succ and
t = s
)
)
}
pragma[nomagic]
private JoinBlockPredecessor getAPossiblyControlledPredecessor(JoinBlock controlled, ConditionalSuccessor s) {
exists(BasicBlock mid |
this.immediatelyControls(mid, s) |
result = mid.getASuccessor*()
) and
result.getASuccessor() = controlled
}
pragma[nomagic]
private predicate isPossiblyControlledJoinBlock(JoinBlock controlled, ConditionalSuccessor s) {
exists(this.getAPossiblyControlledPredecessor(controlled, s)) and
forall(BasicBlock pred |
pred = controlled.getAPredecessor() |
pred = this.getAPossiblyControlledPredecessor(controlled, s)
)
}
/**
* Holds if basic block `controlled` is controlled by this control flow element
* with conditional value `s`. That is, `controlled` can only be reached from
* the callable entry point by going via the `s` edge out of *some* basic block
* ending with this element.
*
* This predicate is different from
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).controls(controlled, s)`
* in that it takes control flow splitting into account.
*/
cached
predicate controlsBlock(BasicBlock controlled, ConditionalSuccessor s) {
this.immediatelyControls(controlled, s)
or
if controlled instanceof JoinBlock then
this.isPossiblyControlledJoinBlock(controlled, s) and
forall(BasicBlock pred |
pred = this.getAPossiblyControlledPredecessor(controlled, s) |
this.controlsBlock(pred, s)
)
else
this.controlsBlock(controlled.getAPredecessor(), s)
}
/**
* Holds if control flow element `controlled` is controlled by this control flow
* element with conditional value `s`. That is, `controlled` can only be reached
* from the callable entry point by going via the `s` edge out of this element.
*
* This predicate is different from
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).controls(controlled.getAControlFlowNode().getBasicBlock(), s)`
* in that it takes control flow splitting into account.
*/
pragma[inline] // potentially very large predicate, so must be inlined
predicate controlsElement(ControlFlowElement controlled, ConditionalSuccessor s) {
forex(BasicBlock bb |
bb = controlled.getAControlFlowNode().getBasicBlock() |
this.controlsBlock(bb, s)
)
}
}

View File

@@ -183,7 +183,7 @@ module ControlFlow {
)
}
/** Gets a successor node of a given flow type, if any. */
/** Gets a successor node of a given type, if any. */
Node getASuccessorByType(SuccessorType t) {
result = getASuccessorByType(this, t)
}
@@ -372,6 +372,7 @@ module ControlFlow {
class EntryBlock = BBs::EntryBasicBlock;
class ExitBlock = BBs::ExitBasicBlock;
class JoinBlock = BBs::JoinBlock;
class JoinBlockPredecessor = BBs::JoinBlockPredecessor;
class ConditionBlock = BBs::ConditionBlock;
}
@@ -2549,7 +2550,7 @@ module ControlFlow {
) > 1
}
private predicate isCandidateSuccessor(PreBasicBlock succ, ConditionalCompletion c) {
private predicate immediatelyControls(PreBasicBlock succ, ConditionalCompletion c) {
succ = succ(this.getLastElement(), c) and
forall(PreBasicBlock pred |
pred = succ.getAPredecessor() and pred != this |
@@ -2559,7 +2560,7 @@ module ControlFlow {
predicate controls(PreBasicBlock controlled, ConditionalSuccessor s) {
exists(PreBasicBlock succ, ConditionalCompletion c |
isCandidateSuccessor(succ, c) |
immediatelyControls(succ, c) |
succ.dominates(controlled) and
s.matchesCompletion(c)
)

View File

@@ -473,19 +473,40 @@ module Internal {
/** Holds if basic block `bb` only is reached when this guard has abstract value `v`. */
predicate controls(BasicBlock bb, AbstractValue v) {
exists(ConditionBlock cb, ConditionalSuccessor s, AbstractValue v0, Guard g |
cb.controls(bb, s) |
v0.branchImplies(cb.getLastNode().getElement(), s, g) and
exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g |
cfe.controlsBlock(bb, s) |
v0.branchImplies(cfe, s, g) and
impliesSteps(g, v0, this, v)
)
}
/** Holds if control flow node `cfn` only is reached when this guard evaluates to `v`. */
predicate controlsNode(ControlFlow::Node cfn, AbstractValue v) {
/**
* Holds if control flow node `cfn` only is reached when this guard evaluates to `v`,
* because of an assertion.
*/
private predicate assertionControlsNode(ControlFlow::Node cfn, AbstractValue v) {
exists(Assertion a, Guard g, AbstractValue v0 |
a.getAControlFlowNode().dominates(cfn) |
asserts(a, g, v0) and
impliesSteps(g, v0, this, v)
|
a.strictlyDominates(cfn.getBasicBlock())
or
exists(BasicBlock bb, int i, int j |
bb.getNode(i) = a.getAControlFlowNode() |
bb.getNode(j) = cfn and
j > i
)
)
}
/**
* Holds if control flow element `cfe` only is reached when this guard evaluates to `v`,
* because of an assertion.
*/
predicate assertionControlsElement(ControlFlowElement cfe, AbstractValue v) {
forex(ControlFlow::Node cfn |
cfn = cfe.getAControlFlowNode() |
this.assertionControlsNode(cfn, v)
)
}
@@ -639,24 +660,33 @@ module Internal {
e = g.getAChildExpr*() |
g.controls(bb, _)
or
g.controlsNode(bb.getANode(), _)
g.assertionControlsElement(bb.getANode().getElement(), _)
)
}
}
private cached module Cached {
pragma[noinline]
private predicate isGuardedBy0(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v) {
exists(ControlFlow::Node cfn |
(g.controls(cfn.getBasicBlock(), v) or g.controlsNode(cfn, v)) and
cfn = guarded.getAControlFlowNode() and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded))
private predicate isGuardedBy0(ControlFlow::Node cfn, AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v) {
cfn = guarded.getAControlFlowNode() and
g.controls(cfn.getBasicBlock(), v) and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded))
}
pragma[noinline]
private predicate isGuardedBy1(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v) {
forex(ControlFlow::Node cfn |
cfn = guarded.getAControlFlowNode() |
isGuardedBy0(cfn, guarded, g, sub, v)
)
or
g.assertionControlsElement(guarded, v) and
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded))
}
cached
predicate isGuardedBy(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v) {
isGuardedBy0(guarded, g, sub, v) and
isGuardedBy1(guarded, g, sub, v) and
sub = g.getAChildExpr*() and
(
not guarded.hasSsaQualifier() and not sub.hasSsaQualifier()

View File

@@ -190,3 +190,10 @@ class SendingMethod extends SensitiveExecutionMethod {
)
}
}
/** A call to a method that sends data, and so should not be run conditionally on user input. */
class SensitiveExecutionMethodCall extends MethodCall {
SensitiveExecutionMethodCall() {
this.getTarget() instanceof SensitiveExecutionMethod
}
}

View File

@@ -68,26 +68,26 @@ module UserControlledBypassOfSensitiveMethod {
}
}
private predicate conditionControlsCall(SensitiveExecutionMethodCall call, SensitiveExecutionMethod def, Expr e, boolean cond) {
exists(ControlFlow::SuccessorTypes::BooleanSuccessor s |
cond = s.getValue() |
e.controlsElement(call, s)
) and
def = call.getTarget()
}
/**
* Calls to a sensitive method that are controlled by a condition
* on the given expression.
*/
predicate conditionControlsMethod(MethodCall call, Expr e) {
exists(ConditionBlock cb, SensitiveExecutionMethod def, boolean cond |
exists(ControlFlow::SuccessorTypes::BooleanSuccessor s |
cond = s.getValue() |
cb.controls(call.getAControlFlowNode().getBasicBlock(), s)
) and
def = call.getTarget() and
predicate conditionControlsMethod(SensitiveExecutionMethodCall call, Expr e) {
exists(SensitiveExecutionMethod def, boolean cond |
conditionControlsCall(call, def, e, cond) and
/*
* Exclude this condition if the other branch also contains a call to the same security
* sensitive method.
*/
not exists(ControlFlow::SuccessorTypes::BooleanSuccessor s |
cond = s.getValue().booleanNot() |
cb.controls(def.getACall().getAControlFlowNode().getBasicBlock(), s)
) and
e = cb.getLastNode().getElement()
not conditionControlsCall(_, def, e, cond.booleanNot())
)
}

View File

@@ -63,39 +63,20 @@
| Guards.cs:196:31:196:31 | access to parameter s | Guards.cs:195:13:195:27 | call to method NotNullTest4 | Guards.cs:195:26:195:26 | access to parameter s | true |
| Guards.cs:198:31:198:31 | access to parameter s | Guards.cs:197:14:197:29 | call to method NullTestWrong | Guards.cs:197:28:197:28 | access to parameter s | false |
| Splitting.cs:13:17:13:17 | access to parameter o | Splitting.cs:12:17:12:25 | ... != ... | Splitting.cs:12:17:12:17 | access to parameter o | true |
| Splitting.cs:14:13:14:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | false |
| Splitting.cs:14:13:14:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | true |
| Splitting.cs:23:24:23:24 | access to parameter o | Splitting.cs:22:17:22:25 | ... != ... | Splitting.cs:22:17:22:17 | access to parameter o | true |
| Splitting.cs:24:13:24:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | false |
| Splitting.cs:24:13:24:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | true |
| Splitting.cs:25:13:25:13 | access to parameter o | Splitting.cs:22:17:22:25 | ... != ... | Splitting.cs:22:17:22:17 | access to parameter o | false |
| Splitting.cs:34:13:34:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | false |
| Splitting.cs:34:13:34:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | true |
| Splitting.cs:35:13:35:13 | access to parameter o | Splitting.cs:32:17:32:25 | ... == ... | Splitting.cs:32:17:32:17 | access to parameter o | false |
| Splitting.cs:44:17:44:17 | access to parameter o | Splitting.cs:41:13:41:21 | ... != ... | Splitting.cs:41:13:41:13 | access to parameter o | true |
| Splitting.cs:45:17:45:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | false |
| Splitting.cs:45:17:45:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | true |
| Splitting.cs:46:17:46:17 | access to parameter o | Splitting.cs:41:13:41:21 | ... != ... | Splitting.cs:41:13:41:13 | access to parameter o | true |
| Splitting.cs:55:13:55:13 | access to parameter o | Splitting.cs:54:13:54:21 | ... != ... | Splitting.cs:54:13:54:13 | access to parameter o | true |
| Splitting.cs:56:13:56:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | false |
| Splitting.cs:56:13:56:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | true |
| Splitting.cs:67:13:67:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | false |
| Splitting.cs:67:13:67:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | true |
| Splitting.cs:66:20:66:20 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | true |
| Splitting.cs:68:13:68:13 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | false |
| Splitting.cs:79:13:79:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | false |
| Splitting.cs:79:13:79:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | true |
| Splitting.cs:88:9:88:9 | access to parameter o | Splitting.cs:87:26:87:34 | ... != ... | Splitting.cs:87:26:87:26 | access to parameter o | true |
| Splitting.cs:89:13:89:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | false |
| Splitting.cs:89:13:89:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | true |
| Splitting.cs:69:16:69:16 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | false |
| Splitting.cs:78:24:78:24 | access to parameter o | Splitting.cs:76:13:76:21 | ... != ... | Splitting.cs:76:13:76:13 | access to parameter o | true |
| Splitting.cs:90:13:90:13 | access to parameter o | Splitting.cs:87:26:87:34 | ... != ... | Splitting.cs:87:26:87:26 | access to parameter o | true |
| Splitting.cs:98:13:98:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | false |
| Splitting.cs:98:13:98:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | true |
| Splitting.cs:99:13:99:13 | access to parameter o | Splitting.cs:97:26:97:34 | ... == ... | Splitting.cs:97:26:97:26 | access to parameter o | true |
| Splitting.cs:107:13:107:13 | access to parameter o | Splitting.cs:105:22:105:30 | ... != ... | Splitting.cs:105:22:105:22 | access to parameter o | true |
| Splitting.cs:108:13:108:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | false |
| Splitting.cs:108:13:108:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | true |
| Splitting.cs:109:13:109:13 | access to parameter o | Splitting.cs:105:22:105:30 | ... != ... | Splitting.cs:105:22:105:22 | access to parameter o | true |
| Splitting.cs:117:9:117:9 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:118:13:118:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | false |
| Splitting.cs:118:13:118:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | true |
| Splitting.cs:119:13:119:13 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |

View File

@@ -157,53 +157,37 @@
| Guards.cs:198:31:198:31 | access to parameter s | Guards.cs:197:14:197:29 | call to method NullTestWrong | Guards.cs:197:28:197:28 | access to parameter s | false |
| Splitting.cs:13:17:13:17 | access to parameter o | Splitting.cs:12:17:12:17 | access to parameter o | Splitting.cs:12:17:12:17 | access to parameter o | non-null |
| Splitting.cs:13:17:13:17 | access to parameter o | Splitting.cs:12:17:12:25 | ... != ... | Splitting.cs:12:17:12:17 | access to parameter o | true |
| Splitting.cs:14:13:14:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | false |
| Splitting.cs:14:13:14:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | Splitting.cs:11:13:11:13 | access to parameter b | true |
| Splitting.cs:23:24:23:24 | access to parameter o | Splitting.cs:22:17:22:17 | access to parameter o | Splitting.cs:22:17:22:17 | access to parameter o | non-null |
| Splitting.cs:23:24:23:24 | access to parameter o | Splitting.cs:22:17:22:25 | ... != ... | Splitting.cs:22:17:22:17 | access to parameter o | true |
| Splitting.cs:24:13:24:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | false |
| Splitting.cs:24:13:24:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | Splitting.cs:21:13:21:13 | access to parameter b | true |
| Splitting.cs:25:13:25:13 | access to parameter o | Splitting.cs:22:17:22:17 | access to parameter o | Splitting.cs:22:17:22:17 | access to parameter o | null |
| Splitting.cs:25:13:25:13 | access to parameter o | Splitting.cs:22:17:22:25 | ... != ... | Splitting.cs:22:17:22:17 | access to parameter o | false |
| Splitting.cs:34:13:34:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | false |
| Splitting.cs:34:13:34:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | Splitting.cs:31:13:31:13 | access to parameter b | true |
| Splitting.cs:35:13:35:13 | access to parameter o | Splitting.cs:32:17:32:17 | access to parameter o | Splitting.cs:32:17:32:17 | access to parameter o | non-null |
| Splitting.cs:35:13:35:13 | access to parameter o | Splitting.cs:32:17:32:25 | ... == ... | Splitting.cs:32:17:32:17 | access to parameter o | false |
| Splitting.cs:44:17:44:17 | access to parameter o | Splitting.cs:41:13:41:13 | access to parameter o | Splitting.cs:41:13:41:13 | access to parameter o | non-null |
| Splitting.cs:44:17:44:17 | access to parameter o | Splitting.cs:41:13:41:21 | ... != ... | Splitting.cs:41:13:41:13 | access to parameter o | true |
| Splitting.cs:45:17:45:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | false |
| Splitting.cs:45:17:45:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | Splitting.cs:43:17:43:17 | access to parameter b | true |
| Splitting.cs:46:17:46:17 | access to parameter o | Splitting.cs:41:13:41:13 | access to parameter o | Splitting.cs:41:13:41:13 | access to parameter o | non-null |
| Splitting.cs:46:17:46:17 | access to parameter o | Splitting.cs:41:13:41:21 | ... != ... | Splitting.cs:41:13:41:13 | access to parameter o | true |
| Splitting.cs:55:13:55:13 | access to parameter o | Splitting.cs:54:13:54:13 | access to parameter o | Splitting.cs:54:13:54:13 | access to parameter o | non-null |
| Splitting.cs:55:13:55:13 | access to parameter o | Splitting.cs:54:13:54:21 | ... != ... | Splitting.cs:54:13:54:13 | access to parameter o | true |
| Splitting.cs:56:13:56:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | false |
| Splitting.cs:56:13:56:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b | true |
| Splitting.cs:67:13:67:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | false |
| Splitting.cs:67:13:67:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | Splitting.cs:63:13:63:13 | access to parameter b | true |
| Splitting.cs:66:20:66:20 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | non-null |
| Splitting.cs:66:20:66:20 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | true |
| Splitting.cs:68:13:68:13 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | null |
| Splitting.cs:68:13:68:13 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | false |
| Splitting.cs:79:13:79:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | false |
| Splitting.cs:79:13:79:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | Splitting.cs:74:13:74:13 | access to parameter b | true |
| Splitting.cs:88:9:88:9 | access to parameter o | Splitting.cs:87:26:87:26 | access to parameter o | Splitting.cs:87:26:87:26 | access to parameter o | non-null |
| Splitting.cs:88:9:88:9 | access to parameter o | Splitting.cs:87:26:87:34 | ... != ... | Splitting.cs:87:26:87:26 | access to parameter o | true |
| Splitting.cs:89:13:89:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | false |
| Splitting.cs:89:13:89:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | Splitting.cs:86:13:86:13 | access to parameter b | true |
| Splitting.cs:69:16:69:16 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | Splitting.cs:65:13:65:13 | access to parameter o | null |
| Splitting.cs:69:16:69:16 | access to parameter o | Splitting.cs:65:13:65:21 | ... != ... | Splitting.cs:65:13:65:13 | access to parameter o | false |
| Splitting.cs:78:24:78:24 | access to parameter o | Splitting.cs:76:13:76:13 | access to parameter o | Splitting.cs:76:13:76:13 | access to parameter o | non-null |
| Splitting.cs:78:24:78:24 | access to parameter o | Splitting.cs:76:13:76:21 | ... != ... | Splitting.cs:76:13:76:13 | access to parameter o | true |
| Splitting.cs:90:13:90:13 | access to parameter o | Splitting.cs:87:26:87:26 | access to parameter o | Splitting.cs:87:26:87:26 | access to parameter o | non-null |
| Splitting.cs:90:13:90:13 | access to parameter o | Splitting.cs:87:26:87:34 | ... != ... | Splitting.cs:87:26:87:26 | access to parameter o | true |
| Splitting.cs:98:13:98:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | false |
| Splitting.cs:98:13:98:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | Splitting.cs:96:13:96:13 | access to parameter b | true |
| Splitting.cs:99:13:99:13 | access to parameter o | Splitting.cs:97:26:97:26 | access to parameter o | Splitting.cs:97:26:97:26 | access to parameter o | null |
| Splitting.cs:99:13:99:13 | access to parameter o | Splitting.cs:97:26:97:34 | ... == ... | Splitting.cs:97:26:97:26 | access to parameter o | true |
| Splitting.cs:107:13:107:13 | access to parameter o | Splitting.cs:105:22:105:22 | access to parameter o | Splitting.cs:105:22:105:22 | access to parameter o | non-null |
| Splitting.cs:107:13:107:13 | access to parameter o | Splitting.cs:105:22:105:30 | ... != ... | Splitting.cs:105:22:105:22 | access to parameter o | true |
| Splitting.cs:108:13:108:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | false |
| Splitting.cs:108:13:108:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | Splitting.cs:106:13:106:13 | access to parameter b | true |
| Splitting.cs:109:13:109:13 | access to parameter o | Splitting.cs:105:22:105:22 | access to parameter o | Splitting.cs:105:22:105:22 | access to parameter o | non-null |
| Splitting.cs:109:13:109:13 | access to parameter o | Splitting.cs:105:22:105:30 | ... != ... | Splitting.cs:105:22:105:22 | access to parameter o | true |
| Splitting.cs:117:9:117:9 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | non-null |
| Splitting.cs:117:9:117:9 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:118:13:118:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | false |
| Splitting.cs:118:13:118:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | Splitting.cs:114:13:114:13 | access to parameter b | true |
| Splitting.cs:119:13:119:13 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | non-null |
| Splitting.cs:119:13:119:13 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | non-null |
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |

View File

@@ -45,9 +45,11 @@
| Splitting.cs:44:17:44:17 | access to parameter o |
| Splitting.cs:46:17:46:17 | access to parameter o |
| Splitting.cs:55:13:55:13 | access to parameter o |
| Splitting.cs:88:9:88:9 | access to parameter o |
| Splitting.cs:66:20:66:20 | access to parameter o |
| Splitting.cs:78:24:78:24 | access to parameter o |
| Splitting.cs:90:13:90:13 | access to parameter o |
| Splitting.cs:107:13:107:13 | access to parameter o |
| Splitting.cs:109:13:109:13 | access to parameter o |
| Splitting.cs:117:9:117:9 | access to parameter o |
| Splitting.cs:119:13:119:13 | access to parameter o |
| Splitting.cs:120:16:120:16 | access to parameter o |

View File

@@ -63,10 +63,10 @@ public class Splitting
if (b)
o.ToString(); // not null guarded
if (o != null)
return o.ToString(); // null guarded (missing)
return o.ToString(); // null guarded
if (b)
o.ToString(); // anti-null guarded
return o.ToString(); // anti-null guarded (missing)
return o.ToString(); // anti-null guarded
}
string M7(bool b, object o, bool b2)
@@ -75,7 +75,7 @@ public class Splitting
o.ToString(); // not null guarded
if (o != null)
if (b2)
return o.ToString(); // null guarded (missing)
return o.ToString(); // null guarded
if (b)
o.ToString(); // not null guarded
return o.ToString(); // not null guarded
@@ -85,7 +85,7 @@ public class Splitting
{
if (b)
Debug.Assert(o != null);
o.ToString(); // not null guarded (incorrect)
o.ToString(); // not null guarded
if (b)
o.ToString(); // null guarded
o.ToString(); // not null guarded
@@ -117,6 +117,6 @@ public class Splitting
o.ToString(); // null guarded
if (b)
o.ToString(); // null guarded
return o.ToString(); // null guarded (missing)
return o.ToString(); // null guarded
}
}