Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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