--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis - iterative function 2



Hello David,

Thank you.

>> Do you have a pencil & paper analysis that proves that such behaviour
>> should not occur? Is your algorithm numerically stable?

This function is part from aerospace control software and it works well.
We have tested the function in a isolated way with a input array and it
works well also.
We believe that the problem is the use of Frama_C_float_interval.

>> I would try to increase -slevel, to 10000 or even 100000.

We have increased the -slevel to 10000 and 100000.
It did not work, there was a overflow.

>> Frama-C like any other formal analysis tool is not a magic tool. You
>> should guide it based on your knowledge of the code you are analysing.

Anyway, we will carefully analyze the function again.

Thank you!
Best regards.
Rovedy, Luciana, Nanci










2013/4/3 David MENTRE <dmentre at linux-france.org>

> Hello,
>
> I probably have not more knowledge than you. Anyway, here are some
> comments.
>
> 2013/3/26 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> > The filter algorithm is implemented as a iterative process whose next
> > iteration is calculated based on the previous calculated value. In that
> > process, the successive calculations with the Cvo_Xf and Cvo_Fqrp
> variables
> > imply accumulated values that grow until reaching the maximum value of
> the
> > double variable.
>
> Do you have a pencil & paper analysis that proves that such behaviour
> should not occur? Is your algorithm numerically stable?
>
> > Is there an annotation or a command line option to deal with this type of
> > iterative algorithm?
>
> As far as I know, there is no such magic flag.
>
> I would try to increase -slevel, to 10000 or even 100000.
>
> Frama-C like any other formal analysis tool is not a magic tool. You
> should guide it based on your knowledge of the code you are analysing.
>
> Good luck!
> Best regards,
> david
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130404/180d0e01/attachment.html>