Improve initialization of runtime slices

[sarranz]

The following program

param int N = 3;

export
fn foo(reg ptr u32[N] pz) -> reg u32 {
    reg u32 i = 0;
    while (i < N-1) {
        reg ptr u32[1] pzi = pz[i:1];
        _ = pzi[0];
        i += 1;
    }
    return i;
}

gives

Default checker parameters.

Analyzing function foo



*** Possible Safety Violation(s):
  "ble.jazz", line 39 (8-19): is_init pzi[0]
  
Memory ranges:
  mem_pz: [0; 0]
  
* Rel:
{mem_pz = 0}
mem_pz ∊ [0; 0]



Program is not safe!

even though the version without the slice checks successfully. Slices with constant indices work properly. I assume that we are being conservative and forgetting the information we know about pz when we take a runtime slice?