ParserException during CBMC check
To reproduce the error:
!ENTRY org.fortiss.af3.tools 1 0 2014-11-19 14:55:43.335
!MESSAGE Performing CPover analysis “clearframe == NoVal, ” on component
PixelTest.
!ENTRY org.fortiss.af3.tools 1 0 2014-11-19 14:55:43.350
!MESSAGE Running cbmc [cbmc, —xml-ui, —32, -I,
/Users/moudy/Downloads/af3/runtime-New_configuration/.metadata/.plugins/org.fortiss.af3.tools/cProver_analyzation_files_2626116829605923503,
—error-label, L_NOTNOTnovalclearframeID1234EQEQtrue,
src-gen/PixelTest_ID_676.c, src-gen/data_dictionary.c,
src-gen/cProver_analysis_entry.c] in directory
/Users/moudy/Downloads/af3/runtime-New_configuration/.metadata/.plugins/org.fortiss.af3.tools/cProver_analyzation_files_2626116829605923503.
!ENTRY org.fortiss.af3.tools 1 0 2014-11-19 14:55:56.008
!MESSAGE Run in 12.672s.
java.lang.reflect.InvocationTargetException
at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:421)
at
org.eclipse.jface.dialogs.ProgressMonitorDialog.run(ProgressMonitorDialog.java:507)
at
org.fortiss.af3.analyses.ui.base.AnalysesProgressBar.doOpen(AnalysesProgressBar.java:100)
at
org.fortiss.af3.analyses.ui.cprover.CProverUIFacade.performModelCheckingAnalysis(CProverUIFacade.java:75)
at
org.fortiss.af3.systavio.ui.SystavioContextMenuContributor$2.createSystavioTestCases(SystavioContextMenuContributor.java:239)
at
org.fortiss.af3.systavio.ui.SystavioContextMenuContributor$2.run(SystavioContextMenuContributor.java:195)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:499)
at
org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at
org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
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.Display.sendEvent(Display.java:4166)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1466)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1489)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1474)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1279)
at
org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4012)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3651)
at
org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1113)
at
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at
org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:997)
at
org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:140)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:611)
at
org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:567)
at
org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
at
org.fortiss.af3.rcapplication.AF3Application.start(AF3Application.java:48)
at
org.eclipse.equinox.internal.apEclipseAppHandle.run(EclipseAppHandle.java:196)
at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(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:354)
at
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:181)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:483)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:636)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:591)
at org.eclipse.equinox.launcher.Main.run(Main.java:1450)
at org.eclipse.equinox.launcher.Main.main(Main.java:1426)
Caused by: org.fortiss.af3.expression.language.ParseException: line 1:13
mismatched input ‘}’ expecting ‘]’
at
org.fortiss.af3.expression.language.Compiler.compileTerm(Compiler.java:56)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.parseValue4Array(CProverLiftedResultBuilder.scala:257)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.parseValue4Type(CProverLiftedResultBuilder.scala:214)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.parseValue4IIdLabeled(CProverLiftedResultBuilder.scala:185)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.buildLiftedCounterExampleState(CProverLiftedResultBuilder.scala:134)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$anonfun
buildLiftedCounterexample$1.apply(CProverLiftedResultBuilder.scala:93)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$anonfun
buildLiftedCounterexample$1.apply(CProverLiftedResultBuilder.scala:93)
at scala.collection.Iterator$class.foreach(Iterator.scala:743)
at scala.collection.AbstractIterator.foreach(Iterator.scala:1174)
at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
at scala.collection.AbstractIterable.foreach(Iterable.scala:54)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.buildLiftedCounterexample(CProverLiftedResultBuilder.scala:92)
at
org.fortiss.af3.analyses.cprover.CProverLiftedResultBuilder$.buildLiftedResult(CProverLiftedResultBuilder.scala:80)
at
org.fortiss.af3.analyses.cprover.CProverBasedAnalyzerBase$CProverLiftedLazyResult.get(CProverBasedAnalyzerBase.scala:270)
at
org.fortiss.af3.analyses.cprover.CProverBasedAnalyzerBase$CProverLiftedLazyResult.get(CProverBasedAnalyzerBase.scala:247)
at
org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:181)
at
org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:104)
at
org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
(from redmine: issue id 2157, created on 2014-11-19, closed on 2015-08-14)
- Uploads: