C#: Rename predicate as per review, and fixup qltest.

This commit is contained in:
Anders Schack-Mulligen
2025-09-17 11:58:39 +02:00
parent 62c8f28e74
commit 5e76d5ff3f
5 changed files with 54 additions and 11 deletions

View File

@@ -274,7 +274,7 @@ module AbstractValues {
private import AbstractValues
/** Gets the value resulting from matching `null` against `pat`. */
private boolean patternContainsNull(PatternExpr pat) {
private boolean patternMatchesNull(PatternExpr pat) {
pat instanceof NullLiteral and result = true
or
not pat instanceof NullLiteral and
@@ -283,18 +283,16 @@ private boolean patternContainsNull(PatternExpr pat) {
not pat instanceof AndPatternExpr and
result = false
or
result = patternContainsNull(pat.(NotPatternExpr).getPattern()).booleanNot()
result = patternMatchesNull(pat.(NotPatternExpr).getPattern()).booleanNot()
or
exists(OrPatternExpr ope | pat = ope |
result =
patternContainsNull(ope.getLeftOperand())
.booleanOr(patternContainsNull(ope.getRightOperand()))
patternMatchesNull(ope.getLeftOperand()).booleanOr(patternMatchesNull(ope.getRightOperand()))
)
or
exists(AndPatternExpr ape | pat = ape |
result =
patternContainsNull(ape.getLeftOperand())
.booleanAnd(patternContainsNull(ape.getRightOperand()))
patternMatchesNull(ape.getLeftOperand()).booleanAnd(patternMatchesNull(ape.getRightOperand()))
)
}
@@ -387,7 +385,7 @@ class DereferenceableExpr extends Expr {
isNull = branch
or
// E.g. `x is string` or `x is ""`
branch.booleanNot() = patternContainsNull(pm.getPattern()) and
branch.booleanNot() = patternMatchesNull(pm.getPattern()) and
isNull = false
or
exists(TypePatternExpr tpe |

View File

@@ -432,7 +432,7 @@ public class E
return @is.Any();
}
static void Ex45(string s)
static void Ex45(string s) // $ Source[cs/dereferenced-value-may-be-null]
{
if (s is null)
{
@@ -441,7 +441,7 @@ public class E
if (s is not not null)
{
s.ToString(); // $ MISSING: Alert[cs/dereferenced-value-is-always-null]
s.ToString(); // $ Alert[cs/dereferenced-value-may-be-null] MISSING: Alert[cs/dereferenced-value-is-always-null]
}
if (s is not null)
@@ -453,6 +453,15 @@ public class E
{
s.ToString(); // GOOD
}
if (s is not object)
{
s.ToString(); // $ Alert[cs/dereferenced-value-may-be-null]
}
else
{
s.ToString(); // GOOD
}
}
}

View File

@@ -1302,9 +1302,10 @@
| E.cs:432:16:432:24 | call to method Any<Int32> | true | E.cs:432:16:432:18 | access to parameter is | non-empty |
| E.cs:437:13:437:21 | ... is ... | false | E.cs:437:13:437:13 | access to parameter s | non-null |
| E.cs:437:13:437:21 | ... is ... | true | E.cs:437:13:437:13 | access to parameter s | null |
| E.cs:442:13:442:29 | ... is ... | true | E.cs:442:13:442:13 | access to parameter s | non-null |
| E.cs:442:13:442:29 | ... is ... | false | E.cs:442:13:442:13 | access to parameter s | non-null |
| E.cs:447:13:447:25 | ... is ... | true | E.cs:447:13:447:13 | access to parameter s | non-null |
| E.cs:452:13:452:23 | ... is ... | true | E.cs:452:13:452:13 | access to parameter s | non-null |
| E.cs:457:13:457:27 | ... is ... | false | E.cs:457:13:457:13 | access to parameter s | non-null |
| F.cs:8:9:8:9 | access to local variable o | non-null | F.cs:7:20:7:23 | null | non-null |
| F.cs:8:9:8:9 | access to local variable o | null | F.cs:7:20:7:23 | null | null |
| F.cs:14:9:14:9 | access to local variable o | non-null | F.cs:13:21:13:24 | null | non-null |

View File

@@ -300,9 +300,10 @@
| E.cs:429:13:429:22 | access to property HasValue | E.cs:429:13:429:13 | access to parameter i | true | false |
| E.cs:437:13:437:21 | ... is ... | E.cs:437:13:437:13 | access to parameter s | false | false |
| E.cs:437:13:437:21 | ... is ... | E.cs:437:13:437:13 | access to parameter s | true | true |
| E.cs:442:13:442:29 | ... is ... | E.cs:442:13:442:13 | access to parameter s | true | false |
| E.cs:442:13:442:29 | ... is ... | E.cs:442:13:442:13 | access to parameter s | false | false |
| E.cs:447:13:447:25 | ... is ... | E.cs:447:13:447:13 | access to parameter s | true | false |
| E.cs:452:13:452:23 | ... is ... | E.cs:452:13:452:13 | access to parameter s | true | false |
| E.cs:457:13:457:27 | ... is ... | E.cs:457:13:457:13 | access to parameter s | false | false |
| Forwarding.cs:9:14:9:30 | call to method IsNullOrEmpty | Forwarding.cs:9:14:9:14 | access to local variable s | false | false |
| Forwarding.cs:14:13:14:32 | call to method IsNotNullOrEmpty | Forwarding.cs:14:13:14:13 | access to local variable s | true | false |
| Forwarding.cs:19:14:19:23 | call to method IsNull | Forwarding.cs:19:14:19:14 | access to local variable s | false | false |

View File

@@ -83,6 +83,8 @@
| E.cs:417:34:417:34 | access to parameter i | E.cs:417:24:417:40 | SSA capture def(i) | E.cs:417:34:417:34 | access to parameter i | Variable $@ may be null at this access because it has a nullable type. | E.cs:415:27:415:27 | i | i | E.cs:415:27:415:27 | i | this |
| E.cs:423:38:423:38 | access to parameter i | E.cs:423:28:423:44 | SSA capture def(i) | E.cs:423:38:423:38 | access to parameter i | Variable $@ may be null at this access because it has a nullable type. | E.cs:420:27:420:27 | i | i | E.cs:420:27:420:27 | i | this |
| E.cs:430:39:430:39 | access to parameter i | E.cs:430:29:430:45 | SSA capture def(i) | E.cs:430:39:430:39 | access to parameter i | Variable $@ may be null at this access because it has a nullable type. | E.cs:427:27:427:27 | i | i | E.cs:427:27:427:27 | i | this |
| E.cs:444:13:444:13 | access to parameter s | E.cs:435:29:435:29 | SSA param(s) | E.cs:444:13:444:13 | access to parameter s | Variable $@ may be null at this access as suggested by $@ null check. | E.cs:435:29:435:29 | s | s | E.cs:437:13:437:21 | ... is ... | this |
| E.cs:459:13:459:13 | access to parameter s | E.cs:435:29:435:29 | SSA param(s) | E.cs:459:13:459:13 | access to parameter s | Variable $@ may be null at this access as suggested by $@ null check. | E.cs:435:29:435:29 | s | s | E.cs:437:13:437:21 | ... is ... | this |
| GuardedString.cs:35:31:35:31 | access to local variable s | GuardedString.cs:7:16:7:32 | SSA def(s) | GuardedString.cs:35:31:35:31 | access to local variable s | Variable $@ may be null at this access because of $@ assignment. | GuardedString.cs:7:16:7:16 | s | s | GuardedString.cs:7:16:7:32 | String s = ... | this |
| NullMaybeBad.cs:7:27:7:27 | access to parameter o | NullMaybeBad.cs:13:17:13:20 | null | NullMaybeBad.cs:7:27:7:27 | access to parameter o | Variable $@ may be null at this access because of $@ null argument. | NullMaybeBad.cs:5:25:5:25 | o | o | NullMaybeBad.cs:13:17:13:20 | null | this |
| Params.cs:14:17:14:20 | access to parameter args | Params.cs:20:12:20:15 | null | Params.cs:14:17:14:20 | access to parameter args | Variable $@ may be null at this access because of $@ null argument. | Params.cs:12:36:12:39 | args | args | Params.cs:20:12:20:15 | null | this |
@@ -445,7 +447,23 @@ edges
| E.cs:423:28:423:44 | SSA capture def(i) | E.cs:423:38:423:38 | access to parameter i |
| E.cs:430:29:430:45 | SSA capture def(i) | E.cs:430:39:430:39 | access to parameter i |
| E.cs:435:29:435:29 | SSA param(s) | E.cs:437:13:437:21 | [true] ... is ... |
| E.cs:437:13:437:21 | [true] ... is ... | E.cs:438:9:440:9 | {...} |
| E.cs:437:13:437:21 | [true] ... is ... | E.cs:439:13:439:13 | access to parameter s |
| E.cs:438:9:440:9 | {...} | E.cs:442:9:445:9 | if (...) ... |
| E.cs:442:9:445:9 | if (...) ... | E.cs:442:22:442:29 | [no-match] not ... |
| E.cs:442:13:442:29 | [true] ... is ... | E.cs:443:9:445:9 | {...} |
| E.cs:442:13:442:29 | [true] ... is ... | E.cs:444:13:444:13 | access to parameter s |
| E.cs:442:18:442:29 | [match] not ... | E.cs:442:13:442:29 | [true] ... is ... |
| E.cs:442:22:442:29 | [no-match] not ... | E.cs:442:18:442:29 | [match] not ... |
| E.cs:443:9:445:9 | {...} | E.cs:447:9:450:9 | if (...) ... |
| E.cs:447:9:450:9 | if (...) ... | E.cs:447:18:447:25 | [no-match] not ... |
| E.cs:447:13:447:25 | [false] ... is ... | E.cs:452:9:455:9 | if (...) ... |
| E.cs:447:18:447:25 | [no-match] not ... | E.cs:447:13:447:25 | [false] ... is ... |
| E.cs:452:9:455:9 | if (...) ... | E.cs:452:13:452:23 | [false] ... is ... |
| E.cs:452:13:452:23 | [false] ... is ... | E.cs:457:9:464:9 | if (...) ... |
| E.cs:457:9:464:9 | if (...) ... | E.cs:457:18:457:27 | [match] not ... |
| E.cs:457:13:457:27 | [true] ... is ... | E.cs:459:13:459:13 | access to parameter s |
| E.cs:457:18:457:27 | [match] not ... | E.cs:457:13:457:27 | [true] ... is ... |
| F.cs:7:16:7:23 | SSA def(o) | F.cs:8:9:8:9 | access to local variable o |
| Forwarding.cs:7:16:7:23 | SSA def(s) | Forwarding.cs:9:13:9:30 | [false] !... |
| Forwarding.cs:9:13:9:30 | [false] !... | Forwarding.cs:14:9:17:9 | if (...) ... |
@@ -894,7 +912,23 @@ nodes
| E.cs:430:39:430:39 | access to parameter i |
| E.cs:435:29:435:29 | SSA param(s) |
| E.cs:437:13:437:21 | [true] ... is ... |
| E.cs:438:9:440:9 | {...} |
| E.cs:439:13:439:13 | access to parameter s |
| E.cs:442:9:445:9 | if (...) ... |
| E.cs:442:13:442:29 | [true] ... is ... |
| E.cs:442:18:442:29 | [match] not ... |
| E.cs:442:22:442:29 | [no-match] not ... |
| E.cs:443:9:445:9 | {...} |
| E.cs:444:13:444:13 | access to parameter s |
| E.cs:447:9:450:9 | if (...) ... |
| E.cs:447:13:447:25 | [false] ... is ... |
| E.cs:447:18:447:25 | [no-match] not ... |
| E.cs:452:9:455:9 | if (...) ... |
| E.cs:452:13:452:23 | [false] ... is ... |
| E.cs:457:9:464:9 | if (...) ... |
| E.cs:457:13:457:27 | [true] ... is ... |
| E.cs:457:18:457:27 | [match] not ... |
| E.cs:459:13:459:13 | access to parameter s |
| F.cs:7:16:7:23 | SSA def(o) |
| F.cs:8:9:8:9 | access to local variable o |
| Forwarding.cs:7:16:7:23 | SSA def(s) |