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