Missing Invariant Checks for Casts

[DavePearce]

Test 000908 reports the wrong error:

type i8 is (int x) where (x >= -128) && (x <= 127)

function f(int x) -> i8[]
requires (x == 0) || (x == 256):
    return [(i8) x]

The error is:

src/main.whiley:5: postcondition may not be satisfied
    return [(i8) x]
    ^^^^^^^^^^^^^^^

But it should be complaining about the cast.

[DavePearce]

The essential problem is that its not checking for casts. This should be doable with a little help.

[DavePearce]

The basic problem here is that DefinednessChecker operates of the Boogie AST and evidence of casts has been eliminated.

[DavePearce]

This example illustrates the problem:

type i8 is (int x) where (x >= -128) && (x <= 127)

function f(int x) -> i8[]
requires (x == 0) || (x == 256):
    return [(i8) x]

The generated Boogie is:

   var t187 : int;
   var x : int;
   x := x#;
   assert nat#is(Int#box(g(HEAP,x)),HEAP);
   $ := g(HEAP,x);
   return;

where we have:

type nat = int;
function nat#inv(n : int, HEAP : [Ref]Any) returns (bool) {
   0 <= n
}
function nat#is(n : Any, HEAP : [Ref]Any) returns (bool) {
   Int#is(n) && nat#inv(Int#unbox(n),HEAP)
}

But this obviously won't pass because this is not strong enough:

function g(HEAP : [Ref]Any, x : int) returns (int);
procedure g(x : int) returns (r : int);
requires Context#Level > 1;
ensures r > 0;
free ensures g(HEAP,x) == r;

Realistically to make this work, I need to fix the boogie backend translation (see #153).