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)
…
else
…
}
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.
Ted