loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
13 stars 5 forks source link

NullPointerException when Verifying All Layers on a component with no AGREE annex #123

Open iamundson opened 2 years ago

iamundson commented 2 years ago

If Verify All Layers is run on a component with no AGREE annex, but with subcomponents containing AGREE annexes, a null pointer exception is thrown with no useful information. This does not happen when Verify Single Layer is run. This is either due to a bug or the exception is not being handled gracefully. See stack trace below:

!ENTRY com.rockwellcollins.atc.agree.analysis 4 0 2022-08-18 16:37:34.080 !MESSAGE !STACK 0 java.lang.NullPointerException at jkind.api.results.CompositeAnalysisResult.addChild(CompositeAnalysisResult.java:19) at com.rockwellcollins.atc.agree.analysis.handlers.VerifyHandler.runJob(VerifyHandler.java:223) at com.rockwellcollins.atc.agree.analysis.handlers.AadlHandler.lambda$1(AadlHandler.java:127) at com.rockwellcollins.atc.agree.analysis.handlers.AadlHandler.lambda$0(AadlHandler.java:113) at org.eclipse.xtext.resource.OutdatedStateManager.exec(OutdatedStateManager.java:70) at org.eclipse.xtext.ui.editor.model.XtextDocument$XtextDocumentLocker.internalReadOnly(XtextDocument.java:525) at org.eclipse.xtext.ui.editor.model.XtextDocument$XtextDocumentLocker.readOnly(XtextDocument.java:497) at org.eclipse.xtext.ui.editor.model.XtextDocument.readOnly(XtextDocument.java:136) at com.rockwellcollins.atc.agree.analysis.handlers.AadlHandler$1.runInWorkspace(AadlHandler.java:105) at org.eclipse.core.internal.resources.InternalWorkspaceJob.run(InternalWorkspaceJob.java:42) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)