Audit for maxnumf* and minnumf* intrinsics
#1248
Conversation
| // Kani does not produce the right expression (which is strange, because it's | ||
| // doing the same for similar expressions and they work) or CBMC is not picking | ||
| // it for some reason. | ||
| // Tracked in https://github.com/model-checking/kani/issues/1025 |
There was a problem hiding this comment.
Michael seemed to believe the issue there was fixed, have you talked to him about this case?
There was a problem hiding this comment.
I added a comment in #1025 about this. In principle, all these builtins should be fixed, but fmaxf is not working for some reason.
There was a problem hiding this comment.
fmaxf and fmaxl were affected, diffblue/cbmc#6904 fixes this.
There was a problem hiding this comment.
... which is now merged, and will be part of the next release.
There was a problem hiding this comment.
Since this is being tracked in #1025, I'm going to merge this PR in its current state. This means that the test will work if all goes well when the CBMC version is upgraded, causing the regression to fail unless the test is renamed @zhassan-aws @tedinski
Description of changes:
Restores and completes the audit for
maxnumf32,maxnumf64,minnumf32andminnumf64. These depend on a set of CBMC builtins (fmaxf,fmax,fminfandfmin) that handle NaN arguments in a specific way.Resolved issues:
Part of #1163
Part of #1025
Call-outs:
fmaxfis not working for an unknown reason, but I think we should restore it in order to ease debugging. The "fixme" test I added for it should work once the issue gets fixed in CBMC (if that's the reason) without needing any changes from Kani.Testing:
How is this change tested? Adds 4 tests (1 of them is a "fixme").
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.