[cfe-dev] Question about sink nodes

[Artem Dergachev via cfe-dev]

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?

On 10/28/19 6:43 AM, Balázs Kéri via cfe-dev wrote:
> Hi!
> 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?
>
> Balázs
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20191028/f0a080e7/attachment.html>