You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
…nly (rust-lang#1117)
rustc reasonably translates if statements at end of a loop body to
backwards jumps to the loop head. This, however, causes CBMC's symbolic
execution to spuriously treat these as nested loops. This commit now
enables a rewrite step that had previously been built for exactly such
cases.
This treatment as nested loops implied that seemingly lower unwinding
bounds were sufficient (as the loop unwinding counter got reset). Three
of the tests exhibited this behaviour, which now makes larger unwinding
bounds necessary.
Fixes: rust-lang#1046
Co-authored-by: Daniel Schwartz-Narbonne <dsn@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Co-authored-by: Daniel Schwartz-Narbonne <dsn@amazon.com>
The compiler tries to use floats as the cases in an LLVM switch, which does not work.
The text was updated successfully, but these errors were encountered: