Annotate adds \old environment to non-static fields with JML format

[GualterP]

Hello,

When proving (using OpenJML) the attached example code, which is annotated with the results from running Annotate, the following errors occur:

error: Non-static fields are not allowed in \old environments in postconditions: cID @ ensures this.customerID == \old(cID);

error: Non-static fields are not allowed in \old environments in postconditions: oID @ ensures this.orderID == \old(oID);

The corresponding postconditions appear in:

/*@
@ public normal_behavior // Generated by Daikon
**@ ensures this.customerID == \old(cID);**
@ ensures this.order.orderID == -1;
@*/
public Customer(int cID) {
	this.customerID = cID;
	this.order = new Order(-1);
}

/*@
@ public normal_behavior // Generated by Daikon
@ requires oID >= -1;
**@ ensures this.orderID == \old(oID);**
@*/
public Order(int oID) {
	this.orderID = oID;
}

The expected results would be that Daikon's Annotate would output non-static fields without the \old environment:

    /*@
@ public normal_behavior // Generated by Daikon
**@ ensures this.customerID == cID;**
@ ensures this.order.orderID == -1;
@*/
public Customer(int cID) {
	this.customerID = cID;
	this.order = new Order(-1);
}

/*@
@ public normal_behavior // Generated by Daikon
@ requires oID >= -1;
**@ ensures this.orderID == oID;**
@*/
public Order(int oID) {
	this.orderID = oID;
}

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