This patch add a new ProgramPoint PostCondition to represent the post position of a branch condition, and a new generateNode method to BranchNodeBuilder using PostCondition ProgramPoint. This method generate a new ExplodedNode but not a new block edge.<br>
<br>This patch is preparation for statistical UncheckedRenturn checker.<br clear="all"><br>I'll appreciate it if there are any advice about this patch.<br clear="all"><br>-- <br>Best regards!<br><br>Lei Zhang<br>