Warning for unused state variable

[olafur-skulason]

Description

I get a warning in Overture, VDM-SL with state variables if I refer to the variable using the format 'state'.'variable' instead of usingthe short form 'variable'. The warning claims that the variable is not used, when using the longer more precise format.

Steps to Reproduce

Code example. Change ending to .vdmsl, github limitation.
bug_report.txt

Expected behavior:

I expect the system to recognise a reference to a variable in the format 'state'.'variable' as being used.

Actual behavior:

The system fails to recognize that the variable is used.

Reproduces how often:

Always

Versions

Overture 2.6.2
Ubuntu 18.04

[peterwvj]

Thanks for the nice bug report :)

So this also seems to be a problem if you use explicit operations and preconditions. Here's another example:

state St of
  x : nat
end

operations 

op: () ==> ()
op() == skip
post St.x > St~.x;

op2 : () ==> ()
op2 () == skip
pre St.x = 2;

VDMJ also produces this warning.

[nickbattle]

Interesting. Thanks for reporting.

This is to do with the way that the state is being accessed. You're using "St.x" as opposed to "x", which is therefore directing the read via the "readonly" version of the state record, St. This will presumably be the cause of the problem. I agree it ought to regard such access as access to the direct state value, since it has been "read" (in the sense of being referred to).

If you change one of the uses to just use "x", then all is fine.

I will investigate.

[nickbattle]

OK, just pushed a fix for this. It's pretty ugly: it has to basically check all field accesses to see whether they correspond to SL state access and then mark the corresponding state as "read". But it seems to work. The example above is now warning free.