Rounding intrinsics are not working #1025
Description
Calling rounding intrinsics (and likely other math intrinsics) results in an "assertion false". For example, the following code:
fn main() {
let x: f32 = kani::any();
let x_ceil = unsafe { std::intrinsics::ceilf32(x) };
}returns this:
RESULTS:
Check 1: ceilf.assertion.1
- Status: FAILURE
- Description: "assertion false"
- Location: <builtin-library-ceilf> in function ceilf
Check 2: <T as kani::Arbitrary>::any.assertion.1
- Status: SUCCESS
- Description: "resume instruction"
- Location: ~/kani/library/kani/src/arbitrary.rs:17:5 in function <T as kani::Arbitrary>::any
SUMMARY:
** 1 of 2 failed
Failed Checks: assertion false
VERIFICATION:- FAILED
It's still not clear what intrinsics are affected, but at least rounding intrinsics (ceil, floor, round) are not working. This is probably due because the irep expressions we generate for them are not exposed in CBMC, or because they are not the right ones.