Failed truncation of stack variables

[vbgl]

Compilation of the following program crashes with:

"bug_681.jazz", line 6 (2-8):
compilation error in function load_small:
asmgen: invalid rexpr for oprd (32)[RSP + ((64u) 0)]
invalid Load size

It seems that stack-allocation emits wrong code.

export
fn load_small(reg u32 x) -> reg u16 {
  stack u32 s;
  reg u16 r;
  s = x;
  r = s;
  return r;
}

[eponier]

I'm working on it, but the changes in the proofs are not that small, so I need some time.