Propagate modifies clause through boogie program

[ailrst]

• Fixes Spurious mem in modifies clause #111 by pushing all the values in the modifies clause up the call tree of the boogie program, right at the end of generation instead of always inserting an extra mem for the rely().
• Also renames "boogie.ProcedureCall" to "boogie.BProcedureCall".

This implementation is fairly inefficient, @l-kent you referred to a broader refactor to do something like this but I'm not sure what you had in mind for that.

[l-kent]

The broader refactor I was thinking of would be moving all the insertion of relies, Gammas, etc. to be a stage of the IR transformation rather than happening as part of the Boogie translation process at the end. This would allow various analyses to directly relate to those if necessary, so we wouldn't need to do two different fixed point propagation of modifies clauses like is happening here.

This will work for now though, sure.

[l-kent]

I've just made it use a Set which should make it marginally more efficient, and made the final modifies output be fully sorted again to ensure the future output is more consistent.

[ailrst]

The broader refactor I was thinking of would be moving all the insertion of relies, Gammas, etc. to be a stage of the IR transformation rather than happening as part of the Boogie translation process at the end. This would allow various analyses to directly relate to those if necessary, so we wouldn't need to do two different fixed point propagation of modifies clauses like is happening here.

This will work for now though, sure.

Yeah that makers sense that would be a good approach