--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pragma declaration problem



Hello,

this is a very partial answer because I am not a specialist of Jessie.

> With this example:
> #pragma JessieFloatModel( < arg> )
> /*@
> requires radius>0;
> ensures \abs(\result - 3.141592654*2.0*radius) <= 0.01;
> */
> float Perimeter(float radius) {
> ??? return 2.0*3.14*radius;
> }

> - strict: it couldn't solve the problem on overflow.

In the strict model, floating-point overflows are considered as
unwanted errors. Your function can produce floating-point overflows,
(it multiplies a radius argument that can be arbitrarily large), so
Jessie should definitely not "solve" the problem on overflow in this
case. Instead, there is a bug in your function and Jessie has
correctly found it.

I think you want a precondition on your function that, if satisfied,
prevents any overflow from happening. But you also want a precondition
that prevents the absolute different between 3.141592654*2.0*radius
and 2.0*3.14*radius to exceed 0.01, which is even more limiting: since
the error of your function is about 2.0*radius*0.0016, radius cannot
exceed about 3.0. I hope I am not making any stupid computation
mistake, because I do not have the automatic provers that would allow
me to check that the specification is indeed verified with the
additional clause requires radius <= 3.0 ;

Pascal