Do IOrigin wrapping around RangeToken, instead of inside its StartToken

[keyboardDrummer]

Description

• A RangeToken no longer takes two IOrigins, which could be wrapped, but instead takes two Token instances. Wrapping now happens around the RangeToken instead of inside its StartToken.
• Add the properties Token StartToken, Token EndToken and Token Center to IOrigin.
• Add the IOrigin Origin property to INode, and remove the getter for the RangeToken property (I'll remove the setter in a follow-up). Any usages of RangeTokens getter are replaced with Origin. INode still has a .Tok as well, but we'll replace that in a follow-up PR with usages of Origin.
• RangeToken now includes an optional field for containing the "Center". Replace most overrides of Node.Tok with assignments to RangeToken.Centre.

Future

• Rename RangeToken to SourceOrigin. Rename RangeNode to OriginNode.
• Replace usages of Node.tok/Tok with Node.Origin
• Replace usages of TokenNode with OriginNode (which requires computing the start and end of expression in the parser already), making OriginWithComputedRange obsolete, and allowing OriginNode to be merged into Node
• Remove token like fields from IOrigin, so users must always choose to use Start/End/Center.
• Get rid of BoogieRangeToken
• Inline MakeAutoGenerated and MakeRefined

How has this been tested?

There are several classes of small changes to reported locations. I have manually inspected all of these changes. Here's some of the categories:

• Message starting with "Warning: This ensures clause is part of a bodyless method.". Previously the reported location was the center of the ensure's predicate, like the == in ensures a == b, and now it is the center of the ensures clause itself, which for now is the start token of the predicate. I would rather it be the keyword of the ensures itself, but that would have introduced more changes and I'd prefer to do that in another PR.
• Message starting with "Warning: XXX with {:only}". Location was previously the start of {:only} but now it's the center, which apparently is the o of only.
• Warning: unnecessary requires clause and "Warning: unnecessary (or partly unnecessary) assume statement" are now reported at the center of the predicate instead of the start

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.