Annotate output missing invariant visibility with JML format

[GualterP]

Hello,

When executing Annotate with JML format, the annotated class invariants are missing their visibility. Annotate adds /*@spec_public */ to private variables in order for them to be used as public when proving the specification. Since the invariants' visibility is missing, when using the annotated code as input in OpenJML, their visibility defaults to package. This creates inconsistencies when proving programs.

Here is an excerpt example of this problem, using the attached code:

/*@ invariant this.customerID >= 1; / /@ invariant this.order != null; / ... /@ spec_public / private int customerID; /@ spec_public */ private Order order;

As is, we have package invariants over public variables. In OpenJML, the following error is obtained when proving this program: "An identifier with public visibility may not be used in a invariant clause with package visibility".

The expected result would be: /*@ public invariant this.customerID >= 1; / /@ public invariant this.order != null; / ... /@ spec_public / private int customerID; /@ spec_public */ private Order order;

The following commands were used in order to obtain the shown results: javac -g *.java java -cp .:$DAIKONDIR/daikon.jar daikon.DynComp Tester java -cp .:$DAIKONDIR/daikon.jar daikon.Chicory --daikon --comparability-file=Tester.decls-DynComp Tester java -cp .:$DAIKONDIR/daikon.jar daikon.tools.jtb.Annotate --format jml Tester.inv.gz Customer.java Order.java

I am using Daikon 5.8.0 with Java 11, in Ubuntu 18.04.

Thank you. example.zip

[markro49]

Thanks for submitting an issue. We hope to investigate shortly.