Move inserting rely()s, Gammas, assertions, etc. to IR

[l-kent]

At some stage we will want to move the insertion of rely() calls, Gamma values, assertions, and any other transformations to the program representation that happen during IRToBoogie to a separate step entirely within the IR, rather than having all that happen as part of the IRToBoogie translation process. This will allow various analyses and transformations, such as the modifies clause propagation, to relate to these, which will be useful.

[l-kent]

A further task following on from this is to make the the Boogie-level specifications (currently only supplied via raw strings) be fully parsed and accessible at the IR level, so they can potentially be used in the analyses.