Boogie L function does not check variable memory range

[b-paul]

At the moment, emitted security policies (L function) in boogie code are of this form.

function {:extern} L(mem$in: [bv64]bv8, index: bv64) returns (bool) {
  (if (index == $y_addr) then false else (if (index == $x_addr) then true else false))
}

We only check base addresses of global variables. This is a problem if we write to an offset of a low variable's address. For example, in this program we write the value of y (truncated to 16 bits) to the address one byte after the address of x.

int x;
int y;

int main(int argc, char **argv) {
    *((short*)(((char*)(&x))+1)) = (short)y;

    return 0;
}

If we use the following spec file

Globals:
x: int
y: int

L: x -> true, y -> false

Subroutine: main
Requires: Gamma_y == false

we are writing a secret into x (since y has a low gamma), but x should not store any secrets, and this should therefore not verify.
Unfortunately it does :(

To fix this I think we should be able to just change the form of L so that it checks address ranges instead of just base addresses.