--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2016 ---
Hello, On Thu, Jul 28, 2016 at 9:13 PM, Timothy E. Wang <zepeem at gmail.com> wrote: > 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? > > try this: /*@ requires \is_finite(x); @ assigns \result \from x; @ ensures \is_finite(\result); @ ensures \result>=-1.0 && \result <=1.0; */ double _sin(double x); -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160728/75b0b09d/attachment.html>