Type errors for undeclared storage references

[d-xo]

The following spec is currently accepted by the typechecker:

constructor of Env
interface constructor()

creates

    uint value := 1

behaviour f of Env
interface f()

returns 1

ensures

    value == 1

This spec is incorrect because value is not mentioned in a storage block in f, and attempts to prove the postcondition will fail as no storage variables is declared for value. The typechecker should ensure that each variable referenced in a behaviour is also mentioned in the storage block for that behaviour.

[zoep]

Closing issue as we no longer require storage variables to be referenced explicitly in the storage block of each function.