blob: 52cd279538affc550ae89497ac6b7184d5a35038 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
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/
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.
|
