--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2013 ---
Hello list, Zachary Anderson (in cc:) recently posted a very interesting Cil tutorial [1] on the Cil Users list [2]. The introductory chapters are very clear, even when they tackle not-so-simple parts of Cil such as the (forward) dataflow in cil/src/ext/Dataflow. The later ones deal with more involved subject, such as a simple WP (chapter 11), or a program instrumentation to measure cache misses (chapter 10). It would be quite useful to translate some of those chapters to Frama-C's Cil, as they would make an excellent introduction to the "AST manipulation" part of the platform. Using some fragments of ACSL instead of the in-house annotation language of chapter 11 could furthermore provide a first taste of the logic part of our Cil. If some of you are interested in helping in this translation, we could set up a collaborative Git repo. Please let us know if you are interested! [1] http://www.inf.ethz.ch/personal/azachary/teaching/ciltut.pdf [2] http://www.mail-archive.com/cil-users at lists.sourceforge.net/ -- Boris