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

David,

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

The most effective is to use the -lib-entry mode.
The simplest way is just to add somme requires to the entry-point that restrict the state produced by -lib-entry to a nominal state of the calling context.
But generally, we need to write a "caller" that is a C function that calls the "to-be-analysed" function.
This caller defines the context, using C language, but also annotations, and/or Frama-C builtin functions. This need to know what are the good hypothesis to use the called function, and as a consequence need a minimal effort of design.
In this modular approach we also need to write stubs for called functions thar are not part of the verified sub-component. For that, there's also different solutions more or less easy to use:
  - the minimal : just the prototype if there is no other side effect than thoses automatically generated from the signature of the function
  - the prototype + ACSL contract with assigns clauses (encrease sid-effects) and ensures (more precise contract)
  - a C language stub defining correct side-effect with the required precision.
That's for the method, roughly speaking.

> 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.
Tooling is an other keypoint of industrial use.
We are currently working on an integration of Frama-C in Eclipse, with batch analysis, making easier the use of the tool in an iterative process.
We will be pleased to make it available in next months to user.

Regards,

St?phane


> -----Message d'origine-----
> De : frama-c-discuss-bounces at lists.gforge.inria.fr
> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la
> part de David MENTRE
> Envoy? : mardi 1 f?vrier 2011 14:08
> ? : Frama-C public discussion
> Objet : Re: [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
>
> _______________________________________________
> 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
>
>
________________________________


Ce message et les pi?ces jointes sont confidentiels et r?serv?s ? l'usage exclusif de ses destinataires. Il peut ?galement ?tre prot?g? par le secret professionnel. Si vous recevez ce message par erreur, merci d'en avertir imm?diatement l'exp?diteur et de le d?truire. L'int?grit? du message ne pouvant ?tre assur?e sur Internet, la responsabilit? du groupe Atos Origin ne pourra ?tre recherch?e quant au contenu de ce message. Bien que les meilleurs efforts soient faits pour maintenir cette transmission exempte de tout virus, l'exp?diteur ne donne aucune garantie ? cet ?gard et sa responsabilit? ne saurait ?tre recherch?e pour tout dommage r?sultant d'un virus transmis.

This e-mail and the documents attached are confidential and intended solely for the addressee; it may also be privileged. If you receive this e-mail in error, please notify the sender immediately and destroy it. As its integrity cannot be secured on the Internet, the Atos Origin group liability cannot be triggered for the message content. Although the sender endeavours to maintain a computer virus-free network, the sender does not warrant that this transmission is virus-free and will not be liable for any damages resulting from any virus transmitted.