diff options
| -rw-r--r-- | debian/.gitignore | 6 | ||||
| -rw-r--r-- | debian/changelog | 5 | ||||
| -rw-r--r-- | debian/compat | 1 | ||||
| -rw-r--r-- | debian/control | 22 | ||||
| -rw-r--r-- | debian/copyright | 390 | ||||
| -rw-r--r-- | debian/gbp.conf | 2 | ||||
| -rwxr-xr-x | debian/rules | 12 | ||||
| -rw-r--r-- | debian/source/format | 1 | ||||
| -rw-r--r-- | debian/watch | 2 |
9 files changed, 441 insertions, 0 deletions
diff --git a/debian/.gitignore b/debian/.gitignore new file mode 100644 index 0000000..dac301c --- /dev/null +++ b/debian/.gitignore @@ -0,0 +1,6 @@ +# .gitignore -*- conf -*- + +# Editor backup files +*~ +\#* +.\#* diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..5f9ea8c --- /dev/null +++ b/debian/changelog @@ -0,0 +1,5 @@ +compcert (2.4-1) UNRELEASED; urgency=medium + + * Initial release. + + -- Benjamin Barenblat <bbaren@mit.edu> Thu, 05 Feb 2015 15:14:50 -0500 diff --git a/debian/compat b/debian/compat new file mode 100644 index 0000000..ec63514 --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +9 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. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 0000000..7808079 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,390 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: CompCert +Upstream-Contact: compcert@yquem.inria.fr +Source: https://github.com/AbsInt/CompCert +Copyright: + 2004-2014 Institut National de Recherche en Informatique et en Automatique + (INRIA) +License: INRIA-non-commercial +Disclaimer: + This package is not part of the Debian distribution. It is provided in + the non-free archive area as a convenience to Debian users. + . + The contents of this package cannot be distributed as part of the Debian + distribution because the INRIA Non-Commercial License Agreement does not allow + commercial use. + +Files: * +Copyright: + 2004-2014 Institut National de Recherche en Informatique et en Automatique +License: INRIA-non-commercial + +Files: + arm/Archi.v + arm/CBuiltins.ml + backend/Cminor.v + backend/CMlexer.mli backend/CMlexer.mll + backend/CMparser.mly + backend/CMtypecheck.ml backend/CMtypecheck.mli + backend/PrintCminor.ml + cfrontend/C2C.ml + cfrontend/Clight.v + cfrontend/ClightBigstep.v + cfrontend/Cop.v + cfrontend/CPragmas.ml + cfrontend/Csem.v + cfrontend/Cstrategy.v + cfrontend/Csyntax.v + cfrontend/Ctypes.v + cfrontend/PrintClight.ml + cfrontend/PrintCsyntax.ml + common/AST.v + common/Behaviors.v + common/Errors.v + common/Events.v + common/Globalenvs.v + common/Memdata.v + common/Memory.v + common/Memtype.v + common/Sections.ml common/Sections.mli + common/Smallstep.v + common/Subtyping.v + common/Switch.v + common/Unityping.v + common/Values.v + cparser/* + doc/coq2html.mll + exportclight/* + ia32/Archi.v + ia32/CBuiltins.ml + lib/* + Makefile + powerpc/Archi.v + powerpc/CBuiltins.ml +Copyright: + 2004-2014 Institut National de Recherche en Informatique et en Automatique +License: INRIA-non-commercial or GPL-2+ + +Files: debian/* +Copyright: 2015 Benjamin Barenblat <bbaren@mit.edu> +License: GPL-3+ + +Files: flocq/* +Copyright: + 2010-2013 Sylvie Boldo + 2010-2013 Guillaume Melquiond +License: LGPL-3+ + +Files: runtime/arm/* runtime/ia32/* runtime/powerpc/* runtime/test/* +Copyright: 2013 Institut National de Recherche en Informatique et en Automatique +License: BSD-3-clause + +Files: test/c/aes.c +Copyright: none (public domain) +License: public-domain + The authors of this file claim that it is "in the public domain". No further + clarification is provided. + +Files: test/c/almabench.c +Copyright: none (public domain) +License: public-domain + The author writes: "No rights reserved. This is public domain software, for + use by anyone." + +Files: + test/c/binarytrees.c + test/c/fannkuch.c + test/c/knucleotide.c + test/c/mandelbrot.c + test/c/nbody.c + test/c/nsieve.c test/c/nsievebits.c + test/c/spectral.c +Copyright: + 2004-2008 Brent Fulgham + 2005-2015 Isaac Gouy +License: BSD-3-clause + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions are met: + . + - Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + - Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + - Neither the name of "The Computer Language Benchmarks Game" nor the name of + "The Computer Language Shootout Benchmarks" nor the names of its + contributors may be used to endorse or promote products derived from this + software without specific prior written permission. + . + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND + ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED + WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR + ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES + (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON + ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +Files: test/c/bisect.c +Copyright: + 1996 McGill University + 1996 McCAT System Group + 1996 ACAPS Benchmark Administrator <benadmin@acaps.cs.mcgill.ca> +License: Free-simple + This program is free software; you can redistribute it and/or modify it + provided this copyright notice is maintained. + . + This program is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. + +Files: test/c/siphash24.c +Copyright: + 2012 Jean-Philippe Aumasson <jeanphilippe.aumasson@gmail.com> + 2012 Daniel J. Bernstein <djb@cr.yp.to> +License: CC0 + +Files: + test/compression/arcode.c test/compression/arcode.h + test/compression/armain.c +Copyright: 2004, 2006, 2007 Michael Dipperstein <mdipper@cs.ucsb.edu> +License: LGPL-3+ + +Files: test/compression/bitfile.c test/compression/bitfile.h +Copyright: 2004-2007 Michael Dipperstein <mdipper@cs.ucsb.edu> +License: LGPL-3+ + +Files: + test/compression/lzdecode.c + test/compression/lzencode.c + test/compression/lzhash.c + test/compression/lzlocal.h + test/compression/lzss.h + test/compression/lzssmain.c + test/compression/lzvars.c +Copyright: 2003-2007 Michael Dipperstein <mdipper@alumni.engr.ucsb.edu> +License: LGPL-3+ + +Files: + test/compression/lzwdecode.c + test/compression/lzwencode.c + test/compression/lzw.h + test/compression/lzwmain.c +Copyright: 2005, 2007 Michael Dipperstein <mdipper@alumni.engr.ucsb.edu> +License: LGPL-3+ + +Files: test/compression/optlist.c test/compression/optlist.h +Copyright: 2007 Michael Dipperstein <mdipper@alumni.engr.ucsb.edu> +License: LGPL-3+ + +Files: test/spass/* +Copyright: 1996-2001 MPI für Informatik +License: GPL-2+ + +Files: test/spass/COPYING +License: FSF-simple + Everyone is permitted to copy and distribute verbatim copies of this license + document, but changing it is not allowed. + +Files: + test/spass/dfgparser.c test/spass/dfgparser.h + test/spass/iaparser.c test/spass/iaparser.h +Copyright: 1984, 1989, 1990, 2000-2002 Free Software Foundation, Inc. +License: GPL-2+ with Bison-generated exception + +License: BSD-3-clause + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + * Neither the name of the <organization> nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + . + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND + ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED + WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY DIRECT, + INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE + OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF + ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +License: CC0 + To the extent possible under law, the author(s) have dedicated all copyright + and related and neighboring rights to this software to the public domain + worldwide. This software is distributed without any warranty. + . + You should have received a copy of the CC0 Public Domain Dedication along with + this software. If not, see <http://creativecommons.org/publicdomain/zero/1.0/>. + +License: GPL-2+ + This program is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation; either version 2 of the License, or (at your option) any later + version. + . + This program is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License along with + this program; if not, write to the Free Software Foundation, Inc., 51 Franklin + Street, Fifth Floor, Boston, MA 02110-1301, USA. + . + On Debian systems, the complete text of the GNU General Public License version + 2 can be found in "/usr/share/common-licenses/GPL-2". + +License: GPL-2+ with Bison-generated exception + This program is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation; either version 2, or (at your option) any later version. + . + This program is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License along with + this program; if not, write to the Free Software Foundation, Inc., 51 Franklin + Street, Fifth Floor, Boston, MA 02110-1301, USA. + . + On Debian systems, the complete text of the GNU General Public License version + 2 can be found in "/usr/share/common-licenses/GPL-2". + . + As a special exception, you may create a larger work that contains part or all + of the Bison parser skeleton and distribute that work under terms of your + choice, so long as that work isn't itself a parser generator using the skeleton + or a modified version thereof as a parser skeleton. Alternatively, if you + modify or redistribute the parser skeleton itself, you may (at your option) + remove this special exception, which will cause the skeleton and the resulting + Bison output files to be licensed under the GNU General Public License without + this special exception. + +License: GPL-3+ + This program is free software: you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation, either version 3 of the License, or (at your option) any later + version. + . + This program is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License along with + this program. If not, see <http://www.gnu.org/licenses/>. + . + On Debian systems, the complete text of the GNU General Public License version + 3 can be found in "/usr/share/common-licenses/GPL-3". + +License: INRIA-non-commercial + INRIA Non-Commercial License Agreement for the CompCert verified compiler + . + 1. Background: Institut National de Recherche en Informatique et en + Automatique (the "Provider") developed the CompCert verified + compiler (the "Software") and seeks to distribute the Software for + public use and benefit. + . + 2. Grant: The Provider hereby grants to you a revocable, nonexclusive, + nontransferable, royalty-free and worldwide license (the "License") + to use the Software solely for educational, research, or evaluation + purposes, in accordance with Paragraph 3 below and subject to the + terms and conditions of this License Agreement (the + "Agreement"). The License entitles you to use the Software to + conduct research or education and to create Derivative Works solely + for academic, non-commercial research endeavors of the Licensee (A + "Derivative Work" is a work that is a modification of, enhancement + to, derived from, or based upon the Software). + . + 3. Limitations on Use: The License is limited to noncommercial + use. Noncommercial use relates only to educational, research, + personal or evaluation purposes. Any other use is commercial use. + You may not use the Software in connection with any activities + which purpose is to procure a commercial gain to you or others. + . + 4. Limitations on Distribution: If you distribute the Software or any + derivative works of the Software, you will distribute them under + the same terms and conditions as in this License, and you will not + grant other rights to the Software or derivative works that are + different from those provided by this License. + . + 5. Ownership: The Software and the accompanying documentation are + licensed, not sold, to you. The Software is a proprietary product + of the Provider and is protected under French copyright law and + international treaty revisions. The Provider retains all rights not + specifically granted to you hereunder, including ownership of the + Software and all copyrights, trade secrets, or other intellectual + property rights in the Software and any accompanying information. + . + 6. Publication Credit: You agree to acknowledge the INRIA CompCert + research project with appropriate citations in any publication or + presentation containing research results obtained in whole or in + part through the use of the Software. + . + 7. Term of License: The License is effective upon receipt by you of + the Software and shall continue until terminated. The License will + terminate immediately without notice by the Provider if you fail to + comply with the terms and conditions of this Agreement. Upon + termination of this License, you shall immediately discontinue all + use of the Software provided hereunder, and return to the Provider + or destroy the original and all copies of all such Software. All of + your obligations under this Agreement shall survive the termination + of the License. + . + 8. Warranty: THE PROVIDER MAKES NO REPRESENTATIONS ABOUT THE + SUITABILITY, USE, OR PERFORMANCE OF THIS SOFTWARE OR ABOUT ANY + CONTENT OR INFORMATION MADE ACCESSIBLE BY THE SOFTWARE, FOR ANY + PURPOSE. THE SOFTWARE IS PROVIDED "AS IS," WITHOUT EXPRESS OR + IMPLIED WARRANTIES INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED + WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR + NONINFRINGEMENT WITH RESPECT TO THE SOFTWARE. THE PROVIDER IS NOT + OBLIGATED TO SUPPORT OR ISSUE UPDATES TO THE SOFTWARE. + . + 9. Limitation on Liability: This Software is provided free of charge + and, accordingly, the Provider shall not be liable under any theory + for any damages suffered by you or any user of the Software. UNDER + NO CIRCUMSTANCES SHALL PROVIDER BE LIABLE TO YOU OR ANY OTHER + PERSON FOR ANY DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR + CONSEQUENTIAL DAMAGES OF ANY CHARACTER INCLUDING, WITHOUT + LIMITATION, DAMAGES FOR LOSS OF GOODWILL, WORK STOPPAGE, COMPUTER + FAILURE OR MALFUNCTION, OR ANY AND ALL OTHER ECONOMIC LOSS OR + COMMERCIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS + SOFTWARE, EVEN IF PROVIDER SHALL HAVE BEEN INFORMED OF THE + POSSIBILITY OF SUCH DAMAGES, OR FOR ANY THIRD-PARTY CLAIMS. + . + 10. Disputes: The Parties agree to attempt to settle amicably any + controversy or claim arising under this Agreement or a breach of + this Agreement. Thereafter, both parties agree that all disputes + between them arising out of or relating to this Agreement, shall + be submitted to non-binding mediation unless the parties mutually + agree otherwise. All parties agree to exercise their best effort + in good faith to resolve all disputes in mediation. This Agreement + shall be governed and construed in accordance with the laws of + France. + . + 11. Entire Agreement: This Agreement contains the entire agreement + between the parties with respect to the subject matter hereof, and + it shall not be modified or amended except by an instrument in + writing signed by both parties hereto. + +License: LGPL-3+ + This library is free software; you can redistribute it and/or modify it under + the terms of the GNU Lesser General Public License as published by the Free + Software Foundation; either version 3 of the License, or (at your option) any + later version. + . + This library is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the COPYING file for more details. + . + You should have received a copy of the GNU Lesser General Public License along + with this program. If not, see <http://www.gnu.org/licenses/>. + . + On Debian systems, the complete text of the GNU Lesser General Public License + version 3 can be found in "/usr/share/common-licenses/LGPL-3". diff --git a/debian/gbp.conf b/debian/gbp.conf new file mode 100644 index 0000000..cec628c --- /dev/null +++ b/debian/gbp.conf @@ -0,0 +1,2 @@ +[DEFAULT] +pristine-tar = True diff --git a/debian/rules b/debian/rules new file mode 100755 index 0000000..151b7e9 --- /dev/null +++ b/debian/rules @@ -0,0 +1,12 @@ +#!/usr/bin/make -f +# -*- makefile -*- + +# Avoid overlinking and reduce library dependencies. +export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed + +%: + dh $@ --parallel + +.PHONY: override_dh_builddeb +override_dh_builddeb: + dh_builddeb -- -Zxz -z9 diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 0000000..163aaf8 --- /dev/null +++ b/debian/source/format @@ -0,0 +1 @@ +3.0 (quilt) diff --git a/debian/watch b/debian/watch new file mode 100644 index 0000000..44996f5 --- /dev/null +++ b/debian/watch @@ -0,0 +1,2 @@ +version=3 +http://compcert.inria.fr/download.html release/compcert-([\d\.]*).tgz
\ No newline at end of file |