Adding location to SP generated variables
I don't know if I already opened an issue for this but there should be locations for ident generated by the sp_expr function in vc.ml. In this part of the code, I would like the None locations to be replaced by the appropriate locations:
let fresh_wr2 v _ = clone_pv None v in let fresh_rd2 v _ = if v.pv_ity.ity_pure then None else Some (clone_pv None v) in
This is apparently possible to do by adding a location to constructor Kseq and then propagating it.
A test for checking that it works is simply to create several assignments in a function and look at the generated task. If the constants of the generated task don't have locations, it does not work.