Compiler pass "add array init" creates a lval with a dummy location

[eponier]

The instruction itself has a location, but not the lval. I do not know what to do here, maybe there is no good solution.

[eponier]

(The corresponding line is

jasmin/proofs/compiler/array_init.v

Line 94 in 3f92895

let x := VarI x dummy_var_info in

)

[J08nY]

This may be possible to solve the same way as in: c727337. There the dummy flag variables __of__, __zf__, ... did not have any variable info. Here, the dummy var info could be replaced with (var_info_of_ii ii) after #736 lands.