Thank you!<br><br><div class="gmail_quote">On Sat, May 17, 2008 at 12:10 AM, Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div><div></div><div class="Wj3C7c"><br>
On May 16, 2008, at 7:32 AM, Zhongxing Xu wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I use GRCoreEngine to do a path sensitive analysis. For example, I can get two paths for the program below:<br>
<br>
int f(int n) {<br>
  if (n > 0)<br>
    ...<br>
  else<br>
    ...<br>
}<br>
<br>
I can use the nodes in EndNodes to get these two paths (by backtracking from endnodes).<br>
There are two BlockEdgeDst nodes after the block containing the IfStmt "if (n>0)".<br>
How can I know which path is led by the condition n > 0 or n <= 0? That is, how can I know which is the "true"/"false" branch edge?<br>
</blockquote>
<br></div></div>
Hi Zhongxing,<br>
<br>
You will want to inspect the successors CFBBlocks of the "source" in the BlockEdge, and compare it against the destination.  For CFGBlock's whose terminator is a branch (if statements, loops, etc), the first successor block is the true branch, the and second successor block is the false branch.  For example:<br>

<br>
<br>
ProgramPoint P = N->getLocation();  // N is an ExplodedNode<...><br>
<br>
if (BlockEdge* BE = dyn_cast<BlockEdge>(&P)) {<br>
<br>
  CFGBlock* Src = BE->getSrc();<br>
  CFGBlock* Dst = BE->getDst();<br>
<br>
  // Test if we are at a (binary) branch.<br>
  if (Src.hasBinaryBranchTerminator()) {<br>
<br>
    if (*Src.succ_begin() == Dst) {<br>
       // We took the true branch.<br>
    }<br>
    else {<br>
       assert (*(Src.succ_begin()+1) == Dst);<br>
       // We took the false branch.<br>
    }<br>
  }<br>
}<br>
<br>
Note that "hasBinaryBranchTerminator" only returns true for terminators that are "ForStmt", "WhileStmt", "DoStmt", "IfStmt", "ChooseExpr", "ConditionalOperator", and "BinaryOperator" (for '&&' and '||').  IndirectGotoStmt and SwitchStmt work differently.  IndirectGotoStmt always branches to a special block where the actual indirect goto takes place (do a CFG dump of code with a labeled goto to see what I mean).  Blocks that have a SwitchStmt terminator have as their successor blocks the targets of the switch.  In that case, each successor block should have "getLabel()" return a SwitchStmt, with the exception of the last successor.  The last successor is always the "default" branch, which may be explicit (with a "default:" label) or implicit (in the case of fall-through to the code after the switch block).<br>

<br>
BTW, "hasBinaryBranchTerminator" was a recently added predicate method.  Most code that inspects terminators actually uses a switch statement on the statement class of the terminator to handle both binary branches and other terminator types.<br>
<font color="#888888">
<br>
Ted<br>
</font></blockquote></div><br>