search

kiniry / Mobius

4 stars 8 forks source link

Re: Partial ESC/Java2 2.0.7 success, but still a problem #523

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

On 2 Mar 2009, at 20:49, Mark Sebern wrote:

Joe --

I am continuing to work on this. I don't think I can use the new
plugin version (2.0.8) now, since I understand from Dermot that the
"feature" file currently does not bring in the correct
"mobius.escjava2_2.0.8.jar" (?) and I have not yet figured out how
to get that one.

The source file feature.xml appears to be correct; the mismatch only
appears in the built feature as published on the update site.

In working with the 2.0.7 plugin and the "jmlspecs" project, I am
continuing to have the previously noted problems with possible JRE
version conflicts. I tried connecting newer versions of the JML
specs to the "jmlspecs" project, but had to manually rename the
directory containing the "old" specs (libs/specs/escspecs- java1.4.jar) to keep them from being used. I haven't figured out
exactly where those specs are added to the ESC2 path, but that
probably explains why ESC2 would still run with NO specs in the
"jmlspecs" project.

[Warning: the following description is rather long, but I didn't
want to omit anything that might be relevant. The bottom line is
that I have not yet found any way to use other specifications to
make the ESC2 plugin work with JRE1.5/1.6, although I can
successfully run the same (pretty simple) code through the GUI
version of ESC2 2.0.5 with only minor warnings about library specs.
This seems to imply that there is something about the Eclipse
environment or plugin that is responsible for the more serious
problems. Also, the same code seems so far to work OK with JRE1.6
and the JML2 Eclipse plugin.]

In trying to take your suggestion about more recent JML2 specs, I
have run into the following:

1) With the "stock" ESC2 "escspecs" from the 2.0.7 plugin, I get
the following results with different JREs:

[JRE1.5 or JRE1.6](as previously noted)

C:\Program Files (x86)\Java\jre1.5.0_15\lib\rt.jar:java/io/ PrintStream.class: Error: Different or incompatible return types on

overridden(hidden) and overriding(hiding) methods

  • All I have to do to get this is to have the declaration
    "PrintStream xx;" in my source Java file.

There might be a JML annotation that suppresses this kind of warning
e.g. "@nowarn"

[JRE1.4.2]

* Mostly works, but gives the following errors on a library spec:

C:\eclipse\plugins\mobius.escjava2.esctools2.0.8\libs\specs \escspecs-java1.4.jar:java/io/OutputStream.refines-java:65:
Caution: No initial also expected since there are no overridden or
refined methods /@ also public behavior ^ C:\eclipse\plugins\mobius.escjava2.esctools2.0.8\libs\specs \escspecs-java1.4.jar:java/io/OutputStream.refines-java:76:
Caution: No initial also expected since there are no overridden or
refined methods /@ also public behavior

^

2) With the JML5.6rc3 specs linked to the "jmlspecs" project:

[JRE1.4.2] Works as in (1) above; same warnings.

[JRE1.5 or JRE1.6]

* As previously reported, still get the error:

C:\Program Files (x86)\Java\jre1.5.0_15\lib\rt.jar:java/io/ PrintStream.class: Error: Different or incompatible return types on

overridden(hidden) and overriding(hiding) methods

3) With JML5.6rc3 specs linked to "jmlspecs" project, and "escjava"
specs directory RENAMED to keep it from being used:

[JRE1.4.2 or JRE1.5 or JRE1.6]

Failed to locate specifications at: libs/specs/escspecs-java1.4.jar
in plugin mobius.escjava2.esctools Failed to locate specifications at: libs/specs/escspecs-java1.4.jar
in plugin mobius.escjava2.esctools ESC/Java version ESCJava-2.0b4 [0.078 s 68466424 bytes]

edu.msoe.se3811.elevator.model.Elevator ... C:\JML\specs\java\lang\Object.jml:39: Fatal error: Can't find type
named "JMLDataGroup" //@ public model non_null JMLDataGroup objectState;

^

4) Like (3) but with the JML5.6rc3 specs copied to another location
and "org/jmlspecs/lang" JMLDataGroup.java and JMLSetType.java specs
added to the tree:

[JRE1.4.2 or JRE1.5 or JRE1.6]

