Question about sink nodes

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Question about sink nodes

Kristof Beyls via cfe-dev
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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Question about sink nodes

Kristof Beyls 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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev