How to know which edge the path is traversing?

I use GRCoreEngine to do a path sensitive analysis. For example, I can get two paths for the program below:

int f(int n) {
if (n > 0)



I can use the nodes in EndNodes to get these two paths (by backtracking from endnodes).
There are two BlockEdgeDst nodes after the block containing the IfStmt “if (n>0)”.
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?

Hi Zhongxing,

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:

ProgramPoint P = N->getLocation(); // N is an ExplodedNode<...>

if (BlockEdge* BE = dyn_cast<BlockEdge>(&P)) {

   CFGBlock* Src = BE->getSrc();
   CFGBlock* Dst = BE->getDst();

   // Test if we are at a (binary) branch.
   if (Src.hasBinaryBranchTerminator()) {

     if (*Src.succ_begin() == Dst) {
        // We took the true branch.
     else {
        assert (*(Src.succ_begin()+1) == Dst);
        // We took the false branch.

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).

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.


Thank you!