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

[Frama-c-discuss] Axiomatic Definition of Rounding Function



Thanks for your explanation. For the work-around, where do I need to put
the cast to? I have tried

   @ axiom rounded_value:
   @    \forall real x ; -0.5  <= (x - (real) lround(x)) <= 0.5;

but this is not allowed.

Frank