This is more convenient to use from rustc and avoids the high risk of overflow whenever we traverse a function body. It's likely a lot faster too. charon-ml users won't see the difference.
One surprising consequence is that this changes some loop spans in Aeneas tests. For a reason I don't understand, Aeneas usually had loop spans that pointed to the whole function instead of just the loop. Now it uses the span that is supposed to cover just the loop. Unfortunately spans are hard so they tend to be wrong anyway.
This is more convenient to use from rustc and avoids the high risk of overflow whenever we traverse a function body. It's likely a lot faster too.
charon-mlusers won't see the difference.One surprising consequence is that this changes some loop spans in Aeneas tests. For a reason I don't understand, Aeneas usually had loop spans that pointed to the whole function instead of just the loop. Now it uses the span that is supposed to cover just the loop. Unfortunately spans are hard so they tend to be wrong anyway.
Fixes #122