Type-checker allows modules to directly access state of other modules

[peterwvj]

Description

Type-checker allows modules to directly access state of other modules.

Steps to Reproduce

Create a file A.vdmsl with the following content:

 module A

 exports all
 definitions

 state St of

 x : nat
 init s == s = mk_St(5)
 end

 end A

 module Entry

 imports from A all
 definitions

 operations

 Run : () ==> ?
 Run () == return A`x; -- ********* line 22 *********

 end Entry

Run java -jar Overture.jar -vdmsl A.vdmsl

Expected behavior: [What you expect to happen]

Expected error to be reported since you're not allowed to access state from another module like this.

Actual behavior: [What actually happens]

No error is reported.

Reproduces how often: [What percentage of the time does it reproduce?]

Every time.

Versions

Overture 2.5.6.

Additional Information

The issue is the same in VDMJ.

[nickbattle]

This is correctly handled by VDMTools, saying that the A'x name is not found, since the imports all should not include it.

[nickbattle]

This is because the "exports all" part of the type checker naively exports every definition from the module. It ought to strip out any state definitions before doing this. A VDMJ fix was easy, so Overture ought to be also.

[nickbattle]

The correction now also includes a second error because the "import all" is for a module with no (effective) exports, now that the state definition is excluded:

Error 3190: Import all from module with no exports? in 'B' (test.vdm) at line 11:16
Error 3182: Name 'A`x' is not in scope in 'B' (test.vdm) at line 15:20

[peterwvj]

Grreat, thanks! I'll include this fix in the release candidate.