Previous Up Next

Chapter 2  Installation instructions

This chapter explains how to install CompCert C.

2.1  Obtaining CompCert C

CompCert C is distributed in source form. It can be freely downloaded from

http://compcert.inria.fr/download.html

The public release above can be used freely for evaluation, research and educational purposes, but commercial uses require purchasing a license from AbsInt (https://www.absint.com/). See the license conditions at http://compcert.inria.fr/doc/LICENSE for more details.

2.2  Prerequisites

The following software components are required to build, install and run CompCert C.

A C compiler: either GNU GCC version 3 to 6 or Windriver Diab C 5
CompCert C provides its own core compiler, of course, but relies on an external toolchain for preprocessing, assembling and linking. For simplicity, the external preprocessor, assembler and linker are invoked through the gcc driver command (for GCC) or dcc driver command (for Diab C). It is recommended to use GCC version 4.

Cross-compilation (e.g. generating PowerPC code from an x86 host) is possible but requires the installation of a matching GCC or Diab cross compiler and cross libraries.

For a Debian or Ubuntu GNU/Linux host, install the gcc package. For a Microsoft Windows host, install the Cygwin development environment from http://www.cygwin.com/.

For hosts running OS X 10.9 or newer install the command line tools via xcode-select --install in the Terminal application. The installation of the Xcode IDE is optional.

The Coq proof assistant, version 8.5pl2 or 8.5pl3
Coq is free software, available from http://coq.inria.fr/ and also as precompiled packages in several Linux distributions and in MacPorts for OS X.
The OCaml functional language, version 4.02 or later
OCaml is free software, available from http://caml.inria.fr/. The OPAM package manager (http://opam.ocaml.org) provides a convenient way to install OCaml and its companion tools. OCaml is also available as precompiled packages in most Linux distributions, in MacPorts for OS X, and in Cygwin for Windows.
The Menhir parser generator, version 20160303 or later
Menhir is free software, available from http://gallium.inria.fr/~fpottier/menhir/, and prepackaged in OPAM, MacPorts, and several Linux distributions.
Standard C library and header files
CompCert C does not provide its own implementation of the C standard library, relying on the standard library and header files of the host system.

For a Debian or Ubuntu GNU/Linux host, install the libc6-dev packages. If you are running a 64-bit version of Debian or Ubuntu, also install libc6-dev-i386.

Under OS X, install the Xcode programming environment version 5.0 or later, including the optional command-line tools. With earlier versions of Xcode, some standard C include files in /usr/include/ contain GCC-isms that cause errors when compiling with CompCert. Symptoms include references to undefined types uint16_t and uint32_t, or a type error when using the assert macro. The recommended solution is to upgrade to a more recent Xcode.

2.3  Installation

Unpacking

Unpack the .tgz archive from a terminal window:

    tar xzf compcert-version-number.tgz
    cd compcert-version-number
Configuration

Run the configure script with appropriate options:

./configure [option …] target

The mandatory target argument identifies the target platform. It must be one of the following:

ppc-linuxPowerPC, Linux
ppc-eabiPowerPC, EABI, with GNU or Unix tools
ppc-eabi-diabPowerPC, EABI, with Diab tools
arm-eabiARM, EABI, default calling conventions, little endian
arm-linuxsynonymous for arm-eabi
arm-eabihfARM, EABI, hard floating-point calling conventions, little endian
arm-hardfloatsynonymous for arm-eabihf
armeb-eabiARM, EABI, default calling conventions, big endian
armeb-linuxsynonymous for armeb-eabi
armeb-eabihfARM, EABI, hard floating-point calling conventions, big endian
armeb-hardfloatsynonymous for armeb-eabihf
x86_32-linuxx86 32 bits (IA32), Linux
x86_32-bsdx86 32 bits (IA32), BSD
x86_32-macosxx86 32 bits (IA32), OS X
x86_32-cygwinx86 32 bits (IA32), Cygwin environment under Windows
x86_64-linuxx86 64 bits (AMD64), Linux
x86_64-macosxx86 64 bits (AMD64), OS X

See section 1.4.1 for more information on the supported platforms. For ARM targets, the arm- or armeb- prefixes can be refined into:

armv6-Little Endian ARMv6 architecture with VFPv2 coprocessor
armv7a-Little Endian ARMv7-A architecture with VFPv3-D16 coprocessor
armv7r-Little Endian ARMv7-R architecture with VFPv3-D16 coprocessor
armv7m-Little Endian ARMv7-M architecture with VFPv3-D16 coprocessor
armebv6-Big Endian ARMv6 architecture with VFPv2 coprocessor
armebv7a-Big Endian ARMv7-A architecture with VFPv3-D16 coprocessor
armebv7r-Big Endian ARMv7-R architecture with VFPv3-D16 coprocessor
armebv7m-Big Endian ARMv7-M architecture with VFPv3-D16 coprocessor

The default arm- and armeb- prefixes correspond to armv7a- and armebv7a- respectively.

For PowerPC targets, the ppc- prefix can be refined into:

ppc64-PowerPC 64 bits
e5500-Freescale e5500 core (PowerPC 64 bits with EREF extensions)

The default ppc- prefix corresponds to PowerPC 32 bits.

For x86 targets in 32-bit mode, ia32- is recognized as synonymous for x86_32-.

The configure script recognizes the following options:

-bindir dir
Install the compiler’s executable ccomp in directory dir. The default location is /usr/local/bin.
-libdir dir
Install the compiler’s supporting library and header files in directory dir. The default location is /usr/local/lib/compcert.
-prefix dir
Equivalent to “-bindir dir/bin -libdir dir/lib/compcert”.
-toolprefix pref
Prefix the name of the external C compiler driver (gcc or dcc) with pref. This option is particularly useful if a cross-compiler is used. For example:
-no-runtime-lib
Do not compile, install, and use the libcompcert library that provides helper functions for 64-bit integer arithmetic. By default, this library is installed and linked with CompCert-generated executables. If it is not, some operations involving 64-bit integers (e.g. division, remainder, conversion to/from floating-point numbers) will not work.
-no-standard-headers
Do not install the CompCert-specific standard header files. By default, the following standard header files are installed and used: <float.h>, <stdarg.h>, <stdbool.h>, <stddef.h>, <stdnoreturn.h>, <iso646.h>, and <varargs.h>.

After successful completion, the configure script generates a configuration file Makefile.config and prints a summary of the configuration. If anything looks wrong, re-run ./configure with different options, or edit Makefile.config by hand.

Building the system

From the same directory where ./configure was executed, issue the command

    make all

or, on a N-core machine, to take advantage of parallel compilation:

    make -j N all

This re-checks all the Coq proofs, then extracts Caml code from the Coq specification and combines it with supporting hand-written Caml code to generate the executable for CompCert. This step can take about 30 minutes on a recent machine with a single core, but less if several cores are used.

Installation

CompCert is now ready to be installed. This will create the ccomp command (documented in chapter 3) in the binary directory selected during configuration, and install supporting .h and .a files in the library directory if needed. Become superuser if necessary and do

    make install

Previous Up Next