--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on September 2013 ---
? 2013/9/3 21:40, frama-c-discuss-request at lists.gforge.inria.fr ??: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Introductory slides on Frama-C (David MENTRE) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 03 Sep 2013 15:27:23 +0200 > From: David MENTRE <d.mentre at fr.merce.mee.com> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: [Frama-c-discuss] Introductory slides on Frama-C > Message-ID: <5225E3BB.8010903 at fr.merce.mee.com> > Content-Type: text/plain; charset="iso-8859-1"; Format="flowed" > > Hello, > > I made some introductory slides on Frama-C. Please find them attached, > under an open-source licence (CC By-SA 3.0), with C code examples. Feel > free to re-use them, modify them, etc. > > Those slides build on previous slides made by Jochen Burghardt > (Fraunhofer First), Virgile Prevosto (CEA), Julien Signoles (CEA), > Nikolay Kosmatov (CEA) and Pascal Cuoq (TrustInSoft). > > Compared to those previous presentations, those slides: > * Present equally WP and Value analysis; > > * Present behaviors; > > * Present E-ACSL; > > * Avoid any mathematical notation (I am targeting C programmers), many > thanks to Jochen Burghardt for his slides in that regard. > > I tried to present an up-to-date view of Frama-C and its ecosystem. > > I would be glad to get any feedback about them: error, things to > improve, etc. > > In slide 47, behaviours found and not_found have opposite logical > condition for assumes clauses. However I find difficult to explain it > without going back to first order logic (!(a ==> b) eq. !(!a || b) eq. > ...) which I would like to avoid. Any idea on a way to explain that simply? > > Code examples where tested with Frama-C Fluorine. > > Best regards, > david Nice presentation. Very useful. :-) Thx.