Support type casting for numeric values

[kammola]

Applying arithmetic operations and comparison between different numeric types should be allowed, e.g. ("#[ensures (result > 100 * i)]" if result is i32 and I is i32).

[kammola]

@vakaras

[fpoli]

Lossless integer casts (e.g. i32 -> u128 etc) should already be supported.

[kammola]

Lossless integer casts (e.g. i32 -> u128 etc) should already be supported.

what about usize -> i32, that should be possible if we can ensure an upper bound on the value.

[fpoli]

what about usize -> i32, that should be possible if we can ensure an upper bound on the value.

That's not supported, but it should be easy to encode the cast as a pure Viper Int -> Int function call, with a precondition that checks that the input value is in the range of the output type.

[fpoli]

It's also easy to support numeric casts when overflow checks are disabled. It's matter of adding one branch to the encode_cast_expr in mir_encoder.rs.