package goblint-cil

C Intermediate Language (CIL)

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:

• Proper support for C99, (#9) and VLAs in particular (#5, #7)

• It uses Zarith instead of the deprecated Num

• Support for more recent OCaml versions (≥ 4.06)

• Large integer constants that do not fit in an OCaml int are represented as a string instead 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

Quickstart

Install the latest release of goblint-cil with opam:

opam install goblint-cil

Read the excellent CIL tutorial by Zachary Anderson, much of which still applies to goblint-cil. The repository referenced in that document has now moved here.

ATTENTION: Don't install the cil package. This is the unmaintained original version of CIL.

Installation from Source

Prerequisites:

• opam

• Some C compiler (preferably gcc)

• Perl

First create a local opam switch and install all dependencies:

opam switch create .

Then, run the following commands to build and install goblint-cil:

./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 directory:

./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 goblint-cil:

dune build
dune runtest    # runs the regression test suite

Usage

You can use cilly (installed in /usr/local/bin by default) as a drop-in replacement for 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"

TODO

• C11 support (#13)

License

goblint-cil is licensed under the BSD license. See LICENSE.