--- layout: fc_discuss_archives title: Message 25 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



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>