Spurious overflow failures with Result/Error types #558
Description
I tried this code:
enum MyError {
Val1,
Val2,
}
fn foo(x: u32) -> Result<(), MyError> {
if x > 10 {
Err(MyError::Val2)
} else {
Ok(())
}
}
fn bar() -> Result<(), MyError> {
let x = foo(15)?;
Ok(x)
}
pub fn main() {
bar();
}using the following command line invocation:
rmc test.rs
with RMC version: 7635cfebfa5
I expected to see this happen: no failures
Instead, this happened: got 2 arithmetic overflow failures:
** Results:
/home/ubuntu/tools/rmc/library/core/src/result.rs function <std::result::Result<T, E> as std::ops::Try>::branch
[<std::result::Result<T, E> as std::ops::Try>::branch.assertion.1] line 1903 unreachable code: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.overflow.1] line 1903 arithmetic overflow on unsigned - in ((unsigned char *)&self)[0] - 2: FAILURE
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_arithmetic.1] line 1903 pointer arithmetic: dead object in (unsigned char *)&self + 0: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_dereference.1] line 1903 dereference failure: dead object in ((unsigned char *)&self)[0]: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_arithmetic.2] line 1904 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[<std::result::Result<T, E> as std::ops::Try>::branch.pointer_dereference.2] line 1904 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS
/home/ubuntu/tools/rmc/src/test/rmc/Enum/result4.rs function bar
[bar.assertion.1] line 18 unreachable code: SUCCESS
[bar.overflow.1] line 18 arithmetic overflow on unsigned - in ((unsigned char *)&var_2)[0] - 2: FAILURE
[bar.pointer_arithmetic.1] line 18 pointer arithmetic: dead object in (unsigned char *)&var_2 + 0: SUCCESS
[bar.pointer_dereference.1] line 18 dereference failure: dead object in ((unsigned char *)&var_2)[0]: SUCCESS
[bar.pointer_arithmetic.2] line 20 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[bar.pointer_dereference.2] line 20 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS
/home/ubuntu/tools/rmc/src/test/rmc/Enum/result4.rs function foo
[foo.pointer_arithmetic.1] line 13 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[foo.pointer_dereference.1] line 13 dereference failure: dead object in ((unsigned char *)&var_0)[0]: SUCCESS
** 2 of 14 failed (2 iterations)
VERIFICATION FAILED
The - 2 in the check:
[bar.overflow.1] line 18 arithmetic overflow on unsigned - in ((unsigned char *)&var_2)[0] - 2: FAILURE
seems to be coming from the number of values in the enum. The arithmetic overflow checks are not expected in the first place.