make cil_exp_of_linexpr1 work with fractional expressions#1493
Conversation
DrMichaelPetter
added
bug
in progress
relational
michael-schwarz
left a comment
michael-schwarz
left a comment
There was a problem hiding this comment.
It would be good to add a (cram) test where we test that the information now actually appears in the witness. Maybe @sim642 can help setting that up?
| if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *) | ||
| None | ||
| else match scalar with | ||
| | Float f -> if Stdlib.Float.is_integer f then Some (Q.of_float f) else None |
There was a problem hiding this comment.
According to Zarith documentation, Q.of_float is exact, so shouldn't this also work for non-integers?
There was a problem hiding this comment.
We could, but in general, I would expect this case to happen, if we come from a float-based apron analysis. Correct me if I am wrong in the following argumentation:
These floats would likely stem from a floating point based analysis in apron, and thus would probably lead to very large denominators due to some +/-1 rounding in the low end of the mantissa. This might not hurt soundness so bad, since the result is only used to perform a scaling on the whole equality, but still the outcome might be very scary looking. In this implementation, I opted for a more conservative approach, just ignoring these floats.
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
|
I should try this on our relational witnesses for Freiburg to see if this produces any new ones we couldn't before. |
3 participants
Fixes #1328 , use Q instead of Z to extract coefficients, and then scale the coefficient with the lcm of their denominators.