compcert: Compiler you can formally trust¹

The CompCert C verified compiler is a high-assurance compiler for almost all of the C language (ISO C 2011), generating efficient code for the ARM, PowerPC, RISC-V and x86 processors.

... part of T2, get it here

URL: https://compcert.org/

Author: INRIA, AbsInt
Maintainer: Tomas Glozar <tglozar [at] gmail [dot] com>

License: Restricted
Status: Stable
Version: 3.15

CPU architectures: Does only support: x86-64

Download: https://github.com/AbsInt/CompCert/ CompCert-3.15.tar.gz

T2 source: compcert.cache
T2 source: compcert.desc
T2 source: configure-rocq-9.patch
T2 source: fix-mantissa-rewrite.patch
T2 source: pos-iter-same.patch
T2 source: ztac-import.patch

Build time (on reference hardware): 290% (relative to binutils)²

Installed size (on reference hardware): 8.30 MB, 19 files

Dependencies (build time detected): 00-dirtree bash binutils coreutils diffutils findutils gawk grep gzip make menhir ocaml ocaml-findlib rocq rocq-stdlib sed tar

Installed files (on reference hardware): n.a.

¹) This page was automatically generated from the T2 package source. Corrections, such as dead links, URL changes or typos need to be performed directly on that source.

²) Compatible with Linux From Scratch's "Standard Build Unit" (SBU).