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

[Frama-c-discuss] Floor problem



-- 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