package goblint-cil
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=6f7db2b495d183458ec887cf1869cd936b8cd6b8bb9dd9c22dda5d510f1b8927
sha512=d101affa1cb5ef0b9048892aa6d1f94117ae3705f999e12793cbe0f5bfa5a9a160f174ffe84afb98a146bf46c02872389d4c161d0857de5a2dc5474994122397
Description
This is a fork of the 'cil' package used for 'goblint'. Major changes include:
- Support for C99 and C11.
- Compatibility with modern OCaml versions.
- Use Zarith instead of Num and use that for integer constants.
- Improved locations with columns and spans.
- Removal of unmaintained extensions and MSVC support.
- Use dune instead of make and ocamlbuild.
- Many bug fixes.
Published: 21 Nov 2023
README
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, C11 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 C99 and C11.
Compatibility with modern OCaml versions.
Use Zarith instead of Num and use that for integer constants.
Improved locations with columns and spans.
Removal of unmaintained extensions and MSVC support.
Use dune instead of make and ocamlbuild.
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
GCC
Perl
First create a local opam switch and install all dependencies:
opam switch create .
Then, 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
To run a single test go to the build directory (e.g. _build/default/test
) and run e.g.:
dune exec -- make test/array1
You can also install goblint-cil
into the opam switch:
dune build @install
dune install
Usage
You can use cilly (installed in the opam switch) 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
OCaml version 4.14.0
# #use "topfind";;
[...]
# #require "goblint-cil";;
[...]
# GoblintCil.cilVersion;;
- : string = "2.0.3"
License
goblint-cil
is licensed under the BSD license. See LICENSE.
Dependencies (10)
- conf-gcc
- cppo
- conf-perl
- yojson
-
ppx_deriving_yojson
>= "3.2"
- stdlib-shims
- dune-configurator
-
dune
>= "2.7"
- zarith
-
ocaml
>= "4.05.0"
Used by (3)
-
goblint
>= "2.2.1" & < "2.4.0"
- imguiml
- lintcstubs