Problems with Annotate and OpenJML

[GP]

Hello,

I've found some problems when running Annotate with invariants written in JML format. I'm using Daikon 5.8.0.

1 - Missing invariant visibility declaration

Daikon annotates private variables with /*@ spec_public */ in order for them to be used as public when proving the specification. However, invariants are written without a declared visibility (e.g. /*@ invariant this.var != null; */), defaulting to package. This leads OpenJML to produce visibility errors (An identifier with public visibility may not be used in a invariant clause with package visibility).

2 - Invariants with format var1 != null ==> \old(this.var2 != null) missing last parenthesis

Daikon annotates these invariants without the last parenthesis, e.g. "this.var1 != null ==> \old(this.var2 != null" or "var1.field != null ==> \old(this.var2 != null" 

3 - Adding pre and post-conditions about Daikon's internal behavior

I've only seen this happen in the Main method. 

It annotates pre-conditions such as: @ requires daikon.Quant.pairwiseEqual(daikon.Quant.collectObject(args, "toString()"), new String[] {  });

and post-conditions such as: @ ensures daikon.Quant.pairwiseEqual(daikon.Quant.collectObject(args, "toString()"), new String[] {  });

                                               @ ensures daikon.Quant.pairwiseEqual(args, \old(args));

If the annotated code is used by OpenJML outside Daikon's directory, it complains about not finding package daikon.

I have tried to solve these issues by experimenting some changes in various files inside daikon/java/daikon/tools/jtb, but so far to no success. 

Thank you.

[Michael Ernst]

Thanks for your message.  I am sorry you are having trouble.

Could you please submit a reproducible bug report?  That would include a tiny example for which Daikon produces incorrect results, all the commands needed to produce output, and a description (like the one in your message) of the results you expected.  The Daikon manual requests that you provide all this information when submitting a bug report.

Please submit bug reports using the issue tracker at https://github.com/codespecs/daikon/issues .  Please submit one bug report per issue.

                     Thanks,

                    -Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/5d2303e3-26a7-4c13-a01a-a3e2402416b3o%40googlegroups.com.