diff options
Diffstat (limited to 'debian/control')
| -rw-r--r-- | debian/control | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..27dd26a --- /dev/null +++ b/debian/control @@ -0,0 +1,22 @@ +Source: compcert +Section: non-free/devel +Priority: extra +Maintainer: Benjamin Barenblat <bbaren@mit.edu> +Build-Depends: + coq (>= 8.4pl1), + coq (<< 8.4pl6), + debhelper (>= 9), + 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. |