--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] An interesting Cil tutorial



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