search

kiniry / Mobius

4 stars 8 forks source link

Fwd: ESCJava bugs #343

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

!html

Reply to: Dermot Cochran }}} {{{

Begin forwarded message:

From: Wojciech Mostowski woj@cs.ru.nl Date: February 14, 2008 2:00:20 PM GMT+00:00 To: Dermot Cochran Dermot.Cochran@ucd.ie Subject: Re: ESCJava bugs

Attached. The specs for the -specs option are in the zip file. The
file giving the exception is EFEntry.java. DFEntry.java also fails
in a weird way.

(Note that the specs in EF/DFFile are work in progress and may not
even be valid/parsable JML, still the error messages I get from ESC/ Java2 are not comprehensible).

/Wojtek

Dermot Cochran wrote:

On Feb 14, 2008, at 1:28 PM, Wojciech Mostowski wrote:

Dermot Cochran wrote:

You can file bugs using the Mobius Trac: https://mobius.ucd.ie of by email: mobius-ticket@mobius.ucd.ie Which version of ESC/Java2 were you using?

Just downloaded the newest I could find - 2.0b4.

/Wojtek

On Feb 14, 2008, at 12:43 PM, Wojciech Mostowski wrote:

Hi Joe & Dermot,

Where do I officially file ESCJava bugs? Any bug tracking page
somewhere, quick browse through the ks pages did not bring
anything. Starting a small project now and already encountered
one (see below), will probably collect more.

Cheers,

Wojtek

I got this exception:

Exception java.lang.ClassCastException: javafe.ast.ArrayType
thrown while processing sos.enikapplet.EFEntry Can you attach/send a copy of the Java file that you are working
with. Which version of Java are you using and which operating system? java.lang.ClassCastException: javafe.ast.ArrayType at escjava.translate.Frame$ModifiesIterator.add (Frame.java:1113) at escjava.translate.Frame$ModifiesIterator.next (Frame.java:1035) at escjava.translate.GetSpec.trMethodDecl(GetSpec.java: 490) at escjava.translate.GetSpec.getCommonSpec(GetSpec.java: 87) at escjava.translate.GetSpec.getSpecForCall (GetSpec.java:36) at escjava.translate.Translate.call(Translate.java:3933) at escjava.translate.Translate.trConstructorCallStmt (Translate.java:2171) at escjava.translate.Translate.trConstructorBody (Translate.java:390) at escjava.translate.Translate.trBody(Translate.java:242) at escjava.Main.computeBody(Main.java:1330) at escjava.Main.processRoutineDecl(Main.java:801) at escjava.Main.processTypeDeclElem(Main.java:697) at escjava.Main.processTD(Main.java:641) 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.Main.main(Main.java:197)

Wojciech Mostowski Radboud University Nijmegen Department of Computing Science P.O. Box 9010, 6500 GL Nijmegen, The Netherlands e-mail: woj@cs.ru.nl www: http://www.cs.ru.nl/~woj/ phone: +31-24-365 2076 fax: +31-24-365 2298

Dermot Cochran Dermot.Cochran@ucd.ie Systems Research Group School of Computer Science & Informatics UCD CASL 8 Belfield Office Park Clonskeagh Dublin 4, Ireland Tel: +353-1-716-5349

Wojciech Mostowski Radboud University Nijmegen Department of Computing Science P.O. Box 9010, 6500 GL Nijmegen, The Netherlands e-mail: woj@cs.ru.nl www: http://www.cs.ru.nl/~woj/ phone: +31-24-365 2076 fax: +31-24-365 2298

Dermot Cochran Dermot.Cochran@ucd.ie Systems Research Group School of Computer Science & Informatics UCD CASL 8 Belfield Office Park Clonskeagh Dublin 4, Ireland Tel: +353-1-716-5349

Wojciech Mostowski Radboud University Nijmegen Department of Computing Science P.O. Box 9010, 6500 GL Nijmegen, The Netherlands e-mail: woj@cs.ru.nl www: http://www.cs.ru.nl/~woj/ phone: +31-24-365 2076 fax: +31-24-365 2298 Dermot Cochran Dermot.Cochran@ucd.ie Systems Research Group School of Computer Science & Informatics UCD CASL 8 Belfield Office Park Clonskeagh Dublin 4, Ireland Tel: +353-1-716-5349

}}}

atiti commented 11 years ago

From: Dermot Cochran (GH: None) Date: Thu Feb 14 15:10:27 2008

added mailto line

This message has 3 attachment(s)

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Thu Feb 14 15:18:27 2008

