dcoughlin added a comment.
Hi Sean,
Sorry it took me so long to get back to you.
================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:266
@@ +265,3 @@
+ /// \sa shouldWidenLoops
+ bool WidenLoops;
+
----------------
Is this field used?
================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1407
@@ +1406,3 @@
+ const CFGBlock *Following = getBlockAfterLoop(L.getDst());
+ if (Following && nodeBuilder.getContext().Eng.blockWasVisited(Following))
+ return;
----------------
What is the purpose of checking whether the block has already been visited by
some other path?
If I understand correctly, this will stop the analyzer from widening before the
"last" iteration through the loop and so will result in a sink after that
iteration. What this means is that we will never explore the code beyond the
loop in the widened state -- but isn't this the whole point of the widening?
So, for example, in your `variable_bound_exiting_loops_not_widened()` test,
don't we want the clang_analyzer_eval() statement after the loop to be
symbolically executed on 4 separate paths? That is, once when i is 0, once when
i is 1, once when i is 2 and once when i is $conj_i$ + 1 where $conj_i$ is the
value conjured for i when widening.
Also, in general, analysis of one path should not depend at all on whether
another path has been explored. This is because we want the analyzer to be free
choose different strategies about path exploration (e.g., BFS vs. DFS,
prioritizing some paths over others, etc.) without changing the issues reported
on along any given path. For this reason, I don't think we necessarily want to
track and expose `blockWasVisited()` on CoreEngine or use this to determine
when to permit a sink.
================
Comment at: lib/StaticAnalyzer/Core/LoopWidening.cpp:98
@@ +97,3 @@
+ RegionAndSymbolInvalidationTraits ITraits;
+ for (int RegionIndex = 0; RegionIndex < NumRegions; ++ RegionIndex) {
+ ITraits.setTrait(Regions[RegionIndex],
----------------
I get a warning here about comparing a signed int (RegionIndex) to an unsigned
(NumRegions).
I think you can avoid this and simplify things by using a range-based for loop:
```
const MemRegion *Regions[] = {
...
};
RegionAndSymbolInvalidationTraits ITraits;
for (auto *Region : Regions) {
...
}
```
http://reviews.llvm.org/D12358
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
