You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The Java bridge can't always resolve imported VDM-SL types.
Steps to Reproduce
Create a file A.vdmsl with the following content:
module G
exports all
definitions
types
T = int;
end G
module A
imports from G all
exports all
definitions
operations
op : () ==> G`T
op () == is not yet specified;
end A
module B
imports from A all
exports all
definitions
operations
op2 : () ==> int
op2 () == A`op();
end B
Create a Java implementation of the operation in A:
Export this Java class as a JAR file, named lib.jar.
Execute B`op() in the following way:
java -cp Overture-2.6.0.jar:lib.jar org.overture.interpreter.VDMJ -vdmsl -default B -e 'B`op2()' A.vdmsl
Expected behavior:
Expected the model to terminate gracefully:
λ java -cp Overture-2.6.1-SNAPSHOT.jar:lib.jar org.overture.interpreter.VDMJ -vdmsl -default B -e 'B`op2()' A.vdmsl
Parsed 3 modules in 0.041 secs. No syntax errors
Type checked 3 modules in 0.055 secs. No type errors
Initialized 3 modules in 0.048 secs.
5
Bye
Actual behavior:
The model crashes, complaining that the type G`T cannot be found:
λ java -cp Overture-2.6.1-SNAPSHOT.jar:lib.jar org.overture.interpreter.VDMJ -vdmsl -default B -e 'B`op2()' A.vdmsl
Parsed 3 modules in 0.047 secs. No syntax errors
Type checked 3 modules in 0.055 secs. No type errors
Initialized 3 modules in 0.047 secs.
Failed in native method: Definition G`T not found
org.overture.interpreter.runtime.ValueException: Definition G`T not found
Execution: Internal 0059: Failed in native method: Definition G`T not found
org.overture.interpreter.runtime.ValueException: Definition G`T not found
Bye
Description
The Java bridge can't always resolve imported VDM-SL types.
Steps to Reproduce
Export this Java class as a JAR file, named
lib.jar
.Execute B`op() in the following way:
java -cp Overture-2.6.0.jar:lib.jar org.overture.interpreter.VDMJ -vdmsl -default B -e 'B`op2()' A.vdmsl
Expected behavior:
Expected the model to terminate gracefully:
Actual behavior:
The model crashes, complaining that the type G`T cannot be found:
Reproduces how often:
Every time.
Versions
Overture 2.6.0
OpenJDK Runtime Environment (build 1.8.0_151-8u151-b12-0ubuntu0.17.10.2-b12)
Linux, Ubuntu 17.10
Additional Information
I have a fix for this, I'll submit it as a pull request later for discussion.
The text was updated successfully, but these errors were encountered: