Source: compcert
Section: non-free/devel
Priority: extra
Maintainer: Benjamin Barenblat <bbaren@mit.edu>
Build-Depends:
 coq (>= 8.4pl1),
 coq (<< 8.4pl6),
 debhelper (>= 9),
 dh-exec,
 menhir (>= 20140422),
 ocaml-nox (>= 4.00.0)
Standards-Version: 3.9.6
Homepage: http://compcert.inria.fr/
Vcs-Browser: https://benjamin.barenblat.name/gitweb/?p=debian-compcert.git
Vcs-Git: git://benjamin.barenblat.name/debian-compcert.git

Package: compcert
Architecture: i386
Depends: ${shlibs:Depends}, ${misc:Depends}
Description: Formally verified C compiler
 CompCert is an optimizing C compiler produced by INRIA.  It supports a
 substantial subset of C99 and a superset of MISRA-C 2004, and it produces
 code roughly comparable in performance to GCC -O1 specified.  Furthermore, it
 has been mathematically proven bug-free: An executable generated by CompCert
 will behave exactly as specified by the semantics of the original C source.