--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2016 ---
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>