-
David Bühler authored
According to the C standard, section 6.5.5 §6: "If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a; otherwise, the behavior of both a/b and a%b is undefined."
David Bühler authoredAccording to the C standard, section 6.5.5 §6: "If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a; otherwise, the behavior of both a/b and a%b is undefined."
addition.res.oracle 1.57 KiB
129,134d128
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
< [eva:garbled-mix:write] addition.i:61: Warning:
< Assigning imprecise value to p14 because of misaligned read of addresses.
142a137,141
> [eva:garbled-mix:summary] Warning:
> Origins of garbled mix generated during analysis:
> addition.i:59: misaligned read of addresses
> (read in 1 statement, propagated through 2 statements)
> garbled mix of &{p1}
144c143
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
168c167
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
362,365d360
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
373c368,373
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
> Origins of garbled mix generated during analysis:
> addition.i:59: misaligned read of addresses
> (read in 1 statement, propagated through 2 statements)
> garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
398c398
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}