Failed to locate specifications at: libs/specs/escspecs-java1.4.jar
in plugin mobius.escjava2.esctools Failed to locate specifications at: libs/specs/escspecs-java1.4.jar
in plugin mobius.escjava2.esctools ESC/Java version ESCJava-2.0b4 [0.015 s 118377232 bytes]

edu.msoe.se3811.elevator.model.Elevator ... D:\Courses\SE3811\ESC-JAVA2\hacks\specs\java\lang\Throwable.jml: 161: Error: No such method infixConcat(java.lang.String,
java.lang.String) in type java.lang.String ... t.equals(this.getClass().theString + ": " + _message); ^ D:\Courses\SE3811\ESC-JAVA2\hacks\specs\java\lang\Throwable.jml: 161: Error: No method valueOf(error) matching given argument types ... t.equals(this.getClass().theString + ": " + _message); ^ D:\Courses\SE3811\ESC-JAVA2\hacks\specs\java\lang\Throwable.jml: 161: Error: No such method infixConcat(error, java.lang.String)
in type java.lang.String ... s(this.getClass().theString + ": " + _message); ^ D:\Courses\SE3811\ESC-JAVA2\hacks\specs\java\lang\Throwable.jml: 161: Error: No method equals(error) matching given argument types @ ensures _message != null ==> \result.equals(this.getClass (). ... ^ Exception javafe.util.AssertionFailureException thrown while
processing edu.msoe.se3811.elevator.model.Elevator javafe.util.AssertionFailureException at javafe.util.Assert.notNull(Assert.java:53) at javafe.ast.ASTDecoration.get(ASTDecoration.java:87) at escjava.ast.Utils$BooleanDecoration.isTrue(Utils.java:127) at escjava.ast.Utils.isPure(Utils.java:145) at escjava.AnnotationHandler$CheckPurity.visitNode (AnnotationHandler.java:1237) at escjava.AnnotationHandler$CheckPurity.visitNode (AnnotationHandler.java:1288) at escjava.AnnotationHandler$CheckPurity.visitNode (AnnotationHandler.java:1288) at escjava.AnnotationHandler$CheckPurity.visitNode (AnnotationHandler.java:1273) at escjava.AnnotationHandler.process(AnnotationHandler.java:204) at escjava.AnnotationHandler.process(AnnotationHandler.java:169) at escjava.tc.FlowInsensitiveChecks.checkTypeDeclElem (FlowInsensitiveChecks.java:228) at javafe.tc.FlowInsensitiveChecks.checkTypeDeclaration (FlowInsensitiveChecks.java:199) at escjava.tc.FlowInsensitiveChecks.checkTypeDeclaration (FlowInsensitiveChecks.java:164) at javafe.tc.TypeSig.typecheck(TypeSig.java:1120) at escjava.backpred.FindContributors.typecheck (FindContributors.java:714) at escjava.backpred.FindContributors.addType (FindContributors.java:217) at escjava.backpred.FindContributors.addType (FindContributors.java:224) at escjava.backpred.FindContributors.walk(FindContributors.java: 389) at escjava.backpred.FindContributors.walk(FindContributors.java: 465) at escjava.backpred.FindContributors.walk(FindContributors.java: 465) at escjava.backpred.FindContributors.backedgeToRoutineDecl (FindContributors.java:692) at escjava.backpred.FindContributors.walk(FindContributors.java: 441) at escjava.backpred.FindContributors.walk(FindContributors.java: 465) at escjava.backpred.FindContributors.walk(FindContributors.java: 351) at escjava.backpred.FindContributors. (FindContributors.java:54) at escjava.Main.processTD(Main.java:580) at escjava.Main.handleTD(Main.java:514) at javafe.SrcTool.handleCU(SrcTool.java:303) at escjava.Main.handleCU(Main.java:467) at javafe.SrcTool.handleAllCUs(SrcTool.java:248) at javafe.SrcTool.frontEndToolProcessing(SrcTool.java:116) at javafe.FrontEndTool.run(FrontEndTool.java:271) at escjava.Main.compile(Main.java:242) at escjava.plugin.EscjavaChecker.run(EscjavaChecker.java:237) at escjava.plugin.EscjavaAction$Check.checkCompilationUnit (EscjavaAction.java:485) at escjava.plugin.EscjavaAction$Check.checkJavaElement (EscjavaAction.java:411) at escjava.plugin.EscjavaAction$Check.run(EscjavaAction.java:380) at org.eclipse.ui.internal.PluginAction.runWithEvent (PluginAction.java:251) at
org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection( ActionContributionItem.java:583) at org.eclipse.jface.action.ActionContributionItem.access$2 (ActionContributionItem.java:500) at org.eclipse.jface.action.ActionContributionItem$5.handleEvent (ActionContributionItem.java:411) at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java: 84) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1003) at org.eclipse.swt.widgets.Display.runDeferredEvents (Display.java:3823) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java: 3422) at org.eclipse.ui.internal.Workbench.runEventLoop (Workbench.java:2382) at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2346) at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2198) at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:493) at org.eclipse.core.databinding.observable.Realm.runWithDefault (Realm.java:288) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench (Workbench.java:488) at org.eclipse.ui.PlatformUI.createAndRunWorkbench (PlatformUI.java:149) at org.eclipse.ui.internal.ide.application.IDEApplication.start (IDEApplication.java:113) at org.eclipse.equinox.internal.app.EclipseAppHandle.run (EclipseAppHandle.java:193) at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplic ation(EclipseAppLauncher.java:110) at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start (EclipseAppLauncher.java:79) at org.eclipse.core.runtime.adaptor.EclipseStarter.run (EclipseStarter.java:386) at org.eclipse.core.runtime.adaptor.EclipseStarter.run (EclipseStarter.java:179) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source) at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source) at java.lang.reflect.Method.invoke(Unknown Source) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java: 549) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:504) at org.eclipse.equinox.launcher.Main.run(Main.java:1236) 0.671 s 126110176 bytes total

