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] An interesting Cil tutorial

  • Subject: [Frama-c-discuss] An interesting Cil tutorial
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Fri, 8 Feb 2013 00:13:27 +0100
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