diff options
110 files changed, 2027 insertions, 4 deletions
@@ -0,0 +1,509 @@ +All files in this distribution are part of the Compcert verified compiler. + +The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008 +Institut National de Recherche en Informatique et en Automatique (INRIA). + +The Compcert verified compiler is distributed under the terms of the +INRIA Non-Commercial License Agreement given below. This is a +non-free license that grants you the right to use the Compcert verified +compiler for educational, research or evaluation purposes only, but +prohibits commercial uses. + +The following files in this distribution are dual-licensed both under +the INRIA Non-Commercial License Agreement and under the Free Software +Foundation GNU General Public License, either version 2 or (at your +option) any later version: + + backend/Cminor.v common/Globalenvs.v + caml/CMlexer.mli common/Mem.v + caml/CMlexer.mll common/Smallstep.v + caml/CMparser.mly common/Switch.v + caml/CMtypecheck.ml common/Values.v + caml/CMtypecheck.mli lib/Coqlib.v + caml/Cil2Csyntax.ml lib/Floats.v + caml/PrintCsyntax.ml lib/Integers.v + cfrontend/Csem.v lib/Maps.v + cfrontend/Csyntax.v lib/Parmov.v + common/AST.v runtime/calloc.c + common/Errors.v runtime/stdio.c + common/Events.v runtime/stdio.h + +A copy of the GNU General Public License version 2 is included below. + +The choice between the two licenses for the files listed above is left +to the user. If you opt for the GNU General Public License, these +files are free software and can be used both in commercial and +non-commercial contexts, subject to the terms of the GNU General +Public License. + +This distribution includes a copy of the CIL library and modifications +to this library in the form of patches. The CIL library is Copyright +2001-2005 George C. Necula, Scott McPeak, Wes Weimer and Ben Liblit. +The modifications contained in the sub-directory cil.patches/ of this +distribution are Copyright Institut National de Recherche en +Informatique et en Automatique. The CIL library and the +modifications contained in the sub-directory cil.patches/ are +distributed under the terms of the BSD license, included below. + +---------------------------------------------------------------------- + +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. + +---------------------------------------------------------------------- + + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc., + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Lesser General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +this service if you wish), that you receive source code or can get it +if you want it, that you can change the software or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +convey the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + <one line to give the program's name and a brief idea of what it does.> + Copyright (C) <year> <name of author> + + 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. + +Also add information on how to contact you by electronic and paper mail. + +If the program is interactive, make it output a short notice like this +when it starts in an interactive mode: + + Gnomovision version 69, Copyright (C) year name of author + Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, the commands you use may +be called something other than `show w' and `show c'; they could even be +mouse-clicks or menu items--whatever suits your program. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a "copyright disclaimer" for the program, if +necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the program + `Gnomovision' (which makes passes at compilers) written by James Hacker. + + <signature of Ty Coon>, 1 April 1989 + Ty Coon, President of Vice + +This General Public License does not permit incorporating your program into +proprietary programs. If your program is a subroutine library, you may +consider it more useful to permit linking proprietary applications with the +library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. + +---------------------------------------------------------------------- + + BSD License for the CIL library + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, +this list of conditions and the following disclaimer. + +2. 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. + +3. The names of the contributors may not 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. @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# Xavier Leroy, INRIA Paris-Rocquencourt # +# # +# Copyright Institut National de Recherche en Informatique et en # +# Automatique. All rights reserved. This file is distributed # +# under the terms of the INRIA Non-Commercial License Agreement. # +# # +####################################################################### + include Makefile.config COQC=coqc $(INCLUDES) @@ -0,0 +1,144 @@ + The Compcert verified compiler + +OVERVIEW: + +The Compcert verified compiler is a compiler for a large subset of the +C programming language that generates code for the PowerPC processor. +The distinguishing feature of Compcert is that it has been formally +verified using the Coq proof assistant: the generated assembly code is +formally guaranteed to behave as prescribed by the semantics of the +source C code. + +Compcert is an ongoing research project. The present release is an +advanced prototype intended for research, educational and evaluation +purposes. + + +COPYRIGHT: + +The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008 +Institut National de Recherche en Informatique et en Automatique (INRIA). +It is distributed under the conditions stated in file LICENSE. + + +PREREQUISITES: + +* A computer running the MacOS 10.4 or 10.5 operating system. + Both PowerPC-based and Intel-based Macs are supported. + The PowerPC code generated by the Compcert compiler runs + natively at full speed on PowerPC-based Macs, and runs under + software emulation at reduced speed on Intel-based Macs. + At least 1 Gb of RAM is required to build Compcert from sources. + +* The XCode development tools, as found on the installation DVDs + for MacOS 10. Before proceeding, check that the "gcc", "as" and + "make" tools are installed and accessible in the search path. + +* The Coq proof assistant, version 8.1pl3 or 8.1pl2 or 8.1. + (8.1pl1 does not work.) Coq is free software, available from + http://coq.inria.fr/ + +* The Caml functional language, version 3.09 or 3.10. + Caml is free software, available from http://caml.inria.fr/ + + +INSTALLATION: + +1- Configure the system. From the top directory, do: + + ./configure + +This generates the Makefile.config file in the top directory +and prepares and configures the CIL library in the cil/ subdirectory. + +The "configure" script accepts the following options: + +-bindir <dir> (default: /usr/local/bin) + Directory where the binaries will be installed + +-libdir <dir> (default: /usr/local/lib/compcert) + Directory where the Compcert support library will be installed + +-prefix <dir> (default: /usr/local) + Set bindir and libdir to + <dir>/bin and <dir>/lib/compcert, respectively. + +2- Build the system. From the top directory, do + + make all + +This re-checks all the Coq proofs, then extracts Caml code from the +Coq specification and combines it with the CIL library and supporting +hand-written Caml code to generate the executable for Compcert. This +step takes 10 to 15 minutes on a recent Mac computer; be patient. + +3- You can now install Compcert. This will create the "ccomp" command +in the binary directory selected during configuration, and install +supporting .h and .a files in the library directory. Become superuser +if necessary and do + + make install + + +USAGE: + +The executable for Compcert is called "ccomp". It has the standard +command-line interface for a Unix C compiler. For instance, to +compile the single-file program "src.c" and create an executable +called "exec", just do + + ccomp -o exec src.c + +To compile a two-file program "src1.c" and "src2.c", do + + ccomp -c src1.c + ccomp -c src2.c + ccomp -o exec src1.o src2.o + +To see the generated assembly code for "src1.c", do + + ccomp -S src1.c + +The generated assembly code is left in file src1.s + +The subset of the C language accepted by Compcert is quite large. +The main features of C that are not supported are: + - The "long long" and "long double" types. + - The "goto" statement, and non-structured forms of the "switch" statement. + - Variable-argument functions. +The "ccomp" command will issue errors and diagnostics if it encounters +a C construct that it cannot process. + +The "ccomp" command recognizes the following classes of input files: + .c C source file + .cm Cminor source file + .o Object code file + .a Library file + +The "ccomp" command recognizes the following options: + +Processing options: + -E Preprocess only, save result in <file>.i + -S Compile to assembler only, save result in <file>.s + -c Compile to object file only (no linking), result in <file>.o +Preprocessing options: + -I<dir> Add <dir> to search path for #include files + -D<symb>=<val> Define preprocessor symbol + -U<symb> Undefine preprocessor symbol +Compilation options: + -flonglong Treat 'long long' as 'long' and 'long double' as 'double' + -dclight Save generated Clight in <file>.light.c + -dasm Save generated assembly in <file>.s +Linking options: + -l<lib> Link library <lib> + -L<dir> Add <dir> to search path for libraries + -o <file> Generate executable in <file> (default: a.out) +General options: + -stdlib <dir> Set the path of the Compcert run-time library + -v Print external commands before invoking them + + +CONTACT: + +The authors can be contacted by e-mail at compcert@yquem.inria.fr + diff --git a/backend/Allocation.v b/backend/Allocation.v index eab5233..3a5960b 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Register allocation. *) Require Import Coqlib. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1b5a415..68d6868 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for the [Allocation] pass (translation from RTL to LTL). *) diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index c0abf0d..469fd3c 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Preservation of typing during register allocation. *) Require Import Coqlib. diff --git a/backend/Bounds.v b/backend/Bounds.v index a0f09ce..0e8b9fa 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Computation of resource bounds forr Linear code. *) Require Import Coqlib. diff --git a/backend/CSE.v b/backend/CSE.v index a7901d6..b7e19c1 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Common subexpression elimination over RTL. This optimization proceeds by value numbering over extended basic blocks. *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index d46a39f..a87cd75 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for common subexpression elimination. *) Require Import Coqlib. diff --git a/backend/Cminor.v b/backend/Cminor.v index 1d2eea7..df541a1 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for the Cminor language. *) Require Import Coqlib. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 859c46e..3578868 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The Cminor language after instruction selection. *) Require Import Coqlib. diff --git a/backend/Coloring.v b/backend/Coloring.v index 57f7d59..5e91b03 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Construction and coloring of the interference graph. *) Require Import Coqlib. diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index ce24030..cea4ce5 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness of graph coloring. *) Require Import SetoidList. diff --git a/backend/Constprop.v b/backend/Constprop.v index fecfb19..18fa589 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Constant propagation over RTL. This is the first of the two optimizations performed at RTL level. It proceeds by a standard dataflow analysis and the corresponding code transformation. *) diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dfa828b..e16f322 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for constant propagation. *) Require Import Coqlib. diff --git a/backend/Conventions.v b/backend/Conventions.v index 9d005b3..ea7d448 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Function calling conventions and other conventions regarding the use of machine registers and stack slots. *) diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 5dc4fe9..c9891c2 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Representation of interference graphs for register allocation. *) Require Import Coqlib. diff --git a/backend/Kildall.v b/backend/Kildall.v index 41011f2..b4445ae 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Solvers for dataflow inequations. *) Require Import Coqlib. diff --git a/backend/LTL.v b/backend/LTL.v index db996ba..e99e016 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The LTL intermediate language: abstract syntax and semantics. LTL (``Location Transfer Language'') is the target language diff --git a/backend/LTLin.v b/backend/LTLin.v index da8719a..6cf2eb5 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The LTLin intermediate language: abstract syntax and semantcs *) (** The LTLin language is a variant of LTL where control-flow is not diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 06c50f8..1c0c3f3 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Typing rules for LTLin. *) Require Import Coqlib. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 646edc8..18308b8 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Typing rules for LTL. *) Require Import Coqlib. diff --git a/backend/Linear.v b/backend/Linear.v index a6e31fb..b9880ff 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The Linear intermediate language: abstract syntax and semantcs *) (** The Linear language is a variant of LTLin where arithmetic diff --git a/backend/Linearize.v b/backend/Linearize.v index 57919b8..42330ed 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Linearization of the control-flow graph: translation from LTL to LTLin *) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index a625ba7..12d0a1f 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for code linearization *) Require Import Coqlib. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 473b342..ba54723 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Type preservation for the Linearize pass *) Require Import Coqlib. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index baf522a..0f5a1ec 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Typing rules for Linear. *) Require Import Coqlib. diff --git a/backend/Locations.v b/backend/Locations.v index aaefc08..1373887 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Locations are a refinement of RTL pseudo-registers, used to reflect the results of register allocation (file [Allocation]). *) diff --git a/backend/Mach.v b/backend/Mach.v index 05805ec..f727504 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract syntax. Mach is the last intermediate language before generation of assembly diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 0abdd1e..32a316a 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract semantics. *) Require Import Coqlib. diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 5349fb5..ffdfb33 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Simulation between the two semantics for the Mach language. *) Require Import Coqlib. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5a095d7..2eb3d47 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: concrete semantics. *) Require Import Coqlib. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 28037ce..5e5f03c 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Type system for the Mach intermediate language. *) Require Import Coqlib. diff --git a/backend/Op.v b/backend/Op.v index 698b433..51b5e53 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Operators and addressing modes. The abstract syntax and dynamic semantics for the CminorSel, RTL, LTL and Mach languages depend on the following types, defined in this library: diff --git a/backend/PPC.v b/backend/PPC.v index 244c595..8af2c9b 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for PowerPC assembly language *) Require Import Coqlib. diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 171945d..805d039 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from Mach to PPC. *) Require Import Coqlib. diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 8d6d934..2b00cfc 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for PPC generation: main proof. *) Require Import Coqlib. diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index c0125fc..107ea05 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for PPC generation: auxiliary results. *) Require Import Coqlib. diff --git a/backend/PPCgenretaddr.v b/backend/PPCgenretaddr.v index f2802ec..3526865 100644 --- a/backend/PPCgenretaddr.v +++ b/backend/PPCgenretaddr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Predictor for return addresses in generated PPC code. The [return_address_offset] predicate defined here is used in the diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index 3d77b57..baab207 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation of parallel moves into sequences of individual moves. In this file, we adapt the generic "parallel move" algorithm diff --git a/backend/RTL.v b/backend/RTL.v index b1afc94..abecd4a 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The RTL intermediate language: abstract syntax and semantics. RTL stands for "Register Transfer Language". This is the first diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v index 0ad6e68..182f593 100644 --- a/backend/RTLbigstep.v +++ b/backend/RTLbigstep.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** An alternate, mixed-step semantics for the RTL intermediate language. *) Require Import Coqlib. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 52a6c8a..3cc0eeb 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from CminorSel to RTL. *) Require Import Coqlib. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index dd8728f..e02463a 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for RTL generation. *) Require Import Coqlib. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 94afff8..b8061a3 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract specification of RTL generation *) (** In this module, we define inductive predicates that specify the diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 4056749..a30f9e5 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Typing rules and a type inference algorithm for RTL. *) Require Import Coqlib. diff --git a/backend/Registers.v b/backend/Registers.v index e4b7b00..c3d04d6 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Pseudo-registers and register states. This library defines the type of pseudo-registers (also known as diff --git a/backend/Reload.v b/backend/Reload.v index 58e17ff..c5559e3 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Reloading, spilling, and explication of calling conventions. *) Require Import Coqlib. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index e9ced51..401ae46 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for the [Reload] pass. *) Require Import Coqlib. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 155c174..3f0ff1e 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Proof of type preservation for Reload and of correctness of computation of stack bounds for Linear. *) diff --git a/backend/Selection.v b/backend/Selection.v index 0183ee7..8a69ade 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Instruction selection *) (** The instruction selection pass recognizes opportunities for using diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 177e321..e28bfaf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness of instruction selection *) Require Import Coqlib. diff --git a/backend/Stacking.v b/backend/Stacking.v index c19e293..16595e5 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Layout of activation records; translation from Linear to Mach. *) Require Import Coqlib. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 905570e..46e19ca 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for the translation from Linear to Mach. *) (** This file proves semantic preservation for the [Stacking] pass. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index fa8a3e2..aa534ff 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Type preservation for the [Stacking] pass. *) Require Import Coqlib. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 15f4676..2f520c6 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Branch tunneling (optimization of branches to branches). *) Require Import Coqlib. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 3777eaa..d0c9546 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for the branch tunneling optimization. *) Require Import Coqlib. diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index c611067..57e1271 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Type preservation for the Tunneling pass *) Require Import Coqlib. diff --git a/caml/CMlexer.mli b/caml/CMlexer.mli index 573c530..c6afb72 100644 --- a/caml/CMlexer.mli +++ b/caml/CMlexer.mli @@ -1,4 +1,17 @@ -(* $Id: CMlexer.mli,v 1.1 2005/01/21 13:11:07 xleroy Exp $ *) +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) val token: Lexing.lexbuf -> CMparser.token exception Error of string diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll index 7951982..ba67a69 100644 --- a/caml/CMlexer.mll +++ b/caml/CMlexer.mll @@ -1,4 +1,17 @@ -(* $Id: CMlexer.mll,v 1.3 2005/03/21 15:53:00 xleroy Exp $ *) +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) { open Camlcoq diff --git a/caml/CMparser.mly b/caml/CMparser.mly index fb09527..e7c656d 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -1,4 +1,17 @@ -/* $Id: CMparser.mly,v 1.2 2005/03/21 15:53:00 xleroy Exp $ */ +/* *********************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Xavier Leroy, INRIA Paris-Rocquencourt */ +/* */ +/* Copyright Institut National de Recherche en Informatique et en */ +/* Automatique. All rights reserved. This file is distributed */ +/* 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 file is also distributed */ +/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* */ +/* *********************************************************************/ %{ open Datatypes diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 9277829..625c36f 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (* A type-checker for Cminor *) open Printf diff --git a/caml/CMtypecheck.mli b/caml/CMtypecheck.mli index 94a1023..44c7654 100644 --- a/caml/CMtypecheck.mli +++ b/caml/CMtypecheck.mli @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + exception Error of string val type_program: Cminor.program -> Cminor.program diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index ec2447f..d60e022 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (* Library of useful Caml <-> Coq conversions *) open Datatypes diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index fd3ad49..554715f 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -1,3 +1,19 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Thomas Moniot, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (************************************************************************** CIL -> CabsCoq translator **************************************************************************) diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml index b3f4515..984fbb3 100644 --- a/caml/Coloringaux.ml +++ b/caml/Coloringaux.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open Camlcoq open Datatypes open BinPos diff --git a/caml/Coloringaux.mli b/caml/Coloringaux.mli index ff4cfea..c5070f2 100644 --- a/caml/Coloringaux.mli +++ b/caml/Coloringaux.mli @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open Registers open Locations open RTL diff --git a/caml/Driver.ml b/caml/Driver.ml index fcd7a57..09c4622 100644 --- a/caml/Driver.ml +++ b/caml/Driver.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open Printf (* Location of the standard library *) diff --git a/caml/Floataux.ml b/caml/Floataux.ml index f61bd5b..0226de2 100644 --- a/caml/Floataux.ml +++ b/caml/Floataux.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open Camlcoq open Integers diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml index a4952a5..02a9524 100644 --- a/caml/Linearizeaux.ml +++ b/caml/Linearizeaux.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open BinPos open Coqlib open Datatypes diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml index 4eff1c6..bc4dea6 100644 --- a/caml/PrintCsyntax.ml +++ b/caml/PrintCsyntax.ml @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Pretty-printer for Csyntax *) open Format diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 97082b9..3d247e1 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -1,4 +1,14 @@ -(* $Id: PrintPPC.ml,v 1.2 2005/01/22 11:28:46 xleroy Exp $ *) +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) (* Printing PPC assembly code in asm syntax *) diff --git a/caml/PrintPPC.mli b/caml/PrintPPC.mli index fbd4004..2ebbb95 100644 --- a/caml/PrintPPC.mli +++ b/caml/PrintPPC.mli @@ -1 +1,13 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + val print_program: out_channel -> PPC.program -> unit diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml index 61abecf..826f988 100644 --- a/caml/RTLgenaux.ml +++ b/caml/RTLgenaux.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + open Switch open CminorSel diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml index 5ed7e6e..6c43227 100644 --- a/caml/RTLtypingaux.ml +++ b/caml/RTLtypingaux.ml @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (* Type inference for RTL *) open Datatypes diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 8596ebf..755aa28 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from Csharpminor to Cminor. *) Require Import FSets. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ff10bb3..a158b13 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for Cminor generation. *) Require Import FSets. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 7617616..35d3cce 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Dynamic semantics for the Clight language *) Require Import Coqlib. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 7afe27f..ce19f68 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for the Csharpminor language. *) Require Import Coqlib. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 4090c55..b3369ae 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from Clight to Csharpminor. *) (** The main transformations performed by this first part are: diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index 9930ef8..87cdb21 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 1: syntactic properties *) Require Import Coqlib. diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 6b7b5e3..f6bef93 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 2: Csharpminor construction functions *) Require Import Coqlib. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 2b2cefb..a25c5b8 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 3: semantic preservation *) Require Import Coqlib. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 00fdaa5..6680efe 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax for the Clight language *) Require Import Coqlib. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 72c4edf..b4dd290 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Typing constraints on C programs *) Require Import Coqlib. diff --git a/common/AST.v b/common/AST.v index 403861d..eab1adf 100644 --- a/common/AST.v +++ b/common/AST.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** This file defines a number of data types and operations used in the abstract syntax trees of many of the intermediate languages. *) diff --git a/common/Complements.v b/common/Complements.v index 2263f4e..6df488f 100644 --- a/common/Complements.v +++ b/common/Complements.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Corollaries of the main semantic preservation theorem. *) Require Import Classical. diff --git a/common/Errors.v b/common/Errors.v index 2c1d752..2c9bbc3 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Error reporting and the error monad. *) Require Import String. diff --git a/common/Events.v b/common/Events.v index e9070e1..c44da01 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Representation of observable events and execution traces. *) Require Import Coqlib. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 7ace0cf..f720914 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Global environments are a component of the dynamic semantics of all languages involved in the compiler. A global environment maps symbol names (names of functions and of global variables) diff --git a/common/Main.v b/common/Main.v index bfee3ff..e5f6280 100644 --- a/common/Main.v +++ b/common/Main.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** The whole compiler and its proof of semantic preservation *) (** Libraries. *) diff --git a/common/Mem.v b/common/Mem.v index 6b66d9d..22a8e1f 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1,3 +1,19 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** This file develops the memory model that is used in the dynamic semantics of all the languages used in the compiler. It defines a type [mem] of memory states, the following 4 basic diff --git a/common/Smallstep.v b/common/Smallstep.v index 8039ba4..ec7a416 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Tools for small-step operational semantics *) (** This module defines generic operations and theorems over diff --git a/common/Switch.v b/common/Switch.v index e8b3967..d98ecaa 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Multi-way branches (``[switch]'') and their compilation to 2-way comparison trees. *) diff --git a/common/Values.v b/common/Values.v index e5b4971..80c5c93 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** This module defines the type of values that is used in the dynamic semantics of all our intermediate languages. *) @@ -1,5 +1,17 @@ #!/bin/sh +####################################################################### +# # +# The Compcert verified compiler # +# # +# Xavier Leroy, INRIA Paris-Rocquencourt # +# # +# Copyright Institut National de Recherche en Informatique et en # +# Automatique. All rights reserved. This file is distributed # +# under the terms of the INRIA Non-Commercial License Agreement. # +# # +####################################################################### + cildistrib=cil-1.3.5.tar.gz prefix=/usr/local bindir='$(PREFIX)/bin' diff --git a/extraction/Makefile b/extraction/Makefile index 513577c..5729642 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# Xavier Leroy, INRIA Paris-Rocquencourt # +# # +# Copyright Institut National de Recherche en Informatique et en # +# Automatique. All rights reserved. This file is distributed # +# under the terms of the INRIA Non-Commercial License Agreement. # +# # +####################################################################### + include ../Makefile.config FILES=\ diff --git a/extraction/extraction.v b/extraction/extraction.v index 22df593..fc2920e 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + Require Iteration. Require Floats. Require RTLgen. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 7bee366..c14ed79 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** This file collects a number of definitions and theorems that are used throughout the development. It complements the Coq standard library. *) diff --git a/lib/Floats.v b/lib/Floats.v index f4c5119..f11ead4 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Axiomatization of floating-point numbers. *) (** In contrast with what we do with machine integers, we do not bother diff --git a/lib/Inclusion.v b/lib/Inclusion.v index 15e37c4..728a725 100644 --- a/lib/Inclusion.v +++ b/lib/Inclusion.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Tactics to reason about list inclusion. *) (** This file (contributed by Laurence Rideau) defines a tactic [in_tac] diff --git a/lib/Integers.v b/lib/Integers.v index a3240e8..2d548fb 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *) Require Import Coqlib. diff --git a/lib/Iteration.v b/lib/Iteration.v index 85c5ded..cabe5b8 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (* Bounded and unbounded iterators *) Require Import Coqlib. diff --git a/lib/Lattice.v b/lib/Lattice.v index f796367..3c39006 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Constructions of semi-lattices. *) Require Import Coqlib. @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Applicative finite maps are the main data structure used in this project. A finite map associates data to keys. The two main operations are [set k d m], which returns a map identical to [m] except that [d] diff --git a/lib/Ordered.v b/lib/Ordered.v index ad47314..4b1f4e0 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Constructions of ordered types, for use with the [FSet] functors for finite sets. *) diff --git a/lib/Parmov.v b/lib/Parmov.v index fa31b67..2c7b82a 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1,3 +1,20 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Laurence Rideau, INRIA Sophia-Antipolis-Méditerranée *) +(* Bernard Paul Serpette, INRIA Sophia-Antipolis-Méditerranée *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* 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 file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation of parallel moves into sequences of individual moves *) (** The ``parallel move'' problem, also known as ``parallel assignment'', diff --git a/runtime/calloc.c b/runtime/calloc.c index 2526ceb..8e5e0b6 100644 --- a/runtime/calloc.c +++ b/runtime/calloc.c @@ -1,3 +1,18 @@ +/* *********************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Xavier Leroy, INRIA Paris-Rocquencourt */ +/* */ +/* Copyright Institut National de Recherche en Informatique et en */ +/* Automatique. All rights reserved. This file is distributed */ +/* 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 file is also distributed */ +/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* */ +/* *********************************************************************/ + #include <stdio.h> #include <stddef.h> #include <stdlib.h> diff --git a/runtime/stdio.c b/runtime/stdio.c index c153257..8351e5d 100644 --- a/runtime/stdio.c +++ b/runtime/stdio.c @@ -1,3 +1,18 @@ +/* *********************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Xavier Leroy, INRIA Paris-Rocquencourt */ +/* */ +/* Copyright Institut National de Recherche en Informatique et en */ +/* Automatique. All rights reserved. This file is distributed */ +/* 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 file is also distributed */ +/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* */ +/* *********************************************************************/ + #include <stdarg.h> #include <stdlib.h> #define _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY diff --git a/runtime/stdio.h b/runtime/stdio.h index 2442dcb..75a2326 100644 --- a/runtime/stdio.h +++ b/runtime/stdio.h @@ -1,3 +1,18 @@ +/* *********************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Xavier Leroy, INRIA Paris-Rocquencourt */ +/* */ +/* Copyright Institut National de Recherche en Informatique et en */ +/* Automatique. All rights reserved. This file is distributed */ +/* 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 file is also distributed */ +/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* */ +/* *********************************************************************/ + #ifndef _COMPCERT_STDIO_H #define _COMPCERT_STDIO_H |