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: STEPHANE.DUPRAT at atosorigin.com (DUPRAT Stephane)
  • Date: Tue, 1 Feb 2011 11:09:22 +0000
  • In-reply-to: <AANLkTikQfC8Xz4x1CMP=XES-e7a=t-QB8WG1R5Xhex75@mail.gmail.com>
 Hello,

Thanks for this return of experience.
If it helps, here's my point of view about these remarks, which are from the side of an industrial user.


> -----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 09:39
> ? : Frama-C public discussion
> Objet : Re: [Frama-c-discuss] French slides to present
> Frama-C, value analysis and Jessie
>
> Hello Benjamin,
>
> 2011/2/1 MONATE Benjamin 205998 <Benjamin.MONATE at cea.fr>:
> > Thanks a lot for making your slides available: they provide
> a nice and precise overview of two plugins of Frama-C.
>
> Thanks.
>
> > What kind of remarks/questions did you get?
>
> Regarding Value analysis (also presented in another lesson):
> mostly questions regarding lack of precision on values,
> especially regarding loops (and "all programs are loops",
> quoting a participant). I talked about the skein analysis in
> Value analysis tutorial which is able to provide some
> interesting result and the use of -slevel. But I lack first
> hand practice on applying value analysis to large code. Is it
> a real issue on control code, for example?

Applying value analysis on the whole code of a large project is a strategy with very added-value, but the process could be very long and is not always a well controlled activity regarding the costs. It depends a lot of the analysed program.
An other strategy for industrial (or not) developpers is to apply value analysis on sub-components of the program during its development.
This strategy is possible thanks to the ACSL language that is able ot replace external component by their formal specification (in a restricted way, for the moment).
On the other hand, size of the subcomponents that are smallers make the analysis easier and faster. It is thus possible to work in an iterative way.
I'm personnaly convinced that use of value analysis is 1/ possible and 2/ adapted to different contexts and not only those of industrial and critical software.

>
> Regarding Jessie: "annotations have the same size as code!"
> and "what about error in annotations?". For the former
> remark, I could only tell that this was the price to pay to
> be able to *prove* code in all its generality. Regarding the
> latter remark, I told it would not be possible to prove the
> goals, but a was lacking convincing arguments.
> One of the attendee followed a lesson on code proof using a
> functional approach and PVS powerful tactics made by a
> researcher at INRIA Rennes (Thomas Genet) and told the
> approach was more powerful and simple. I answered that the
> discussion between the two approaches is still on-going. :-)

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.
For the second remark, formal specification are specification that need a review.
We have to be care in case of using a lot of axiomatic and complex formal specification.

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

Regards,

Stephane

>
> Sincerely yours,
> 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
>
>
--
-----------------------------------------------
Stephane DUPRAT
Innovation et Bureau m?thode
R?gion Midi-Pyr?n?es - Agence de Toulouse
6 Impasse Alice Guy
B.P. 43045
31024 - Toulouse Cedex 03
T?l : 05 34 36 32 78
Fax : 05 34 36 31 00

mailto :stephane.duprat at atosorigin.com

=======================================================================
Ce  message  electronique  est  confidentiel.   Il  peut  contenir  des
informations  protegees  par  le  secret  professionnel,  le  secret de
fabrication ou  autres regles legales.  Si vous recevez ce message  par
erreur,  il vous est interdit  de le reproduire  ou de le distribuer en
tout ou en partie,  ou de le divulguer de quelque maniere que ce soit a
quelque  personne  que ce soit.  Nous vous prions  de bien  vouloir  en
informer  Atos Origin,  par telephone  ou par retour  d'e-mail  puis de
detruire le message et toutes copies de votre systeme informatique.  Le
contenu  de ce message  ne reflete pas  necessairement  ni les opinions
d'Atos Origin  ni celle des membres de son groupe.  Bien que l'emetteur
de ce message  ait fait  tout son possible  pour maintenir  son systeme
informatique sans virus,  il ne peut garantir que cette transmission ne
comporte  aucun virus  et il ne pourra  etre tenu  pour responsable  de
quelque dommage que ce soit resultant de la transmission d'un virus.
=======================================================================
This   electronic  transmission   is  confidential.   It  may   contain
information  that  is  covered  by legal professional  privilege,  work
product  immunity  or other  legal rules.  If  you have  received  this
transmission in error,  you must not copy or distribute this message or
any part  of it  or otherwise disclose  its contents to anyone.  Please
notify  Atos Origin Legal Services  by telephone or return E-mail,  and
then delete this transmission  and any copies of it  from your computer
system.  The views  expressed  in this  electronic transmission  do not
necessarily reflect those of Atos Origin SA or any member of its group.
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.
=======================================================================

________________________________


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.