How to interpret daikon output node[].skip[0] elements != null

[naveed ul Mustafa]

Hi all,

Can you please let me know how interpret following ooutput from daikon

node[].skip[0] elements != null

Does it mean that for all elements of node, skip pointer field is never NULL? If yes, the reported invariant is not true. Is it normal that invariants reported by Daikon are actually not satisfied by the workload?

Please note that I have set --config_option daikon.inv.Invariant.confidence_limit=0.99 for running daikon.

Thank you

[Michael Ernst]

Can you please let me know how interpret following ooutput from daikon

node[].skip[0] elements != null

Please see Chapter 5, "Daikon output", of the Daikon user manual.

In particular, see Section 5.3, "Variable names"; that explains the "node[]" notation, which can be a bit confusing.

In your case, the invariant means the skip field of the first element of nodes is a collection, and that collection never contains null.

Does it mean that for all elements of node, skip pointer field is never NULL? If yes, the reported invariant is not true. Is it normal that invariants reported by Daikon are actually not satisfied by the workload?

No, that is not what it means. Regarding your section question, ss also noted in Chapter 5, a reported property was always true in the observed samples (the execution or trace file).  If you ever observe that to be false, that is a bug in Daikon; please report it.

Mike