--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on September 2013 ---
Hi David, That's a nice work. It could be put somewhere on the Frama-C wiki: on the tutorial page? (http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial) -- Julien On 09/03/2013 03:27 PM, David MENTRE wrote: > 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 > > > _______________________________________________ > 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