As I observed, if a (path sensitive) checker generates a sink node and another checker (or the same) generates other non-sink nodes (from the same predecessor) the analysis continues on the non-sink paths. This is not always the wanted operation, for example NoReturnFunctionChecker should stop analysis on all paths. Is it possible to achieve this behavior in a checker? Or we should change the code to stop analysis on all descendant nodes if (at least) one of them is sink node?
The only way to generate nodes from the same predecessor in two different checkers is to specify the wrong predecessor explicitly - eg., C.addTransition(State, C.getPredecessor()->getFirstPred());.
Normally C.getPredecessor() is chosen from the frontier nodes of the NodeBuilder, which are the nodes generated by the previous checker. So different checkers are chained together.
Because sink nodes don’t get put into the frontier, they don’t get sent to other checkers.
So i think we agree upon how it’s intended to work, but i don’t think i’ve observed any deviations from this behavior; could you give a concrete example?