Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

>
>
> >> 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.
>

Really? So what intervals do Cvo_Fqrp, Cvo_Xf[0] and Cvo_Xf[1] evolve in
with the initial conditions in your main()?

As David said, it would help if you knew what you are trying to prove. You
can do it by trial and error, but it would be faster to go straight for the
intervals that can really happen. It will be long enough to go straight for
the solution.


> We believe that the problem is the use of Frama_C_float_interval.


There is only one documented method for getting near-optimal results from
Frama-C's value analysis.

Sometimes the problem is that the property you are trying to establish is
out of reach of this single universal method, and that may be the case for
your example. But, for now, the problem is not that. The problem is that
you have not followed the method to the end yet.

>> 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.


The property you are trying to establish, if true, is true because of the
relation that holds between Cvo_Fqrp, Cvo_Xf[0] and Cvo_Xf[1] at each
iteration. You should have already gotten used to the idea that the value
analysis was fundamentally a non-relational analysis where relations are
represented, when necessary, by separation of abstract states.

Option slevel separates abstract states along the execution paths of the
program.

What do you do next when separating along the execution paths of the
program does not provide the precision you are aiming for?

How does the square example in section ?Case analysis? of the manual work?

How does this tutorial work:
http://blog.frama-c.com/index.php?post/2011/06/02/Skein-7 ?

How does this tutorial work:
http://blog.frama-c.com/index.php?post/2011/03/26/Helping-the-value-analysis-2?

How does this tutorial work:
http://blog.frama-c.com/index.php?post/2011/02/10/Verifying-numerical-precision-part-2?

What do the solutions in these tutorials have in common?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130405/82534c8b/attachment.html>