diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..dcdf7c77a71052d12c8f78f6ff6974a7827fe41a
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Makefile b/Makefile
index 2a795e438956b7b7f18ffec83c107bd6d75eed81..afadd77840c35838c5c009eb22d723e7dc42b696 100644
--- a/Makefile
+++ b/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
COQC=coqc $(INCLUDES)
diff --git a/README b/README
new file mode 100644
index 0000000000000000000000000000000000000000..9cfad16dd994345e620648bd3cd1008a4585510e
--- /dev/null
+++ b/README
@@ -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 eab5233da19aa6154a94dcbf13bfc31b537003e8..3a5960be7d3c493973874cece0f7065374b680f3 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 1b5a41563055e6168c02b39cf3826d2daa7e9b1a..68d6868c2a5364d4b5ff112404637667581f6ff0 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 c0abf0d6d3319f04926ada588f450f6954c766b1..469fd3c3996fb8bd4ab2bc17f59c219b173dbf87 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 a0f09ce8a407800f67281de49fa6e5bca20a660d..0e8b9faf5a4dfd999b789d72d5bddaa6e3ac64ae 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 a7901d6166b5a6c566ccc918f712582568e264d6..b7e19c1bcaffd01bdb416284768d61e15f996da2 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 d46a39f123b1de88c3b7d6936ab2a91cf82cf84f..a87cd7586f8b843da353eaa1db0e14dab3a2e30c 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 1d2eea74de3e18a9459e3fa9593884f553ec1fcb..df541a11701eb4110d4f0a8f146d0d809d7712c6 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 859c46e7585e2524dfd244d22a0acf99343e7c77..357886853264d99e518c5bc4c25e6e74d57290dc 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 57f7d5946731b12903b291fa8ac516889095d1ad..5e91b03c0535fa136a545ddc37cd081db4c21a5b 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 ce24030de71e05079277d5993696ee78260d12db..cea4ce5fd583583e14da2b07db7643481dae929f 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 fecfb19fc978cdd71cb814c7e720a69ff30a45f1..18fa589ff6d4ba34c0f3de36062d839b0dc6ce4d 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 dfa828bfe7bfda0f10002afe71d3706df1d88f29..e16f322ec7b06388e7adde3b77df065fafeb0ef6 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 9d005b3475507ac08787687562257c3d1b9b9dca..ea7d448e2b7bbf24ac9178d67a2b3006e6e4d709 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 5dc4fe9ed23aa0252bec1e73d409cffa6e006765..c9891c273525a819043d36544ca1a7e69fe4fd90 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 41011f2b14411784768f9d5dee62e0a3cd039baa..b4445aebd0948131e687d586189d651db2cc26aa 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 db996ba4b0503a6ba44c0f7f4d476a59cb818f8a..e99e016e887b424a301b3db4e185ec9a42896da0 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 da8719ac9ec75a8cc18407ad08cde817cdcd8650..6cf2eb5386354cc5d8f5c8b602731f780ee54c71 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 06c50f8be66d268add5b373745a229a8043374a4..1c0c3f30a742bc30f7acede693dd2450a4950279 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 646edc827fb1a16e6ce2fee980fac0ce3950c39d..18308b8fd3beebf7232d3ea0973814f799bdc478 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 a6e31fb60de2c94d0eff5bddac97c0e6cff861c0..b9880ff1119779e0127d122750e197d86282ff28 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 57919b87a296a4c82ef22c0268b8de5eb48065fa..42330ed9e09ea8e5b65c6aac99424c3f710d2284 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 a625ba7577ba5e1a4526d3d96101f6126164ce92..12d0a1f3f3b7c5b01c0cf24539bbedfd1e73e93b 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 473b3421b1645b74bc3f7aa702d84612854bed4f..ba5472308010150f4e488c21a78f0504b05b7b06 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 baf522aad2989016d7f110c270162175043c7659..0f5a1ec99f0b4a0ee61ae7cfc18f0319323b3b3b 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 aaefc08c50fc743f0ecb68a84aaa473bcec474db..1373887f18678f1e72a9a71d9c7a1494e80a8340 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 05805ec5fee14264331aed5a504dfdf4d6548537..f7275041307abcfd0efea693b1970b90fcffad0e 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 0abdd1e1c8d9ccc76a95f1cdb2b1ed2df0f13dad..32a316ae6cb1a244d534395913081d7dab44173c 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 5349fb500504cba64fd15f64a8cdba7589621cef..ffdfb3362a63efe2279360c48d089ee6ee30d18c 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 5a095d798a468966117d6e7444d096065c290e3b..2eb3d47838357b5fbc761d5d035533b7a1d1246d 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 28037cec5ea6d4b6bf3b97a06f9e40908ae74b7c..5e5f03c4c385dd833aef035660dadf7fc38c11b6 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 698b433c044c5c87ef433aa8379d3189a38b0cad..51b5e53057b6a5f73a631853a8c373125e005a9c 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 244c595168ed272f865d792640342001820a198d..8af2c9be253d187cd9db0e3e1a930e57e732c0ce 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 171945dea2c04aaa5068594c52c8084b7b1af9c4..805d039b707f03653967f17b27915a292e9de272 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 8d6d9342b6baf36a5777f90bb470311ab83e117e..2b00cfc0387d95fa240b65cee0459c7a7cf0868f 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 c0125fc2417cdf9bae8727c8d4050f10729cc5de..107ea05316bf9ade6774cf6c68ffd207ae128d79 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 f2802ecd9635966223a5f1ad2d43045ad0a01f39..3526865e324c3e3c9b00175fa5c662ccc328f26a 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 3d77b57ae8aac9d46d2b0f4543dd5104a97ffb55..baab2071133f8551c6967039609e0b29da00f7d7 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 b1afc94acd9043dc37acccdd7c1167811817fe2b..abecd4a7f85c9682cbc4f93cda1b47cb384da7cd 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 0ad6e68a12fb9c9acb7b8c9bc3062cdc60bad4ce..182f5935c74ba54e95a520b030e59d47ae7327c6 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 52a6c8aea23b49dab26f96c542d756cd229d73bf..3cc0eebf8567531f7b48bb5c8b829f4558e304fd 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 dd8728fda3e4a9094363b9365d23eb5bc6919078..e02463a2e5aa98b64b4a99b38c15bb023943bc17 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 94afff85f13915b07eeaf42035bbbcc54ac6634d..b8061a3f91ceccf7842d2009b2a0d46f6351d9a6 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 40567491e6912ca9bdc91956cc83ca23f8355752..a30f9e50a85aff2afcdf71021a4499042994bb9d 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 e4b7b000b5f53811fe5e6bb3fd73cecfbd667dab..c3d04d60234b48ae3b008a250ddd7d9ae4b034f1 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 58e17ff52253595d51988a9e87377dde30a98604..c5559e3588528949bb58a5fe08c12509e544f76a 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 e9ced51f9acb1153cb030b8893ff1a6ac30827ba..401ae4660dbe92dbbd0435330445408618f1030c 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 155c174d57851c90eca53cb2562a4c66091e5b46..3f0ff1ee39824e929ba88457650dd144413e39a9 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 0183ee7d9fa8fe3e27d727ba9b271f4b820235fd..8a69adecd27325ad1678c19c85321902a9c41ab9 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 177e32118253aa420c7f730b5ade321f90dba40d..e28bfaf387d3b0e818a58f7acc69dcb8d1632d0b 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 c19e293f5113a5a0dca48379d58a71926de56424..16595e543e41f55afe55b68a20721679f00938b0 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 905570ef86fc050498fa15b40bc0475cc7fd38d9..46e19ca905a636048d6dccb99c1f670534e5b10b 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 fa8a3e2eaf786da43e666448446010fc96716858..aa534ff05d9cb81cbdc8f87647a55090c6641476 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 15f4676d7df3edb98c65fbd85204a9fee5a5cf41..2f520c61b5a91f43aed72bec0eea93593b0ff886 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 3777eaa9d42ba4dba761f0adec180ecf216b056b..d0c954622d7396546d3db78ed673537a56a88007 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 c611067cd0af7cd7e22463ca962a0dad35207936..57e1271d1c9fd0bf95efb18bf21759ba1a68be66 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 573c530510792bb866889787cfa7904309174d76..c6afb72c820c9b9a29c9d1a0eedf32b98307e0ba 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 7951982f25fd7933e1d95ec920255a810ec281a9..ba67a6991783fa130ab7cc23c8aa1050a2b683b1 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 fb095275aa163da88ee0fca33a2271423d1bddb0..e7c656d69be76345febd3fb2287f4755a5903e33 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 9277829c4cb4c07f119ffbc2e18fe0873ed7b3de..625c36fc8602b0525807e68defe6c8989bf4ad5e 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 94a1023ad6f3dc646e852228e93baf15a1e2e773..44c76544ad224811b7040244a22f0caf46574ddd 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 ec2447fa2fd5acdf5e681b707a593cf437216833..d60e022224cd7a3f9f8e7d0789f18795101adcc4 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 fd3ad4969b55f5670244a7243c4c6e1286ec4863..554715fc0b6fea6a640c47c2481f56d73713960b 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 b3f4515e91b7b80344fc613a0141a3835068492f..984fbb3460cb7d312a3973b75d88b1ec44da56f8 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 ff4cfeaaa23cfbebfb0af9d4daf33eb47a303d8a..c5070f202325956535eaad3be191b5403eef2864 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 fcd7a57bf74710c05115f5611e008c3052208b1e..09c4622a49d21aee2d8ee1f18c3c4f0dc3eaa6be 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 f61bd5b50a5dc82c11d634a84b1a2675cdc57070..0226de27bbfee2926b155cd63cebbd282d4b3157 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 a4952a5ecb6ba0e0fa5dde5c47870e11279871eb..02a9524185927d12e2dde9ef9e78e276c218b909 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 4eff1c68684a1d3eca35112fc984f9be27b394f9..bc4dea65507fe2f31aa8dace4928261d3701798d 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 97082b9b6db011b6969db18c09986b449345cb1f..3d247e10c04954d58bcbc2276d5dc5b34a28d4aa 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 fbd40045e6d6e660daa02be3e17c89bfa908302f..2ebbb9556506476798c7f05bdf5e3363f901f469 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 61abecfa06f36ceeb3a5840972a9a67a26a3bf87..826f98878bad10aa483b4d17a4606c0e7865eab4 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 5ed7e6e25da92b6d0f2515ab4edbe7342a8868cd..6c43227b1d4bb356f110dc926e9f38bbd91388aa 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 8596ebfa8dbf5ac306366fcf1916799daa0fcbaa..755aa28c833f3b05248554133d2b4aaa14401ff5 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 ff10bb3ee11d818ff8fd2c47428682055df166e9..a158b133c1fe152008becd288f5932292578ca9f 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 761761631b51b817d05b5ed9df1bbb5610024cc5..35d3cce77c7f913c4f2e97f76d1b252c56a8683e 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 7afe27f2f203a1d21150db4395713ec61877e710..ce19f6878ac988977d13f4e2e95f880918f2d16e 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 4090c55a187ae4dea9152605eba1e67c027c6bdc..b3369ae2c1600edbbd9e88bc8565d240d3d9ba49 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 9930ef808dc95cbd54fba4302ae4c1f3cea16a94..87cdb21d33a5688cfa18ff831d1cabd14559123e 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 6b7b5e3c7a8e447586911cd9fcd1f86743c24114..f6bef93e47a4ec362bb2fd0f519b3609f010dd61 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 2b2cefbc79a73166ad4fc77ed546bb5c3887e45d..a25c5b8bffcceec0596c1b820bd4613c3eb17dba 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 00fdaa55ffeac00cf5ea596fa19e458962be4a80..6680efe2cd08baa69dcfb4e777b8441360675870 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 72c4edf2b61ad457feda408e4268da8fe23d2169..b4dd290469b72fe6bba420d5c67a8d60235b1c37 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 403861deba6635f961f6f8b9874e4f8df7d51176..eab1adf170365f804943e89fd97e9b1009f4ac68 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 2263f4ece81b640c13cbd122dfa038be489225d4..6df488fc75d72761f68fc18ffdb246109e2f26e0 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 2c1d752aecb8c38fbabf5f6c82c1baa4b089d023..2c9bbc3fb7f1a2bc2c1c0f0cb95e898de701fc3e 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 e9070e169d0698309b00f489f4098f8bac2fbfbf..c44da0138b84c24fe4bfff0e14ed98960662bfb4 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 7ace0cf1b7fe4d1b06c67198f6eb3ca045801299..f7209141db38e0fcea508e66b5832f84db7fdbb3 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 bfee3ff35e19918e8f6ee614264c16c377e8c356..e5f6280ca16b8166f839c01e703567534692ff3b 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 6b66d9da5225bd79d164859d1f2e9918fbdc5879..22a8e1f0dad77a18ad127dc9186747b19a7a7da2 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 8039ba43a293373324abf14786416b0bad278b5d..ec7a416d31ff63126c3e5943a9c6cdfb45fd933a 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 e8b396719665cf43ff2ff571df35233acea2cbc4..d98ecaa08625d301aac49d608d4739354c8f1eb3 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 e5b497114b728438806067c54cedd30ac82fa061..80c5c93e65263e00ca4fa87e5614baaeb12ebe15 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. *)
diff --git a/configure b/configure
index 2f4edf34b6ad036cdbe4a18909b7340dc5d0286f..7214a311025869413b8a7345ef04252aed9ac186 100755
--- a/configure
+++ b/configure
@@ -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 513577c0bea8dd152edfd9e8e853e4c0a78e7d2e..5729642c27864a2ab5186281fa61a6661e4b1374 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 22df5933706d952dd17ecf58f6d18ceca7f43c2c..fc2920efbda7585f3f8f16fc1bcc6facfabbc7c8 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 7bee366b12c48f343bc8eabc64bbd3d37fdace11..c14ed790f30241a045a8cc6c648c4c8d6582cb0e 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 f4c5119e4114e8f343807a97956ef7a7603846d6..f11ead4a0ed373c665875be2fbd607e074bee466 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 15e37c460d126fec8b818f8b3c140e6923759e74..728a7252b3be9a68711cf48530671e69ecfdd308 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 a3240e8184975d69b2cfda3d037a883b0564d72e..2d548fb66ed50f10f6c5ca931e37d74da9ef8ac7 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 85c5ded8dec61d9860a62c8013b5149692017426..cabe5b82570a81333061807103706f73631fa767 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 f796367dcaace1b6f79e5247ef6914bd2e166f7a..3c390069e12a726939648157b30e6333cafe87c0 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.
diff --git a/lib/Maps.v b/lib/Maps.v
index 238009b2e4c155812c38ee2e63f2d71b8222c2bb..4a346c6cf64708397a02207ce9f35ba7cfd36159 100644
--- a/lib/Maps.v
+++ b/lib/Maps.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. *)
+(* *)
+(* *********************************************************************)
+
(** 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 ad47314a661d5e5c46d1f99b8419969ca0f0ccab..4b1f4e0fec64e6a67bfa75d5c36844207dd10ad3 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 fa31b673e69da3c6659fb03d8215203a3d0bf19b..2c7b82a7b2a95bc99d57d1dd4e076c0376fb2538 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 2526cebf5cec61c2c204c54fd5a77e97a6e22afb..8e5e0b6d6b19f76231b9c3dda4b252f1af7072f8 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 c1532572c6f4545e88a8d5ba2b0b8eaf07952cf7..8351e5d95a2b380c52142c693c4cdb5662a06a17 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 2442dcb15cb57ec9f51631a5c6e4811a64eb121e..75a23266a472d0c0dbfc0177f32a01b5f7250d7c 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