Logging is now on ESC/Java2 plugin is starting Builder mobius.escjava2.plugin.autocheckEscjavaBuilder added to problem_test enabled Specs project already exists - jmlspecs Installed specs as project in project problem_test ESC/Java2 Nature added - problem_test Completed Enable Esc/Java operation Thu Feb 14 14:16:36 GMT 2008 Doing project problem_test 1 items Completed Enable Esc/Java action Thu Feb 14 14:16:42 GMT 2008 Running Escjava checker Specs project already exists - jmlspecs Specs library already installed /jmlspecs Using simplify executable at /Users/dermotcochran/Desktop/eclipse_enterprise/plugins/mobius.simplify.plugin_1.5.6/Simplify-1.5.5.macosx ESC/Java version ESCJava-2.0b4 /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java:26: Fatal error: Expected a Name, got 'for' for(short i=0;i<this.entries.length; i++) { ^ MARKER /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java 26 Fatal error: Expected a Name, got 'for'

!ENTRY mobius.escjava2.plugin 1 0 2008-02-14 14:16:47.957 !MESSAGE MARKER /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java 26 Fatal error: Expected a Name, got 'for' 1 error Escjava checker ended, status code 2 Doing project problem_test 1 items Completed Enable Esc/Java action Thu Feb 14 14:17:21 GMT 2008 Running Escjava checker Specs project already exists - jmlspecs Specs library already installed /jmlspecs Using simplify executable at /Users/dermotcochran/Desktop/eclipse_enterprise/plugins/mobius.simplify.plugin_1.5.6/Simplify-1.5.5.macosx ESC/Java version ESCJava-2.0b4 [0.015 s 150839080 bytes]

sos.enikapplet.EFEntry ... Prover started:0.252 s 127344824 bytes [3.322 s 127596544 bytes]

sos.enikapplet.EFEntry: EFEntry(short, byte, byte[], byte) ... Exception java.lang.ClassCastException: javafe.ast.ArrayType thrown while processing sos.enikapplet.EFEntry java.lang.ClassCastException: javafe.ast.ArrayType at escjava.translate.Frame$ModifiesIterator.add(Frame.java:1113) at escjava.translate.Frame$ModifiesIterator.next(Frame.java:1035) at escjava.translate.GetSpec.trMethodDecl(GetSpec.java:490) at escjava.translate.GetSpec.getCommonSpec(GetSpec.java:87) at escjava.translate.GetSpec.getSpecForCall(GetSpec.java:36) at escjava.translate.Translate.call(Translate.java:3933) at escjava.translate.Translate.trConstructorCallStmt(Translate.java:2171) at escjava.translate.Translate.trConstructorBody(Translate.java:390) at escjava.translate.Translate.trBody(Translate.java:242) at escjava.Main.computeBody(Main.java:1330) at escjava.Main.processRoutineDecl(Main.java:801) at escjava.Main.processTypeDeclElem(Main.java:697) at escjava.Main.processTD(Main.java:641) 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:256) at org.eclipse.ui.internal.WWinPluginAction.runWithEvent(WWinPluginAction.java:229) at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:546) at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:490) at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:402) at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:66) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1495) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1519) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1504) at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1295) at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3350) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:2954) at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2389) at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2353) at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2219) at org.eclipse.ui.internal.Workbench$4.run(Workbench.java:466) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:289) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:461) at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149) at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:106) at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:169) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:106) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:76) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:363) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:176) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25) at java.lang.reflect.Method.invoke(Method.java:585) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:508) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:447) at org.eclipse.equinox.launcher.Main.run(Main.java:1173) 3.354 s 127789144 bytes total Escjava checker ended, status code 0 ESC/Java2 Nature is already present - problem_test Completed Enable Esc/Java operation Thu Feb 14 14:18:12 GMT 2008 Doing project problem_test 1 items Completed Enable Esc/Java action Thu Feb 14 14:18:16 GMT 2008 Running Escjava checker Specs project already exists - jmlspecs Specs library already installed /jmlspecs Using simplify executable at /Users/dermotcochran/Desktop/eclipse_enterprise/plugins/mobius.simplify.plugin_1.5.6/Simplify-1.5.5.macosx ESC/Java version ESCJava-2.0b4 /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java:26: Fatal error: Expected a Name, got 'for' for(short i=0;i<this.entries.length; i++) { ^ MARKER /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java 26 Fatal error: Expected a Name, got 'for'

!ENTRY mobius.escjava2.plugin 1 0 2008-02-14 14:18:20.095 !MESSAGE MARKER /Users/dermotcochran/Documents/workspace_mobius/problem_test/src/sos/enikapplet/DFEntry.java 26 Fatal error: Expected a Name, got 'for' 1 error Escjava checker ended, status code 2

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Mon Jun 30 11:36:23 2008

Milestone ESCJava2.0b5 release deleted

atiti commented 11 years ago

From: kiniry (GH: kiniry) Date: Mon Apr 26 13:28:33 2010

Frame axioms are not supported on blocks, only on methods.

Ticket triage for new Javafe, ESC/Java2, and PVE release.

Not important enough to fix, as we are no longer actively working on ESC/Java2.