core JDK specs wrong/missing?

[atiti]

Attempting to check a minimal Java class results in an purity error. What specs are shipped with the OpenJML upon which Beetlz depends?

{{{ package testpackage;

public class TestClass { //@ public invariant 0 <= i; public int i; //@ protected invariant b <= 0; protected byte b; //@ invariant 0 < s.length(); /_@ nonnull @/ String s = " "; /@ nullable @/ private Object o;

/**
 * @param args the command-line arguments.
 */
public static void main(/*@ non_null @*/ String[] args) {
    // TODO Auto-generated method stub

}

} }}}

Error message: {{{

Old classpath: /Applications/Eclipse-3.5-x86_64-PVE/plugins/org.eclipse.equinox.launcher_1.0.201.R35x_v20090715.jar Added: /Local/Sandboxes/workspace_ebon/Beetlz/lib/openjml.jar Added: /Applications/Eclipse-3.5-x86_64-PVE/plugins/org.eclipse.equinox.launcher_1.0.201.R35x_v20090715.jar New classpath: :/Local/Sandboxes/workspace_ebon/Beetlz/lib/openjml.jar:/Applications/Eclipse-3.5-x86_64-PVE/plugins/org.eclipse.equinox.launcher_1.0.201.R35x_v20090715.jar: /Users/kiniry/Documents/workspace-empty/Test/src/testpackage/TestClass.java:8: warning: A non-pure method is being called where it is not permitted: length() //@ invariant 0 < s.length(); ^ Checking direction Java -> BON Checking direction BON -> Java -> General Notes: BON and Java have different default frame conditions: in BON all queries are automatically pure, whereas in Java the default is 'assignable \everything'. -> Java Errors: -> Java Warnings: -> Jml Errors: bon_skeleton.bon:7: TEST_CLASS is missing these invariant clauses: 0 <= i b <= 0 0 < s.count -> Jml Warnings: 0 Java errors, 0 Java warnings, 1 JML errors and 0 JML warnings found. }}}

[atiti]

From: fintan (GH: fintanf) Date: Tue Nov 17 13:31:19 2009

I can confirm this bug.

It seems that saying -specs /path/to/openjml.jar does not give us what we want (it did before).

Not using -specs at all (which presumably uses the specs built into openjml.jar) or using -specs /path/to/jmlspecs.jar (built by openjml build script) has a different effect, but a lot of other errors.

I'll drop David an email and check if we're doing something wrong.

[atiti]

From: fintan (GH: fintanf) Date: Tue Nov 17 15:24:05 2009

Fixed in [75354].