Hi JML Developers!
I'm working on including the JML2 tools into Eclipse.
A first somewhat usable version is available at
http://www.sct.inf.ethz.ch/research/universes/tools/eclipse/
Comments very welcome.
I am executing the JML tools within the same JVM as Eclipse, which
is faster than starting a new JVM every time.
But I run into the following problem with the JML RAC, that can
hopefully be reproduced by the following steps.
x Build MJ/JML2 and put everything in the CLASSPATH, but do
not have the "specs" subdir on the classpath.
x Compile the attached JmlBugSimple.java with the normal Java compiler
Put the attached file Small.java in the current directory.
x Execute
$JAVA JmlBugSimple -S xxx/JML2/specs:. Small.java
x You should see something like:
Checker 1
parsing Small.java
parsing xxx/JML2/specs/java/lang/Object.jml
parsing xxx/JML2/specs/java/lang/reflect/Array.refines-spec
...
Result: true
RAC
parsing Small.java
typechecking Small.java
...
parsing ../../tmp/jmlrac51498.java
typechecking Small.java
Result: true
Checker 2
parsing Small.java
typechecking Small.java
File "Small.java", line 3, character 32 error: Cannot find field "objectState" [JLS2 15.11]
Result: false
The first time the checker is called everything works fine, then the RAC
still works ok. But the next run of the checker sees some side-effects from
the vious runs and does not find the "specs" files any more.
I looked at all methods that sound like they would reset the compiler and call
them in the clearJmlState method, but no difference.
Does anyone know which class I forget to reset?
Any hints would be greatly apciated!
Cheers,
cu, WMD.
____________________________________________________________________________________
Never miss a thing. Make Yahoo your home page.
http://www.yahoo.com/r/hs
|
