[cfe-dev] [StaticAnalyzer] False positive with loop handling

[Dominic Chen via cfe-dev]

Hello,

I've been trying to track down a false positive with symbolic execution of an array assignment within a loop, but I'm having some trouble       figuring out the root cause. In the attached loop.c file, the analyzer identifies the LHS of the assignment equal operation on line 11 to be a garbage value, but this is actually initialized on line 6.
Initially, I thought that this was an issue with dead symbols being incorrectly purged, because the trimmed ExplodedGraph shows that the analyzer identifies the array "c" to be an ElementRegion "c: &element{c, 0 S64b,int}" in an earlier node before PreStmtPurgeDeadSymbols. But this is unchanged even after eliminating calls to collectNode(), so I'm confused if the graph is representing the actual symbolic execution exploration state, or just simply the ordering of explored states from the worklist?
The other place that I've been looking at is the branch condition handling inside ExprEngine::processBranch(). When the symbolic execution engine assumes either of the false/true branches, does that also entail the body of the loop?
Thanks,

Dominic
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20161019/86ed0b86/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: loop.c
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20161019/86ed0b86/attachment.c>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20161019/86ed0b86/attachment-0001.html>