4 errors

  • I understand that not handling infix String concatenation is a
    known issue, but the last error (crash) was not clear. This type of
    error persisted even when I commented out THE ENTIRE CLASS BODY.

5) Like (3), but with "jmlspecs" project linked to the ESC2 2.0.5
"specs" directory instead of to the JML2 specs:

  • Same results as case (1). However, when I run the GUI version of
    ESC2 2.0.5 on the same source file (outside of Eclipse, of course),
    I get warnings and errors that are consistent with expected
    results, and no crash. In addition to the warnings/errors on my own code, I also get the
    following output (which I'm not too worried about) on a different
    source file that uses an ArrayList:

    /ESCJava2/specs/java/util/List.spec:58: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: /@ also ^ /ESCJava2/specs/java/util/Collection.spec:122: Associated declaration: /_@ also public normal_behavior ^ /ESCJava2/specs/java/util/List.spec:70: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: /@ also ^ /ESCJava2/specs/java/util/Collection.spec:143: Associated declaration: /_@ public normal_behavior ^ /ESCJava2/specs/java/util/List.spec:80: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: /@ also ^ /ESCJava2/specs/java/util/Collection.spec:155: Associated declaration: /_@ public normal_behavior ^ /ESCJava2/specs/java/util/ArrayList.spec:112: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: /@ also ^ /ESCJava2/specs/java/lang/Object.spec:97: Associated declaration: /_@ protected normal_behavior ^ /ESCJava2/specs/java/util/ArrayList.spec:126: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: public /@ pure @/ Object[] toArray(); ^ /ESCJava2/specs/java/util/Collection.spec:143: Associated declaration: /@ public normal_behavior ^ /ESCJava2/specs/java/util/ArrayList.spec:129: Caution: The nullable
    annotation (explicit or implicit) is ignored because this method
    overrides a method declared nonnull: public Object[] toArray(Object[] a); ^ /ESCJava2/specs/java/util/Collection.spec:155: Associated declaration: /@ public normal_behavior ^ /ESCJava2/specs/java/util/AbstractList.spec:75: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public /@ pure @/ Iterator iterator(); ^ /ESCJava2/specs/java/util/Collection.spec:122: Associated declaration: /@ also public normal_behavior ^ /ESCJava2/specs/java/util/AbstractList.spec:77: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public /@ pure @/ ListIterator listIterator(); ^ /ESCJava2/specs/java/util/List.spec:346: Associated declaration: /@ pure @/ /@ nonnull @/ ListIterator listIterator(); ^ /ESCJava2/specs/java/util/AbstractList.spec:80: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public /@ pure @/ ListIterator listIterator(final int index); ^ /ESCJava2/specs/java/util/List.spec:364: Associated declaration: /@ pure @/ /@ nonnull @/ ListIterator listIterator(int
    index) ... ^ /ESCJava2/specs/java/util/AbstractCollection.jml:39: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public abstract /@ pure @/ Iterator iterator(); ^ /ESCJava2/specs/java/util/Collection.spec:122: Associated declaration: /@ also public normal_behavior ^ /ESCJava2/specs/java/util/AbstractCollection.jml:51: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public /@ pure @/ Object[] toArray(); ^ /ESCJava2/specs/java/util/Collection.spec:143: Associated declaration: /@ public normal_behavior ^ /ESCJava2/specs/java/util/AbstractCollection.jml:54: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared nonnull: public Object[] toArray(Object[] a); ^ /ESCJava2/specs/java/util/Collection.spec:155: Associated declaration: /@ public normal_behavior ^ /ESCJava2/specs/java/util/AbstractCollection.jml:84: Caution: The
    nullable annotation (explicit or implicit) is ignored because this
    method overrides a method declared non_null: public String toString(); ^ /ESCJava2/specs/java/lang/Object.spec:166: Associated declaration: /*@ public normal_behavior ^

Don't know if this will help you at all. I am afraid I am going to
have to give up and go back to the stand-alone GUI for ESC2 unless
I can figure this out very quickly. (And hope that the JML2 Eclipse
plugin keeps working as I try more complex things.)

Thanks for the feedback.

The strange (to me) thing is that I think I have come close to
duplicating the environment that works for you, unless the
difference is that you are only trying to use JRE1.4.2.

Thanks for your help.

-- Mark

Joseph Kiniry wrote:

Mark,

As Dermot mentioned, this is due to the fact that the JML specs
for Java >=1.5 are still evolving, and the snapshot that ships
with ESC/Java2 is somewhat out-of-date. The purpose of the
jmlspecs project that gets automatically created is that one can
copy the JML specs for the JDK from more recent versions of the
JML2 tool suite into that project and ESC/Java2 will automatically
use them. Please let us know how this goes for you.

Joe

On 1 Mar, 2009, at 4:50, Mark Sebern wrote:

Joe (and Dermot) --

A little more information before I give up for the evening:

1) I don't know why the JML specifications failed to install (or
at least that message was generated), but I did manually add the
"libs/specs" plugin folder as a source folder (! -- got this
clue from the plugin source code, but may have misinterpreted it)
to the "jmlspecs" project build path. Whether that really changed
anything, related to the errors, I am not sure. Even before I
made this change, it seemed that the "failed to install specs"
message appeared only on the first try, before the "jmlspecs"
project was created.

2) By enabling some extra error reporting, I got a clue that the
"locToOffset" exception may have something to do with an error
message formatting problem, perhaps related to finding an ESC
error in the Java runtime library. I switched to a 1.5 JRE and
compiler specification, even though I'm not sure that is still
required. In any case, I got some errors like these:

ESC/Java version ESCJava-2.0b4 [0.0080 s 77139040 bytes]

edu.msoe.se3811.elevator.model.ElevatorSystem ... C:\Program Files (x86)\Java\jre1.5.0_15\lib\rt.jar:java/lang/ AbstractStringBuilder.class: Error: Different or incompatible
return types on overridden(hidden) and overriding(hiding) methods Exception javafe.util.AssertionFailureException: Precondition
violated: locToOffset passed a whole-file location thrown while
processing edu.msoe.se3811.elevator.model.ElevatorSystem javafe.util.AssertionFailureException: Precondition violated:
locToOffset passed a whole-file location at javafe.util.Assert.precondition(Assert.java:79) at javafe.util.LocationManagerCorrelatedReader.locToOffset (LocationManagerCorrelatedReader.java:326) at javafe.util.Location.toOffset(Location.java:118) at escjava.plugin.EscjavaChecker.report(EscjavaChecker.java:83) at javafe.util.ErrorSet.report(ErrorSet.java:409) at javafe.util.ErrorSet.error(ErrorSet.java:238) at javafe.tc.PrepTypeDeclaration.addInheritedMembers (PrepTypeDeclaration.java:809) at escjava.tc.PrepTypeDeclaration.addInheritedMembers (PrepTypeDeclaration.java:313)

...

... C:\Program Files (x86)\Java\jre1.5.0_15\lib\rt.jar:java/io/ PrintStream.class: Error: Different or incompatible return types
on overridden(hidden) and overriding(hiding) methods

...

These errors immediately preceded the "locToOffset" precondition
exceptions.

I haven't gotten very far in figuring out the cause of these
errors; could it be some kind of inconsistency between the JML
specs and the JRE?

Your suggestions are welcome. Sorry to cause so much trouble.

-- Mark

Mark Sebern wrote:

Joe (and Dermot) --

Picking up on your suggestion about loading the plugins
manually, I tried two different ways to install ESC2 2.0.7 (not
2.0.8):

1) Downloaded and unpacked JARs from various places to get the
set of directories you had listed as being on your Mac, and then
restarted Eclipse with "-clean".

2) Downloaded the "mobius.Escjava2.feature_2.0.7.jar" feature
JAR and used it to reference the repository at "http:// kind.ucd.ie/products/opensource/ESCJava2/escjava-eclipse/updates".

In both cases, using a clean install of Eclipse on Vista, I was
able to get the "Window->Preferences" page with "Java->ESC/ Java2" and set the "use internal Simplify version" as you
suggested.

The remaining problem I have now is that, when executing ESC/ Java2, the "jmlspecs" project is created and linked into the
target project, but I then get a crash with the exception:

Failed to install the JML specifications Exception javafe.util.AssertionFailureException: Precondition
violated: locToOffset passed a whole-file location thrown while
processing edu.msoe.se3811.elevator.model.Elevator javafe.util.AssertionFailureException: Precondition violated:
locToOffset passed a whole-file location

...

This closely resembles the tickets:

1) https://mobius.ucd.ie/trac/ticket/475 (closed on "works for me") 2) https://mobius.ucd.ie/trac/ticket/633 (opened "7 months ago")

It looks to me like an attempt is being made to add the
"jmlspecs" tree to the project, but it is failing. I tried
adding the "specs" directory and/or "escspecs.jar" to the path
of "jmlspecs", with no improvement.

Compared to the 2.0.8 version, the 2.0.7 version seems much
closer to working, but obviously this "jmlspecs" issue remains
an obstacle. (I also installed the JML2 tools, to see if there
was some dependency on them, but there were no apparent changes
in the failure.)

I'll keep looking, but any pointers would be appreciated.

Thanks.

-- Mark

-- Dr. Mark J. Sebern, PE Professor and Program Director, Software Engineering Electrical Engineering and Computer Science Department Milwaukee School of Engineering EECS Department, L-333 1025 N. Broadway Milwaukee, WI 53202-3109 Voice: 414-277-7213 FAX: 414-277-7465 http://people.msoe.edu/~sebern/ http://www.msoe.edu/eecs/se/ (software engineering) Email: sebern@msoe.edu

Dr. Mark J. Sebern, PE Professor and Program Director, Software Engineering Electrical Engineering and Computer Science Department Milwaukee School of Engineering EECS Department, L-333 1025 N. Broadway Milwaukee, WI 53202-3109 Voice: 414-277-7213 FAX: 414-277-7465 http://people.msoe.edu/~sebern/ http://www.msoe.edu/eecs/se/ (software engineering) Email: sebern@msoe.edu

Dr. Mark J. Sebern, PE Professor and Program Director, Software Engineering Electrical Engineering and Computer Science Department Milwaukee School of Engineering EECS Department, L-333 1025 N. Broadway Milwaukee, WI 53202-3109 Voice: 414-277-7213 FAX: 414-277-7465 http://people.msoe.edu/~sebern/ http://www.msoe.edu/eecs/se/ (software engineering) Email: sebern@msoe.edu

}}}

[attachment:"untitled-part.html"]

atiti commented 11 years ago

From: Dermot Cochran (GH: None) Date: Tue Mar 3 12:53:39 2009

This message has 1 attachment(s)

atiti commented 11 years ago

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted

atiti commented 11 years ago

From: kiniry (GH: kiniry) Date: Fri Apr 30 10:56:44 2010

I believe that these problems were all corrected in Julien's final work on getting ESC/Java2 to work with Java 1.5 and 1.6 API specs and bytecode.