--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2014 ---
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.