--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on November 2014 ---
-- Lo?c Correnson (2014-11-18) > > > 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. Hi Lo?c, isn't it the case that "truncate" rounds towards zero, while \floor is meant to round towards -infinity? If so, your definition above only holds for non-negative values of arguments. -- Yannick Moy, Senior Software Engineer, AdaCore