GualterP issues

Repositories
Issues
Comments

Results 2 issues of


                                            GualterP

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

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...

Annotate output missing invariant visibility with JML format

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...