search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.18k stars 86 forks source link

Handle new `F16` and `F128` types #3069

Open zhassan-aws opened 6 months ago

zhassan-aws commented 6 months ago

This is a tracking issue for adding support for the new 16-bit and 128-bit floating-point types that are being added to Rust.

Upstream tracking issue: https://github.com/rust-lang/rust/issues/116909

tgross35 commented 6 months ago

Just FYI these are super unstable and will basically ICE if you do anything at all with them. Hopefully that will change in a couple weeks.

Thanks for being on top of it!

jaisnan commented 3 months ago

Some support is being added as of this PR: https://github.com/model-checking/kani/pull/3306. @zhassan-aws is this enough to close the issue or should we keep the issue open till they're fully stable?

tgross35 commented 3 months ago

FYI most of the ICE paths have been removed (const time as casting being the last thing until https://github.com/rust-lang/rust/pull/127032). Platform support is still weak though, we're having some problems getting compiler_builtins updated.

See https://github.com/rust-lang/rust/blob/c4c0897a262d42f26f89aaca16ed52457f6a4f05/library/std/build.rs#L78-L127 if you need a rough estimate of what works where (I'll be keeping that up to date as more support gets added)