JmlEclipseRunTests

[JmlEclipse] Developer Notes: Running Tests

• Ensure you have completed the setup.
• Run the following as a JUnit test, and consult the [JmlEclipseDeveloperJournal] to see if you get the expected number of passed tests:
  org.jmlspecs.eclipse.jdt.core.tests/src/org.jmlspecs.eclipse.jdt.core.tests/RunJmlEclipseStandardTests.java.

Running the tests will generate compiler warnings on the console (though the tests will still pass). This is because (non-local-variable) declarations are assumed to be non-null by default in JML. Unfortunately, this causes warnings to be issued when an auxiliary test file, used by the !JUnit test framework, VerifyTests is compiled using [JmlEclipse] is batch mode. To eliminate these errors add the following text to the inlined source of VerifyTests, just before the "public class VerifyTests" (on line 159 of file org.eclipse.jdt.core.tests.compiler/src/org/eclipse/jdt/core/tests/util/TestVerifier.java):

/@nullable_by_default/

so that lines 159 and 160 look like this

  "/*@nullable_by_default*/\n" +
  "public class !VerifyTests {\n" +

(Actually, this doesn't eliminate all warnings, but most.)