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] French slides to present Frama-C, value analysis and Jessie

  • Subject: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 1 Feb 2011 14:08:21 +0100
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F8778E50@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <AANLkTikQfC8Xz4x1CMP=XES-e7a=t-QB8WG1R5Xhex75@mail.gmail.com> <569C6D7D26484241A530B87F45ADE1F8778E50@AOFRWMBXRSC004.resources.atosorigin.local>
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