--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2010 ---
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