Assume integer bounds with CREUSOT_UNBOUNDED

[jhjourdan]

Something to discuss: after #309, we have seen a weird behaviour of CREUSOT_UNBOUNDED=1: activating this option can break proofs, which is highly unexpected. In particular, it is unexpected that unsigned integers can then contain negative values.

I would suggest either:

• assume that arithmetic operations are always in bounds when performing said arithmetic operations,
• do the same, but only for the sign of unsigned operations.

[xldenis]

The current behavior was a rapid addition which mimics how Prusti disables bounds checks by changing the type that integers are translated to. I'd like to remove it entirely and replace it with a more fine-grained toggle, perhaps something which would allow disabling checks for individual operations or blocks of operations instead.

[xldenis]

Perhaps this could just be done by providing an alternate prelude in which we use a version of the machine integer types & functions with no preconditions?

[jhjourdan]

This seems indeed a good way to go.