
<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii">


    <meta http-equiv="content-type" content="text/html; charset=utf-8">

  </head><body bgcolor="#FFFFFF" text="#000000" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">

    <p class="">Hello,</p>

    <p class="">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.<br class="">

    </p>

    <p class="">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?<br class="">

    </p>

    <p class="">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?<br class="">

    </p>

    <p class="">Thanks,</p>

    <p class="">Dominic<br class="">

    </p>

  
</body></html>