#396 openjml rac extended class

[fithwith]

hi all,
my config is:
-eclipse juno
-openjml eclipse plugin v 0.2.7

i have two class Person and Child when i want rac class Child an error occur but no error with Person class, the rac of Person class works perfectly

so my probleme is with Child class, i did some test and i noticed that when i delete "extends Parent" from child class the rac works perfectly

the error:

INVALID COMMAND LINE: return code = 4 Command: -rac -d F:/Dev_Project/eclipse/JMLTest/bin -source 1.7 -noPurityCheck -showNotImplemented -noInternalSpecs -noInternalRuntime -nonnullByDefault -specspath ;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java7;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java6;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java5;F:\eclipse\configuration\org.eclipse.osgi\bundles\950\2\.cp\java4 -classpath F:/Dev_Project/eclipse/JMLTest/src;C:/Program Files/Java/jre7/lib/resources.jar;C:/Program Files/Java/jre7/lib/rt.jar;C:/Program Files/Java/jre7/lib/jsse.jar;C:/Program Files/Java/jre7/lib/jce.jar;C:/Program Files/Java/jre7/lib/charsets.jar;C:/Program Files/Java/jre7/lib/jfr.jar;C:/Program Files/Java/jre7/lib/ext/access-bridge-64.jar;C:/Program Files/Java/jre7/lib/ext/dnsns.jar;C:/Program Files/Java/jre7/lib/ext/jaccess.jar;C:/Program Files/Java/jre7/lib/ext/localedata.jar;C:/Program Files/Java/jre7/lib/ext/sunec.jar;C:/Program Files/Java/jre7/lib/ext/sunjce_provider.jar;C:/Program Files/Java/jre7/lib/ext/sunmscapi.jar;C:/Program Files/Java/jre7/lib/ext/zipfs.jar;F:/eclipse/plugins/org.jmlspecs.OpenJMLUI_0.2.7/jmlruntime.jar;/;F:\eclipse\plugins\org.jmlspecs.OpenJMLUI_0.2.7\bin\..\jmlruntime.jar -dirs F:/Dev_Project/eclipse/JMLTest/src/PersonChild/Child.java

[fithwith]

Child class

[fithwith]

Person class

[fithwith]

the 2 class are attached