Merge pull request #579 from hvitved/csharp/guards-loop

C#: Fix bug in guards library when the guarded expression is in a loop
This commit is contained in:
calumgrant 2018-11-30 10:27:21 +00:00 коммит произвёл GitHub
Родитель 1c5322274a a12a72e90f
Коммит ca72c8ebfe
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
7 изменённых файлов: 30 добавлений и 2 удалений

Просмотреть файл

@ -55,7 +55,8 @@ class Assertion extends MethodCall {
bb = this.getAControlFlowNode().getBasicBlock() |
result = bb.getASuccessor*()
) and
result.getASuccessor() = jb
result.getASuccessor() = jb and
not jb.dominates(result)
}
pragma[nomagic]
@ -64,6 +65,8 @@ class Assertion extends MethodCall {
forall(BasicBlock pred |
pred = jb.getAPredecessor() |
pred = this.getAPossiblyDominatedPredecessor(jb)
or
jb.dominates(pred)
)
}

Просмотреть файл

@ -106,7 +106,8 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
this.immediatelyControls(mid, s) |
result = mid.getASuccessor*()
) and
result.getASuccessor() = controlled
result.getASuccessor() = controlled and
not controlled.dominates(result)
}
pragma[nomagic]
@ -115,6 +116,8 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
forall(BasicBlock pred |
pred = controlled.getAPredecessor() |
pred = this.getAPossiblyControlledPredecessor(controlled, s)
or
controlled.dominates(pred)
)
}

Просмотреть файл

@ -62,6 +62,8 @@
| Guards.cs:194:31:194:31 | access to parameter s | Guards.cs:193:14:193:25 | call to method NullTest3 | Guards.cs:193:24:193:24 | access to parameter s | false |
| 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 |
| Guards.cs:205:13:205:13 | access to parameter o | Guards.cs:203:13:203:21 | ... != ... | Guards.cs:203:13:203:13 | access to parameter o | true |
| Guards.cs:208:17:208:17 | access to parameter o | Guards.cs:203:13:203:21 | ... != ... | Guards.cs:203:13:203:13 | access to parameter o | true |
| 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: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: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 |

Просмотреть файл

@ -155,6 +155,10 @@
| 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:196:31:196:31 | access to parameter s | Guards.cs:195:26:195:26 | access to parameter s | Guards.cs:195:26:195:26 | access to parameter s | non-null |
| 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 |
| Guards.cs:205:13:205:13 | access to parameter o | Guards.cs:203:13:203:13 | access to parameter o | Guards.cs:203:13:203:13 | access to parameter o | non-null |
| Guards.cs:205:13:205:13 | access to parameter o | Guards.cs:203:13:203:21 | ... != ... | Guards.cs:203:13:203:13 | access to parameter o | true |
| Guards.cs:208:17:208:17 | access to parameter o | Guards.cs:203:13:203:13 | access to parameter o | Guards.cs:203:13:203:13 | access to parameter o | non-null |
| Guards.cs:208:17:208:17 | access to parameter o | Guards.cs:203:13:203:21 | ... != ... | Guards.cs:203:13:203:13 | access to parameter o | true |
| 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: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 |

Просмотреть файл

@ -197,4 +197,16 @@ public class Guards
if (!NullTestWrong(s))
Console.WriteLine(s); // not null guarded
}
void M17(object o, string[] args)
{
if (o != null)
{
o.ToString(); // null guarded
foreach (var arg in args)
{
o.ToString(); // null guarded
}
}
}
}

Просмотреть файл

@ -200,6 +200,8 @@
| Guards.cs:195:13:195:27 | call to method NotNullTest4 | true | Guards.cs:195:26:195:26 | access to parameter s | non-null |
| Guards.cs:197:13:197:29 | !... | false | Guards.cs:197:14:197:29 | call to method NullTestWrong | true |
| Guards.cs:197:13:197:29 | !... | true | Guards.cs:197:14:197:29 | call to method NullTestWrong | false |
| Guards.cs:203:13:203:21 | ... != ... | false | Guards.cs:203:13:203:13 | access to parameter o | null |
| Guards.cs:203:13:203:21 | ... != ... | true | Guards.cs:203:13:203:13 | access to parameter o | non-null |
| Splitting.cs:12:17:12:25 | ... != ... | false | Splitting.cs:12:17:12:17 | access to parameter o | null |
| Splitting.cs:12:17:12:25 | ... != ... | true | Splitting.cs:12:17:12:17 | access to parameter o | non-null |
| Splitting.cs:22:17:22:25 | ... != ... | false | Splitting.cs:22:17:22:17 | access to parameter o | null |

Просмотреть файл

@ -39,6 +39,8 @@
| Guards.cs:192:31:192:31 | access to parameter s |
| Guards.cs:194:31:194:31 | access to parameter s |
| Guards.cs:196:31:196:31 | access to parameter s |
| Guards.cs:205:13:205:13 | access to parameter o |
| Guards.cs:208:17:208:17 | access to parameter o |
| Splitting.cs:13:17:13:17 | access to parameter o |
| Splitting.cs:23:24:23:24 | access to parameter o |
| Splitting.cs:35:13:35:13 | access to parameter o |