stack allocation: invalid slot

[eponier]

In the following example

export fn main () -> reg u64 {
  reg u64 res;
  stack u64[3] a, b;
  a[0:2] = b[1:2];
  res = a[0];
  return res;
}

the OCaml oracle associates a partly negative range to variable b. Then the Coq checker fails due to the negative starting index.

I am not sure what to do here. Should the OCaml oracle be patched to fail early? Or do we consider that this is normal, but just need a bettor error message from the Coq checker?

[eponier]

@vbgl