--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] value analysis and annotated post-conditions



Dear all,

A quick question. I am trying to get Value to take into account the
post-conditions that are part of the specifications of a library function.
I have a simple example below.  The output of the _sin function is
guaranteed to be within the interval [-1,1] but for some reason Value is
still returning [-MAX_FLOAT, MAX_FLOAT] for the variable y in the main
function. Any clue why this is happening?

Best,

Tim

#include "__fc_builtin.h"

/*@ requires \is_finite(x);
  @ assigns \result \from x;
  @ ensures \result>=-1.0 && \result <=1.0;
*/
double _sin(double x);

int main() {
double x=Frama_C_float_interval(-1.57,1.57);
double y=0.0;
y=_sin(x);
x=y;
return 1;
}

-- 
Future planes will have one pilot and one dog in the cockpit. The pilot's
job will be to feed the dog. The dog's job will be to make sure the pilot
stays away from the instruments.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160728/3fe49114/attachment.html>