This is a simple tutorial about how to use the CIL compiler frontend to do
static and dynamic program analysis.

Author: Zach Anderson (

1. Intro
2. Building and Installing
3. Files
4. Bugs and Feedback
5. Citation

1. Intro:

CIL is a frontend for C compilers. It takes C code as input, which can then be
analyzed or instrumented, and then spits out C code, which can be passed to
your favorite C compiler. This process can be automated such that your CIL-based
front-end can be made to look like gcc, or whatever, and used directly in your
build process. This tutorial creates such a frontend, and demonstrates, in
tutorial form, some nifty things that might be done with it.

2a. Building and Installing (Ubuntu):

There are a few dependencies:
. Everything you need to build C programs
. OCaml
. cmake
  - Ubuntu packages: cmake cmake-data
  - Build and install from
  - There is a problem building against versions 1.7.{1,2}. 
    If you encounter errors while linking, try the tip of
    the CIL git repo, or an earlier version.
. ocamlgraph
  - Ubuntu package: libocamlgraph-ocaml-dev
. Please let me know if I've forgotten anything

Dependencies only for the theorem proving example (
. why3
. theorem provers (e.g. alt-ergo)
. pass -DBUILD_TUT11=true to cmake to include this example

Dependencies only for the automated test generation example (
. Yices SMT solver (
. ocamlyices (
. pass -DBUILD_TUT15=true to cmake to include this example

Then, to obtain and build:

$ hg clone
$ mkdir build
$ cd build
$ cmake [-DBUILD_TUT11=true] [-DBUILD_TUT15=true] ..
$ make
$ sudo make install

Then, enter the test directory and build a program like so:

$ ciltutcc -o tut1 --enable-tut1 test/tut1.c
test/tut1.c:9: Deleted assignment: #line 9 "test/tut1.c"
deleted = 0;
$ ./tut1
r = 37

The generated ciltutcc takes all of the usual gcc arguments, in addition to the

--trace       - shows all of the commands run
--save-temps  - saves all of the intermediate files
--enable-tutN - enables the pass defined by

And others that you can define in src/

If you do:

$ ciltutcc --save-temps -o test1 test1.c

A file called test1.cil.c will be created showing the source file created by
the frontend before it is passed on to gcc.

  [Ocamlyices installation]

$ git clone git://
$ cd ocamlyices
(Download yices for your platform from
 into the ocamlyices directory. If the version statically linked with gmp
 doesn't work, then try the dynamically linked version.)
$ sudo ./ [the tar.gz file you dl'd]
$ autoconf [if needed]
$ ./configure
$ make
$ sudo make install

  [Alt-Ergo installation]

$ wget
$ tar zxf alt-ergo-0.94.tar.gz
$ cd alt-ergo-0.94
$ autoconf [if needed]
$ ./configure
$ make
$ sudo make install

  [Why3 Installation]

$ git clone
$ cd why3
$ autoconf [if needed]
$ ./configure
$ make
$ make byte
$ sudo make install
$ sudo make install-lib
$ why3config

2b. Building and Installing (Mac OS X)

This project should build and install on 10.8 using the MacPorts OCaml install.
I have not yet tried to get tutorials 11 and 15 running on it yet, though.

(It appears that there is some problem with linking the calls from C -> OCaml
in tut15.c, but Why3, Alt-Ergo, and Ocamlyices *should* build without
problems---I just haven't tried it yet.)

Anyway, here's what you'll need to do:
1. install XCode and be sure to install the "Unix" or "Command line" tools.
2. install MacPorts from
3. Do:

$ sudo port install ocaml ocaml-findlib lablgl lablgtk lablgtk2 mercurial cmake

4. Install CIL:

$ git clone git://
$ cd cil
$ ./configure; make; sudo make install

5. Build cil-tutorial

As above

6. Let me know if I've missed any steps =)

3. Files:

CMakeLists.txt - Add additional filenames to CILTUT_SRC on line 48 to add
additional OCaml modules. Other parts of the Makefile can probably remain
unchanged unless you need to do something weird.

src/ - Reads in a source file, calls into the various tutorial modules,
spits out the result. Hopefully it is obvious where to add code to call into
any new modules that you write.

src/ - Defines command line options.

src/tut*.ml - Tutorial modules explaining how to use CIL.

ciltut-include/ciltut.h - Various function and macro definitions needed for
building ciltut-lib and the things in test/.

ciltut-lib/ - The runtime library. The files in src/tut*.c
go along with the corresponding .ml files. ciltut_libc.c has utility functions.
To add new code to the runtime, add file names to the CMakeLists.txt file under
the src/ directory in the obvious place.

lib/ - A perl script that sits in front of the actual compiler
frontend. It is used for massaging the command line a bit. For example, it makes
sure that the final result links against the code in ciltut-lib/.

test/tut*.c - Test programs for the various tutorial modules.

LICENSE - All the code in this project is licensed under a standard 3-clause
BSD license.

4. Bugs, and Feedback:

Please use the issue tracker on bitbucket to report bugs, make suggestions,
give feedback, etc..

5. Citation:

If you use cil-template as a starting point for your project, please make the
following citation:

Zachary Anderson. A CIL Tutorial: Using CIL for Language Extensions and Program
  Analysis, <the date given on the document>. <>.

At the time this README file was written, this evaluates to:

Zachary Anderson. A CIL Tutorial: Using CIL for Language Extensions and Program
  Analysis, January 2013.

Or in bibtex format:

  title = {A {CIL} Tutorial: Using {CIL} for Language Extensions and Program Analysis},
  author = {Zachary Anderson},
  month = Jan,
  year = 2013,
  note = {\url{}},