CPP: Fix for LocalScopeReachability.

This commit is contained in:
Geoffrey White
2019-05-23 12:30:27 +01:00
parent f4b4ddbdaf
commit 56adcff2c9
3 changed files with 25 additions and 23 deletions

View File

@@ -131,20 +131,27 @@ private predicate bbLoopEntryConditionAlwaysTrueAt(BasicBlock bb, int i, Control
}
/**
* Basic block `pred` ends with a condition belonging to a loop, and that
* condition is provably true upon entry. Basic block `succ` is a successor
* of `pred`, and `skipsLoop` indicates whether `succ` is the false-successor
* of `pred`.
* Basic block `pred` contains all or part of the condition belonging to a loop,
* and there is an edge from `pred` to `succ` that concludes the condition.
* If the edge corrseponds with the loop condition being found to be `true`, then
* `skipsLoop` is `false`. Otherwise the edge corresponds with the loop condition
* being found to be `false` and `skipsLoop` is `true`. Non-concluding edges
* within a complex loop condition are not matched by this predicate.
*/
private predicate bbLoopConditionAlwaysTrueUponEntrySuccessor(BasicBlock pred, BasicBlock succ, boolean skipsLoop) {
succ = pred.getASuccessor() and
exists(ControlFlowNode last |
last = pred.getEnd() and
loopConditionAlwaysTrueUponEntry(_, last) and
if succ = pred.getAFalseSuccessor() then
skipsLoop = true
else
skipsLoop = false
exists(ControlFlowNode loop |
loopConditionAlwaysTrueUponEntry(loop, _) and
(
(
succ = loop.(Loop).getFollowingStmt() and
pred.getAFalseSuccessor() = succ and
skipsLoop = true
) or (
succ = loop.(Loop).getStmt() and
pred.getATrueSuccessor() = succ and
skipsLoop = false
)
)
)
}
@@ -176,7 +183,7 @@ predicate bbSuccessorEntryReachesLoopInvariant(BasicBlock pred, BasicBlock succ,
// The edge from `pred` to `succ` is _not_ from a loop condition provably
// true upon entry, so the values of `predSkipsFirstLoopAlwaysTrueUponEntry`
// and `succSkipsFirstLoopAlwaysTrueUponEntry` must be the same.
not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, _, _) and
not bbLoopConditionAlwaysTrueUponEntrySuccessor(pred, succ, _) and
succSkipsFirstLoopAlwaysTrueUponEntry = predSkipsFirstLoopAlwaysTrueUponEntry and
// Moreover, if `pred` contains the entry point of a loop where the
// condition is provably true upon entry, then `succ` is not allowed

View File

@@ -8,12 +8,7 @@
| test.cpp:132:9:132:9 | j | The variable $@ may not be initialized here. | test.cpp:126:6:126:6 | j | j |
| test.cpp:219:3:219:3 | x | The variable $@ may not be initialized here. | test.cpp:218:7:218:7 | x | x |
| test.cpp:243:13:243:13 | i | The variable $@ may not be initialized here. | test.cpp:241:6:241:6 | i | i |
| test.cpp:268:9:268:11 | val | The variable $@ may not be initialized here. | test.cpp:261:6:261:8 | val | val |
| test.cpp:292:9:292:11 | val | The variable $@ may not be initialized here. | test.cpp:285:6:285:8 | val | val |
| test.cpp:304:9:304:11 | val | The variable $@ may not be initialized here. | test.cpp:297:6:297:8 | val | val |
| test.cpp:316:9:316:11 | val | The variable $@ may not be initialized here. | test.cpp:309:6:309:8 | val | val |
| test.cpp:329:9:329:11 | val | The variable $@ may not be initialized here. | test.cpp:321:6:321:8 | val | val |
| test.cpp:336:10:336:10 | a | The variable $@ may not be initialized here. | test.cpp:333:7:333:7 | a | a |
| test.cpp:342:9:342:11 | val | The variable $@ may not be initialized here. | test.cpp:334:6:334:8 | val | val |
| test.cpp:369:10:369:10 | a | The variable $@ may not be initialized here. | test.cpp:358:7:358:7 | a | a |
| test.cpp:378:9:378:11 | val | The variable $@ may not be initialized here. | test.cpp:359:6:359:8 | val | val |

View File

@@ -265,7 +265,7 @@ int test23() {
val = 1;
loop = false;
}
return val; // GOOD [FALSE POSITIVE]
return val; // GOOD
}
int test24() {
@@ -289,7 +289,7 @@ int test25() {
val = 1;
loop = false;
}
return val; // GOOD [FALSE POSITIVE]
return val; // GOOD
}
int test26() {
@@ -301,7 +301,7 @@ int test26() {
val = 1;
loop = false;
}
return val; // GOOD [FALSE POSITIVE]
return val; // GOOD
}
int test27() {
@@ -313,7 +313,7 @@ int test27() {
val = 1;
loop = false;
}
return val; // GOOD [FALSE POSITIVE]
return val; // GOOD
}
int test28() {
@@ -339,7 +339,7 @@ int test29() {
b = false;
c = false;
}
return val; // GOOD [FALSE POSITIVE]
return val; // GOOD
}
int test30() {