--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie



Hello St?phane,

2011/2/1 DUPRAT Stephane <STEPHANE.DUPRAT at atosorigin.com>:
> If it helps, here's my point of view about these remarks, which are from the side of an industrial user.

It helps! Thanks a lot.


> An other strategy for industrial (or not) developpers is to apply value analysis on sub-components of the program during its development.

How do you proceed in practice to do such analysis? Are you writing a
stub that generates required values with the Frama_C_* functions and
then call the top functions of the analysed sub-component (as in Skein
tutorial for example)? Are you using -lib-entry -main options? A
combination of both?

[...]
> About the remark about the size of annotation:
> Deductive proof is made for functional verification that are traditionnaly made by tests.
> And we have to know that tests are larger thant source code. And formal specification are smaller thant tests scripts.

Interesting point of view. I'll reused it. ;-)

>> Overall, I already asked for it but having some examples (or
>> better an article that could be cited!) detailing how Frama-C
>> is applied on some industrial code (size of code, most
>> important issues and approaches used to work around them,
>> results obtained) would be very useful.
>
> I will try to export more concrete exemple.

I'm looking forward to see them.

And I would also be interested in experience report on people
integrating Frama-C analyses in their development cycle, e.g. regular
call of Frama-C in batch mode on a source version control checkout.

Thanks a lot for the information,
Best regards,
david