#java #eclipse #key-formal-verification
Вопрос:
Я работаю над проектом с формальной проверкой с помощью ключа на Java. Для этого я использую плагин Eclipse. Все работало нормально, когда у меня была Xtext версии 2.10. Однако по некоторым причинам я решил обновить Xtext до 2.25. К сожалению, сейчас я получаю следующую ошибку:
!ENTRY org.eclipse.e4.ui.workbench 4 0 2021-05-20 11:22:24.373
!MESSAGE Failed to evaluate: AndExpression [children=[WithExpression [variable=selection, children=[AndExpression [children=[<test property="isGoal" plug-in activation: eager/>]]]]]]
!STACK 0
org.eclipse.core.runtime.CoreException: No property tester contributes a property org.key_project.keyide.ui.isGoal to type class org.eclipse.jface.text.TextSelection
at org.eclipse.core.internal.expressions.TypeExtensionManager.getProperty(TypeExtensionManager.java:131)
at org.eclipse.core.expressions.TestExpression.evaluate(TestExpression.java:104)
at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
at org.eclipse.core.expressions.AndExpression.evaluate(AndExpression.java:36)
at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
at org.eclipse.core.expressions.WithExpression.evaluate(WithExpression.java:84)
at org.eclipse.core.expressions.CompositeExpression.evaluateAnd(CompositeExpression.java:54)
at org.eclipse.core.expressions.AndExpression.evaluate(AndExpression.java:36)
at org.eclipse.ui.internal.services.EvaluationReference.evaluate(EvaluationReference.java:79)
at org.eclipse.ui.internal.services.EvaluationReference.evaluate(EvaluationReference.java:109)
at org.eclipse.ui.internal.services.EvaluationReference.changed(EvaluationReference.java:103)
at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
at org.eclipse.ui.internal.services.EvaluationService$1.changed(EvaluationService.java:79)
at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
at org.eclipse.ui.internal.e4.compatibility.SelectionService.handleSelectionChanged(SelectionService.java:85)
at org.eclipse.ui.internal.e4.compatibility.SelectionService.lambda$0(SelectionService.java:72)
at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$1.run(SelectionAggregator.java:123)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
at org.eclipse.e4.ui.internal.workbench.SelectionAggregator.notifyListeners(SelectionAggregator.java:120)
at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$5.lambda$0(SelectionAggregator.java:220)
at org.eclipse.e4.core.contexts.RunAndTrack.runExternalCode(RunAndTrack.java:59)
at org.eclipse.e4.ui.internal.workbench.SelectionAggregator$5.changed(SelectionAggregator.java:220)
at org.eclipse.e4.core.internal.contexts.TrackableComputationExt.update(TrackableComputationExt.java:108)
at org.eclipse.e4.core.internal.contexts.EclipseContext.processScheduled(EclipseContext.java:364)
at org.eclipse.e4.core.internal.contexts.EclipseContext.set(EclipseContext.java:379)
at org.eclipse.e4.ui.internal.workbench.SelectionServiceImpl.setSelection(SelectionServiceImpl.java:34)
at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.selectionChanged(CompatibilityPart.java:471)
at org.eclipse.jface.viewers.Viewer$1.run(Viewer.java:151)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:174)
at org.eclipse.jface.viewers.Viewer.fireSelectionChanged(Viewer.java:148)
at org.eclipse.jface.text.TextViewer.fireSelectionChanged(TextViewer.java:2621)
at org.eclipse.jface.text.TextViewer.selectionChanged(TextViewer.java:2600)
at org.eclipse.jface.text.TextViewer.setSelectedRange(TextViewer.java:2287)
at org.eclipse.jface.text.DefaultTextDoubleClickStrategy.doubleClicked(DefaultTextDoubleClickStrategy.java:192)
at org.eclipse.jface.text.TextViewer$TextDoubleClickStrategyConnector.getPreviousOffset(TextViewer.java:238)
at org.eclipse.swt.custom.StyledTextListener.handleEvent(StyledTextListener.java:95)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:89)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4443)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1512)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1535)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1520)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1324)
at org.eclipse.swt.custom.StyledText.sendWordBoundaryEvent(StyledText.java:8401)
at org.eclipse.swt.custom.StyledText.getWordPrevious(StyledText.java:5508)
at org.eclipse.swt.custom.StyledText.getWordPrevious(StyledText.java:5482)
at org.eclipse.swt.custom.StyledText.handleMouseDown(StyledText.java:6193)
at org.eclipse.swt.custom.StyledText.lambda$1(StyledText.java:5796)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:89)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4443)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1512)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1535)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1520)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1324)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4229)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3839)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$5.run(PartRenderingEngine.java:1157)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1046)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:155)
at org.eclipse.ui.internal.Workbench.lambda$3(Workbench.java:644)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:338)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:551)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:156)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:152)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:203)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:401)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:255)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:64)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:564)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:653)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:590)
at org.eclipse.equinox.launcher.Main.run(Main.java:1461)
at org.eclipse.equinox.launcher.Main.main(Main.java:1434)
Когда я искал решения, я обнаружил, что другие натыкаются на аналогичную проблему, но с другой библиотекой. Решение состояло в том, чтобы просто обновить библиотеку.
Сайт обновления eclipse с ключа сломан, поэтому я не могу обновить свой проект. Моя текущая версия ключа-Eclipse 1.0.0
Комментарии:
1. возможно, вам следует проверить, где определена цель org.key_project.keyide.ui.и в этом плагине (возможно, org.key_project.keyide.ui) можно активировать, а если нет, то почему бы и нет. вы также должны проверить, где используется org.key_project.keyide.ui.isGoal, и можете ли вы удалить его оттуда
2. Я даже не использую метод цели. Мой проект не запустится, потому что зависимость (org.key_project.keyide.ui) содержит синтаксическую ошибку. Это странно, потому что я скачал последний ключ с GitHub, и там нет org.key_project.keyide.ui.isGoal. Удалось найти только de.uka.ilkd.ключ.ядро.цель и de.uka.ilkd.ключ.доказательство.цель.
3. поиск внутри org.key_project.keyide.ui/plugin.xml (или как бы ни назывался плагин) для цели
4. Плагин активирован из того, что я понял. Вот файл непосредственно из репозитория key_project.
5. что-нибудь еще в журнале ошибок