Check assume/guarantee Bug
- Check assume/guarantee under Assume/Guarantee Reasoning does not work under Component Architecture.
- Check selected Component under Assume/Guarantee Reasoning does not work for a component with a Code Specification.
Error log:
!ENTRY org.fortiss.af3.tools 1 0 2013-08-03 17:44:36.826
!MESSAGE Running z3 [z3, -smt2, assumption0b7-5564450619422312475.smt2] on file assumption0b7-5564450619422312475.smt2 in directory /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools.
!ENTRY org.fortiss.af3.tools 1 0 2013-08-03 17:44:36.868
!MESSAGE Run in 0,041s.
!ENTRY org.fortiss.af3.tools 4 0 2013-08-03 17:44:36.869
!MESSAGE Error on running z3 on file: /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/assumption0b7-5564450619422312475.smt2 The file was not deleted and can be debugged!
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 -
at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
at java.util.concurrent.FutureTask.get(FutureTask.java:91)
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 -
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
at java.util.concurrent.FutureTask.run(FutureTask.java:138)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
at java.lang.Thread.run(Thread.java:680)
!ENTRY org.fortiss.af3.tools 4 0 2013-08-03 17:44:36.872
!MESSAGE Unexpected error!
!STACK 0
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 -
at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
at java.util.concurrent.FutureTask.get(FutureTask.java:91)
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 -
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
at java.util.concurrent.FutureTask.run(FutureTask.java:138)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
at java.lang.Thread.run(Thread.java:680)
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:99)
at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.performAnalyzesAndDisplayResults(AssumeGuaranteeView.java:301)
at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.access$0(AssumeGuaranteeView.java:280)
at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView$2.widgetSelected(AssumeGuaranteeView.java:191)
at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:240)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4128)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1457)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
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:344)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
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:597)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
at org.eclipse.equinox.launcher.Main.main(Main.java:1386)
Caused by: java.lang.RuntimeException: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 -
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:319)
at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 -
at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
at java.util.concurrent.FutureTask.get(FutureTask.java:91)
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
... 6 more
Caused by: java.lang.Exception: z3 exited with code 1 -
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
at java.util.concurrent.FutureTask.run(FutureTask.java:138)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
at java.lang.Thread.run(Thread.java:680)
For test see attached AF3 Project.
(from redmine: issue id 1570, created on 2013-08-03, closed on 2013-08-05)
- Uploads: