Skip to content
This repository has been archived by the owner. It is now read-only.

NPE when using the instance() function on a simple model #167

Closed
paolo-crisafulli opened this issue Aug 6, 2018 · 2 comments
Closed

NPE when using the instance() function on a simple model #167

paolo-crisafulli opened this issue Aug 6, 2018 · 2 comments
Assignees
Labels

Comments

@paolo-crisafulli
Copy link

@paolo-crisafulli paolo-crisafulli commented Aug 6, 2018

Hi,

Below is a simple model which crashes Resolute:

package hardware
public
	annex Resolute {** 
	claim(c: component) <=
	  ** "Always true" **
	  let c1: component = instance(Board.i);
	  true
	**};

	system Board
	end Board;
	
	system Cpu
	end Cpu;

	system implementation Board.i
		subcomponents
			cpu_1: system; -- assign Cpu type to cpu_1 and Resolute will crash no more
		annex Resolute {**
		  prove(claim(this))
	    **};
	end Board.i;
end hardware;

Do you think this can be fixed?
Thank you very much for your help.

Below is the stack trace of the thrown exception:

java.lang.NullPointerException
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteBuiltInFnCallEvaluator.isInstanceOf(ResoluteBuiltInFnCallEvaluator.java:801)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteBuiltInFnCallEvaluator.evaluate(ResoluteBuiltInFnCallEvaluator.java:681)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteEvaluator.caseBuiltInFnCallExpr(ResoluteEvaluator.java:589)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteEvaluator.caseBuiltInFnCallExpr(ResoluteEvaluator.java:1)
	at com.rockwellcollins.atc.resolute.resolute.util.ResoluteSwitch.doSwitch(ResoluteSwitch.java:398)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.eval(ResoluteProver.java:72)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseLetExpr(ResoluteProver.java:154)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseLetExpr(ResoluteProver.java:1)
	at com.rockwellcollins.atc.resolute.resolute.util.ResoluteSwitch.doSwitch(ResoluteSwitch.java:452)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseBinaryExpr(ResoluteProver.java:100)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseBinaryExpr(ResoluteProver.java:1)
	at com.rockwellcollins.atc.resolute.resolute.util.ResoluteSwitch.doSwitch(ResoluteSwitch.java:281)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.claimCall(ResoluteProver.java:271)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseFnCallExpr(ResoluteProver.java:247)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteProver.caseFnCallExpr(ResoluteProver.java:1)
	at com.rockwellcollins.atc.resolute.resolute.util.ResoluteSwitch.doSwitch(ResoluteSwitch.java:407)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteInterpreter.evaluateProveStatementBody(ResoluteInterpreter.java:29)
	at com.rockwellcollins.atc.resolute.analysis.execution.ResoluteInterpreter.evaluateProveStatement(ResoluteInterpreter.java:22)
	at com.rockwellcollins.atc.resolute.analysis.handlers.ResoluteHandler.runJob(ResoluteHandler.java:218)
	at com.rockwellcollins.atc.resolute.analysis.handlers.AadlHandler$1$1.exec(AadlHandler.java:73)
	at com.rockwellcollins.atc.resolute.analysis.handlers.AadlHandler$1$1.exec(AadlHandler.java:1)
	at org.eclipse.xtext.resource.OutdatedStateManager.exec(OutdatedStateManager.java:91)
	at org.eclipse.xtext.ui.editor.model.XtextDocument$XtextDocumentLocker.internalReadOnly(XtextDocument.java:520)
	at org.eclipse.xtext.ui.editor.model.XtextDocument$XtextDocumentLocker.readOnly(XtextDocument.java:492)
	at org.eclipse.xtext.ui.editor.model.XtextDocument.readOnly(XtextDocument.java:133)
	at com.rockwellcollins.atc.resolute.analysis.handlers.AadlHandler$1.runInWorkspace(AadlHandler.java:68)
	at org.eclipse.core.internal.resources.InternalWorkspaceJob.run(InternalWorkspaceJob.java:39)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:56)
@kfhoech
Copy link
Contributor

@kfhoech kfhoech commented Aug 8, 2018

Fixed by addition of a null check.

The nightly testing build should contain the fix tomorrow.

Thanks for reporting this bug!

@paolo-crisafulli
Copy link
Author

@paolo-crisafulli paolo-crisafulli commented Sep 19, 2018

Thank you very much, works fine with Osate 2.3.5.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants