CIL is a front-end for the C programming language that facilitates
program analysis and transformation. CIL will parse and typecheck a
program, and compile it into a simplified subset of C.
goblint-cil is a fork of CIL that supports C99 as well as most of the
extensions of the GNU C. It makes many changes to the original CIL in an effort
to modernize it and keep up with the latest versions of the C language. Here is
an incomplete list of some of the ways
goblint-cil improves upon CIL:
Support for more recent OCaml versions (≥ 4.06)
Large integer constants that do not fit in an OCaml
intare represented as a
stringinstead of getting truncated
Syntactic search extension (#21)
More precise locations (with columns)
Some warnings were made optional
Unmaintained extensions (#30) were removed
Many bug fixes
Install the latest release of
goblint-cil with opam:
opam install goblint-cil
ATTENTION: Don't install the
cil package. This is the unmaintained
original version of CIL.
Installation from Source
Some C compiler (preferably
First create a local opam switch and install all dependencies:
opam switch create .
Then, run the following commands to build and install
./configure make make test # runs the regression test suite, optional make install # as root or using sudo
If you want to install to some other directory, you can tweak the prefix
during the configure step. For instance, to install in your local opam
./configure --prefix=`opam config var prefix`
Build with Dune
Alternatively, you can use dune to build
goblint-cil. Run the following
commands to build and test
dune build dune runtest # runs the regression test suite
You can use cilly (installed in
/usr/local/bin by default) as a drop-in
gcc to compile and link your programs.
You can also use
goblint-cil as a library to write your own programs. For
instance in the OCaml toplevel using Findlib:
$ ocaml Objective Caml version 4.00.1 # #use "topfind";; [...] # #require "cil";; [...] # Cil.cilVersion;; - : string = "1.8.2"
C11 support (#13)
goblint-cil is licensed under the BSD license. See LICENSE.