# --- T2-COPYRIGHT-BEGIN ---
# t2/package/*/compcert/compcert.desc
# Copyright (C) 2025 The T2 SDE Project
# SPDX-License-Identifier: GPL-2.0
# --- T2-COPYRIGHT-END ---

[I] Compiler you can formally trust

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

[U] https://compcert.org/

[A] INRIA, AbsInt
[M] Tomas Glozar <tglozar@gmail.com>

[C] extra/development
[R] + x86-64

[L] Restricted
[S] Stable
[V] 3.15
[P] X -----5---9 510.200

var_append confopt ' ' 'x86_64-linux' # TODO: Support other architectures
var_append confopt ' ' '-ignore-coq-version -ignore-ocaml-version'

[D] 6f8d56d5639a608176268bc57092769944048b1a8ab9e216b54eab10 CompCert-3.15.tar.gz https://github.com/AbsInt/CompCert/archive/refs/tags/v3.15/