--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floor problem



Yes, of course!
And indeed, the specification from Claude is much better.
	L.

>> It is interesting to notice that WP translates a double d into an int with `to_uint32(truncate (d))`.
>> So in your case, you should use a driver directive like:
>> ```
>> logic real \floor(real) = "truncate" ;
>> ```
>> However, I?m afraid `truncate` is not yet axiomatized completely, but you can provide supplementary axioms about the `truncate` function on your own.