From ec0f5c6fa4d021be9b86ac6c18b4296c977fb323 Mon Sep 17 00:00:00 2001 From: "Andrew W. Appel" Date: Fri, 29 Apr 2022 10:38:27 -0400 Subject: [PATCH] Clean up licensing and configure/install scripts 1. The LICENSE file referred to VCFloat's dependencies on several external library, some of which it no longer depends on. Deleted references to those. 2. Clarified dependencies on CompCert (which needed clarification because some parts of CompCert are not open-source). 3. Deleted many obsolete build/configure/patch scripts. Those are no longer needed, because we can access all needed libraries through the Coq Platform. 4. Cleaned up and simplified LICENSE, while still adhering to the terms of the original license for the current components of VCFloat. --- ACKS | 1187 +--------------------------------------- LICENSE | 28 +- cecill-c-1.0.txt | 517 ----------------- clean_external_libs.sh | 51 -- configure | 160 ------ get_external_libs.sh | 167 ------ patches/compcert.patch | 509 ----------------- patches/interval.patch | 97 ---- 8 files changed, 24 insertions(+), 2692 deletions(-) delete mode 100644 cecill-c-1.0.txt delete mode 100755 clean_external_libs.sh delete mode 100755 configure delete mode 100755 get_external_libs.sh delete mode 100644 patches/compcert.patch delete mode 100644 patches/interval.patch diff --git a/ACKS b/ACKS index b74816c..d39735e 100644 --- a/ACKS +++ b/ACKS @@ -1,1191 +1,32 @@ -VCFloat depends on the following external libraries, which VCFloat's -building system automatically downloads from their official sources -(see README for more information): - -- R-CoqLib, a general-purpose tactic and theorem library for Coq. - - Copyright (C) 2015 Reservoir Labs Inc. All rights reserved. - - R-CoqLib is distributed under the GNU General Public License, - version 3.0 (GNU GPL v3) or (at your option) any later version. A - verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt +VCFloat depends on the following external libraries, +which are normally supplied by the Coq Platform installation +(either by opam or by other means): - The CompCert C verified compiler. - Copyright (C) 2004-2015 INRIA. All rights reserved. - - CompCert is distributed under the INRIA Non-Commercial license - (reproduced verbatim in extenso below). Some of its files, including - all files used by VCFloat, are dual-licensed under the INRIA - Non-Commercial license and the GNU General Public License, version - 2.0 (reproduced verbatim in extenso below) or (at your option) any - later version. - -- Ssreflect, the Small-Scale reflection library. + Copyright (C) 2004-2022 INRIA. - Copyright (C) 2008-2015 The Mathematical Components Team at the - INRIA-Microsoft Research Joint Center (Andrea Asperti, Jeremy - Avigad, Yves Bertot, Cyril Cohen, Francois Garillot, Georges - Gonthier, Stephane Le Roux, Assia Mahboubi, Sidi Ould Biha, Ioana - Pasca, Laurence Rideau, Enrico Tassi, Laurent Thery and Russell - O'Connor). All rights reserved. + VCFloat can be built and used with or without CompCert. + Some components of VCFloat (and some applications of VCFloat) need + CompCert, other components (and applications) do not. - Ssreflect is distributed under the CeCILL-B license (reproduced - verbatim in extenso below). - -- MathComp, the Mathematical Components library. - - Copyright (C) 2008-2015 The Mathematical Components Team at the - INRIA-Microsoft Research Joint Center (Andrea Asperti, Jeremy - Avigad, Yves Bertot, Cyril Cohen, Francois Garillot, Georges - Gonthier, Stephane Le Roux, Assia Mahboubi, Sidi Ould Biha, Ioana - Pasca, Laurence Rideau, Enrico Tassi, Laurent Thery and Russell - O'Connor). All rights reserved. - - MathComp is distributed under the CeCILL-B license (reproduced - verbatim in extenso below). + Those parts of VCFloat that depend on CompCert, require only + CompCert's dual-licensed components: that is, the portion of CompCert + that is licensed by either/both the (open-source) GNU Lesser Public License + and the (not open-source) INRIA License. See the CompCert + distribution for explanations of licenses. - Flocq, a Floating-Point Library for Coq. - Copyright (C) 2010-2015 Sylvie Boldo and Guillaume Melquiond. All - rights reserved. + Copyright (C) 2010-2022 Sylvie Boldo and Guillaume Melquiond. Flocq is distributed under the GNU Lesser General Public License, (GNU LGPL) version 3.0 (reproduced verbatim in extenso below). - Coq-Interval, an Interval Package for Coq. - Copyright (C) 2007-2015 Guillaume Melquiond. All rights reserved. + Copyright (C) 2007-2022 Guillaume Melquiond. Coq-Interval is distributed under the CeCILL-C free software license (reproduced verbatim in cecill-c.txt). - -BEGIN INRIA Non-Commercial License (for CompCert) - -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. - -END INRIA Non-Commercial - - -BEGIN GNU GPL 2.0 (for CompCert) - - 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. - - - Copyright (C) - - 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. - - , 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. - -END GNU GPL 2.0 - - -BEGIN CeCILL-B free software license (for Ssreflect, MathComp) - -CeCILL-B FREE SOFTWARE LICENSE AGREEMENT - - - Notice - -This Agreement is a Free Software license agreement that is the result -of discussions between its authors in order to ensure compliance with -the two main principles guiding its drafting: - - * firstly, compliance with the principles governing the distribution - of Free Software: access to source code, broad rights granted to - users, - * secondly, the election of a governing law, French law, with which - it is conformant, both as regards the law of torts and - intellectual property law, and the protection that it offers to - both authors and holders of the economic rights over software. - -The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) -license are: - -Commissariat à l'Energie Atomique - CEA, a public scientific, technical -and industrial research establishment, having its principal place of -business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. - -Centre National de la Recherche Scientifique - CNRS, a public scientific -and technological establishment, having its principal place of business -at 3 rue Michel-Ange, 75794 Paris cedex 16, France. - -Institut National de Recherche en Informatique et en Automatique - -INRIA, a public scientific and technological establishment, having its -principal place of business at Domaine de Voluceau, Rocquencourt, BP -105, 78153 Le Chesnay cedex, France. - - - Preamble - -This Agreement is an open source software license intended to give users -significant freedom to modify and redistribute the software licensed -hereunder. - -The exercising of this freedom is conditional upon a strong obligation -of giving credits for everybody that distributes a software -incorporating a software ruled by the current license so as all -contributions to be properly identified and acknowledged. - -In consideration of access to the source code and the rights to copy, -modify and redistribute granted by the license, users are provided only -with a limited warranty and the software's author, the holder of the -economic rights, and the successive licensors only have limited liability. - -In this respect, the risks associated with loading, using, modifying -and/or developing or reproducing the software by the user are brought to -the user's attention, given its Free Software status, which may make it -complicated to use, with the result that its use is reserved for -developers and experienced professionals having in-depth computer -knowledge. Users are therefore encouraged to load and test the -suitability of the software as regards their requirements in conditions -enabling the security of their systems and/or data to be ensured and, -more generally, to use and operate it in the same conditions of -security. This Agreement may be freely reproduced and published, -provided it is not altered, and that no provisions are either added or -removed herefrom. - -This Agreement may apply to any or all software for which the holder of -the economic rights decides to submit the use thereof to its provisions. - - - Article 1 - DEFINITIONS - -For the purpose of this Agreement, when the following expressions -commence with a capital letter, they shall have the following meaning: - -Agreement: means this license agreement, and its possible subsequent -versions and annexes. - -Software: means the software in its Object Code and/or Source Code form -and, where applicable, its documentation, "as is" when the Licensee -accepts the Agreement. - -Initial Software: means the Software in its Source Code and possibly its -Object Code form and, where applicable, its documentation, "as is" when -it is first distributed under the terms and conditions of the Agreement. - -Modified Software: means the Software modified by at least one -Contribution. - -Source Code: means all the Software's instructions and program lines to -which access is required so as to modify the Software. - -Object Code: means the binary files originating from the compilation of -the Source Code. - -Holder: means the holder(s) of the economic rights over the Initial -Software. - -Licensee: means the Software user(s) having accepted the Agreement. - -Contributor: means a Licensee having made at least one Contribution. - -Licensor: means the Holder, or any other individual or legal entity, who -distributes the Software under the Agreement. - -Contribution: means any or all modifications, corrections, translations, -adaptations and/or new functions integrated into the Software by any or -all Contributors, as well as any or all Internal Modules. - -Module: means a set of sources files including their documentation that -enables supplementary functions or services in addition to those offered -by the Software. - -External Module: means any or all Modules, not derived from the -Software, so that this Module and the Software run in separate address -spaces, with one calling the other when they are run. - -Internal Module: means any or all Module, connected to the Software so -that they both execute in the same address space. - -Parties: mean both the Licensee and the Licensor. - -These expressions may be used both in singular and plural form. - - - Article 2 - PURPOSE - -The purpose of the Agreement is the grant by the Licensor to the -Licensee of a non-exclusive, transferable and worldwide license for the -Software as set forth in Article 5 hereinafter for the whole term of the -protection granted by the rights over said Software. - - - Article 3 - ACCEPTANCE - -3.1 The Licensee shall be deemed as having accepted the terms and -conditions of this Agreement upon the occurrence of the first of the -following events: - - * (i) loading the Software by any or all means, notably, by - downloading from a remote server, or by loading from a physical - medium; - * (ii) the first time the Licensee exercises any of the rights - granted hereunder. - -3.2 One copy of the Agreement, containing a notice relating to the -characteristics of the Software, to the limited warranty, and to the -fact that its use is restricted to experienced users has been provided -to the Licensee prior to its acceptance as set forth in Article 3.1 -hereinabove, and the Licensee hereby acknowledges that it has read and -understood it. - - - Article 4 - EFFECTIVE DATE AND TERM - - - 4.1 EFFECTIVE DATE - -The Agreement shall become effective on the date when it is accepted by -the Licensee as set forth in Article 3.1. - - - 4.2 TERM - -The Agreement shall remain in force for the entire legal term of -protection of the economic rights over the Software. - - - Article 5 - SCOPE OF RIGHTS GRANTED - -The Licensor hereby grants to the Licensee, who accepts, the following -rights over the Software for any or all use, and for the term of the -Agreement, on the basis of the terms and conditions set forth hereinafter. - -Besides, if the Licensor owns or comes to own one or more patents -protecting all or part of the functions of the Software or of its -components, the Licensor undertakes not to enforce the rights granted by -these patents against successive Licensees using, exploiting or -modifying the Software. If these patents are transferred, the Licensor -undertakes to have the transferees subscribe to the obligations set -forth in this paragraph. - - - 5.1 RIGHT OF USE - -The Licensee is authorized to use the Software, without any limitation -as to its fields of application, with it being hereinafter specified -that this comprises: - - 1. permanent or temporary reproduction of all or part of the Software - by any or all means and in any or all form. - - 2. loading, displaying, running, or storing the Software on any or - all medium. - - 3. entitlement to observe, study or test its operation so as to - determine the ideas and principles behind any or all constituent - elements of said Software. This shall apply when the Licensee - carries out any or all loading, displaying, running, transmission - or storage operation as regards the Software, that it is entitled - to carry out hereunder. - - - 5.2 ENTITLEMENT TO MAKE CONTRIBUTIONS - -The right to make Contributions includes the right to translate, adapt, -arrange, or make any or all modifications to the Software, and the right -to reproduce the resulting software. - -The Licensee is authorized to make any or all Contributions to the -Software provided that it includes an explicit notice that it is the -author of said Contribution and indicates the date of the creation thereof. - - - 5.3 RIGHT OF DISTRIBUTION - -In particular, the right of distribution includes the right to publish, -transmit and communicate the Software to the general public on any or -all medium, and by any or all means, and the right to market, either in -consideration of a fee, or free of charge, one or more copies of the -Software by any means. - -The Licensee is further authorized to distribute copies of the modified -or unmodified Software to third parties according to the terms and -conditions set forth hereinafter. - - - 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION - -The Licensee is authorized to distribute true copies of the Software in -Source Code or Object Code form, provided that said distribution -complies with all the provisions of the Agreement and is accompanied by: - - 1. a copy of the Agreement, - - 2. a notice relating to the limitation of both the Licensor's - warranty and liability as set forth in Articles 8 and 9, - -and that, in the event that only the Object Code of the Software is -redistributed, the Licensee allows effective access to the full Source -Code of the Software at a minimum during the entire period of its -distribution of the Software, it being understood that the additional -cost of acquiring the Source Code shall not exceed the cost of -transferring the data. - - - 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE - -If the Licensee makes any Contribution to the Software, the resulting -Modified Software may be distributed under a license agreement other -than this Agreement subject to compliance with the provisions of Article -5.3.4. - - - 5.3.3 DISTRIBUTION OF EXTERNAL MODULES - -When the Licensee has developed an External Module, the terms and -conditions of this Agreement do not apply to said External Module, that -may be distributed under a separate license agreement. - - - 5.3.4 CREDITS - -Any Licensee who may distribute a Modified Software hereby expressly -agrees to: - - 1. indicate in the related documentation that it is based on the - Software licensed hereunder, and reproduce the intellectual - property notice for the Software, - - 2. ensure that written indications of the Software intended use, - intellectual property notice and license hereunder are included in - easily accessible format from the Modified Software interface, - - 3. mention, on a freely accessible website describing the Modified - Software, at least throughout the distribution term thereof, that - it is based on the Software licensed hereunder, and reproduce the - Software intellectual property notice, - - 4. where it is distributed to a third party that may distribute a - Modified Software without having to make its source code - available, make its best efforts to ensure that said third party - agrees to comply with the obligations set forth in this Article . - -If the Software, whether or not modified, is distributed with an -External Module designed for use in connection with the Software, the -Licensee shall submit said External Module to the foregoing obligations. - - - 5.3.5 COMPATIBILITY WITH THE CeCILL AND CeCILL-C LICENSES - -Where a Modified Software contains a Contribution subject to the CeCILL -license, the provisions set forth in Article 5.3.4 shall be optional. - -A Modified Software may be distributed under the CeCILL-C license. In -such a case the provisions set forth in Article 5.3.4 shall be optional. - - - Article 6 - INTELLECTUAL PROPERTY - - - 6.1 OVER THE INITIAL SOFTWARE - -The Holder owns the economic rights over the Initial Software. Any or -all use of the Initial Software is subject to compliance with the terms -and conditions under which the Holder has elected to distribute its work -and no one shall be entitled to modify the terms and conditions for the -distribution of said Initial Software. - -The Holder undertakes that the Initial Software will remain ruled at -least by this Agreement, for the duration set forth in Article 4.2. - - - 6.2 OVER THE CONTRIBUTIONS - -The Licensee who develops a Contribution is the owner of the -intellectual property rights over this Contribution as defined by -applicable law. - - - 6.3 OVER THE EXTERNAL MODULES - -The Licensee who develops an External Module is the owner of the -intellectual property rights over this External Module as defined by -applicable law and is free to choose the type of agreement that shall -govern its distribution. - - - 6.4 JOINT PROVISIONS - -The Licensee expressly undertakes: - - 1. not to remove, or modify, in any manner, the intellectual property - notices attached to the Software; - - 2. to reproduce said notices, in an identical manner, in the copies - of the Software modified or not. - -The Licensee undertakes not to directly or indirectly infringe the -intellectual property rights of the Holder and/or Contributors on the -Software and to take, where applicable, vis-à-vis its staff, any and all -measures required to ensure respect of said intellectual property rights -of the Holder and/or Contributors. - - - Article 7 - RELATED SERVICES - -7.1 Under no circumstances shall the Agreement oblige the Licensor to -provide technical assistance or maintenance services for the Software. - -However, the Licensor is entitled to offer this type of services. The -terms and conditions of such technical assistance, and/or such -maintenance, shall be set forth in a separate instrument. Only the -Licensor offering said maintenance and/or technical assistance services -shall incur liability therefor. - -7.2 Similarly, any Licensor is entitled to offer to its licensees, under -its sole responsibility, a warranty, that shall only be binding upon -itself, for the redistribution of the Software and/or the Modified -Software, under terms and conditions that it is free to decide. Said -warranty, and the financial terms and conditions of its application, -shall be subject of a separate instrument executed between the Licensor -and the Licensee. - - - Article 8 - LIABILITY - -8.1 Subject to the provisions of Article 8.2, the Licensee shall be -entitled to claim compensation for any direct loss it may have suffered -from the Software as a result of a fault on the part of the relevant -Licensor, subject to providing evidence thereof. - -8.2 The Licensor's liability is limited to the commitments made under -this Agreement and shall not be incurred as a result of in particular: -(i) loss due the Licensee's total or partial failure to fulfill its -obligations, (ii) direct or consequential loss that is suffered by the -Licensee due to the use or performance of the Software, and (iii) more -generally, any consequential loss. In particular the Parties expressly -agree that any or all pecuniary or business loss (i.e. loss of data, -loss of profits, operating loss, loss of customers or orders, -opportunity cost, any disturbance to business activities) or any or all -legal proceedings instituted against the Licensee by a third party, -shall constitute consequential loss and shall not provide entitlement to -any or all compensation from the Licensor. - - - Article 9 - WARRANTY - -9.1 The Licensee acknowledges that the scientific and technical -state-of-the-art when the Software was distributed did not enable all -possible uses to be tested and verified, nor for the presence of -possible defects to be detected. In this respect, the Licensee's -attention has been drawn to the risks associated with loading, using, -modifying and/or developing and reproducing the Software which are -reserved for experienced users. - -The Licensee shall be responsible for verifying, by any or all means, -the suitability of the product for its requirements, its good working -order, and for ensuring that it shall not cause damage to either persons -or properties. - -9.2 The Licensor hereby represents, in good faith, that it is entitled -to grant all the rights over the Software (including in particular the -rights set forth in Article 5). - -9.3 The Licensee acknowledges that the Software is supplied "as is" by -the Licensor without any other express or tacit warranty, other than -that provided for in Article 9.2 and, in particular, without any warranty -as to its commercial value, its secured, safe, innovative or relevant -nature. - -Specifically, the Licensor does not warrant that the Software is free -from any error, that it will operate without interruption, that it will -be compatible with the Licensee's own equipment and software -configuration, nor that it will meet the Licensee's requirements. - -9.4 The Licensor does not either expressly or tacitly warrant that the -Software does not infringe any third party intellectual property right -relating to a patent, software or any other property right. Therefore, -the Licensor disclaims any and all liability towards the Licensee -arising out of any or all proceedings for infringement that may be -instituted in respect of the use, modification and redistribution of the -Software. Nevertheless, should such proceedings be instituted against -the Licensee, the Licensor shall provide it with technical and legal -assistance for its defense. Such technical and legal assistance shall be -decided on a case-by-case basis between the relevant Licensor and the -Licensee pursuant to a memorandum of understanding. The Licensor -disclaims any and all liability as regards the Licensee's use of the -name of the Software. No warranty is given as regards the existence of -prior rights over the name of the Software or as regards the existence -of a trademark. - - - Article 10 - TERMINATION - -10.1 In the event of a breach by the Licensee of its obligations -hereunder, the Licensor may automatically terminate this Agreement -thirty (30) days after notice has been sent to the Licensee and has -remained ineffective. - -10.2 A Licensee whose Agreement is terminated shall no longer be -authorized to use, modify or distribute the Software. However, any -licenses that it may have granted prior to termination of the Agreement -shall remain valid subject to their having been granted in compliance -with the terms and conditions hereof. - - - Article 11 - MISCELLANEOUS - - - 11.1 EXCUSABLE EVENTS - -Neither Party shall be liable for any or all delay, or failure to -perform the Agreement, that may be attributable to an event of force -majeure, an act of God or an outside cause, such as defective -functioning or interruptions of the electricity or telecommunications -networks, network paralysis following a virus attack, intervention by -government authorities, natural disasters, water damage, earthquakes, -fire, explosions, strikes and labor unrest, war, etc. - -11.2 Any failure by either Party, on one or more occasions, to invoke -one or more of the provisions hereof, shall under no circumstances be -interpreted as being a waiver by the interested Party of its right to -invoke said provision(s) subsequently. - -11.3 The Agreement cancels and replaces any or all previous agreements, -whether written or oral, between the Parties and having the same -purpose, and constitutes the entirety of the agreement between said -Parties concerning said purpose. No supplement or modification to the -terms and conditions hereof shall be effective as between the Parties -unless it is made in writing and signed by their duly authorized -representatives. - -11.4 In the event that one or more of the provisions hereof were to -conflict with a current or future applicable act or legislative text, -said act or legislative text shall prevail, and the Parties shall make -the necessary amendments so as to comply with said act or legislative -text. All other provisions shall remain effective. Similarly, invalidity -of a provision of the Agreement, for any reason whatsoever, shall not -cause the Agreement as a whole to be invalid. - - - 11.5 LANGUAGE - -The Agreement is drafted in both French and English and both versions -are deemed authentic. - - - Article 12 - NEW VERSIONS OF THE AGREEMENT - -12.1 Any person is authorized to duplicate and distribute copies of this -Agreement. - -12.2 So as to ensure coherence, the wording of this Agreement is -protected and may only be modified by the authors of the License, who -reserve the right to periodically publish updates or new versions of the -Agreement, each with a separate number. These subsequent versions may -address new issues encountered by Free Software. - -12.3 Any Software distributed under a given version of the Agreement may -only be subsequently distributed under the same version of the Agreement -or a subsequent version. - - - Article 13 - GOVERNING LAW AND JURISDICTION - -13.1 The Agreement is governed by French law. The Parties agree to -endeavor to seek an amicable solution to any disagreements or disputes -that may arise during the performance of the Agreement. - -13.2 Failing an amicable solution within two (2) months as from their -occurrence, and unless emergency proceedings are necessary, the -disagreements or disputes shall be referred to the Paris Courts having -jurisdiction, by the more diligent Party. - - -Version 1.0 dated 2006-09-05. - -END CeCILL-B free software license - - -BEGIN GNU LGPL 3.0 (for Flocq) - - GNU LESSER GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - - This version of the GNU Lesser General Public License incorporates -the terms and conditions of version 3 of the GNU General Public -License, supplemented by the additional permissions listed below. - - 0. Additional Definitions. - - As used herein, "this License" refers to version 3 of the GNU Lesser -General Public License, and the "GNU GPL" refers to version 3 of the GNU -General Public License. - - "The Library" refers to a covered work governed by this License, -other than an Application or a Combined Work as defined below. - - An "Application" is any work that makes use of an interface provided -by the Library, but which is not otherwise based on the Library. -Defining a subclass of a class defined by the Library is deemed a mode -of using an interface provided by the Library. - - A "Combined Work" is a work produced by combining or linking an -Application with the Library. The particular version of the Library -with which the Combined Work was made is also called the "Linked -Version". - - The "Minimal Corresponding Source" for a Combined Work means the -Corresponding Source for the Combined Work, excluding any source code -for portions of the Combined Work that, considered in isolation, are -based on the Application, and not on the Linked Version. - - The "Corresponding Application Code" for a Combined Work means the -object code and/or source code for the Application, including any data -and utility programs needed for reproducing the Combined Work from the -Application, but excluding the System Libraries of the Combined Work. - - 1. Exception to Section 3 of the GNU GPL. - - You may convey a covered work under sections 3 and 4 of this License -without being bound by section 3 of the GNU GPL. - - 2. Conveying Modified Versions. - - If you modify a copy of the Library, and, in your modifications, a -facility refers to a function or data to be supplied by an Application -that uses the facility (other than as an argument passed when the -facility is invoked), then you may convey a copy of the modified -version: - - a) under this License, provided that you make a good faith effort to - ensure that, in the event an Application does not supply the - function or data, the facility still operates, and performs - whatever part of its purpose remains meaningful, or - - b) under the GNU GPL, with none of the additional permissions of - this License applicable to that copy. - - 3. Object Code Incorporating Material from Library Header Files. - - The object code form of an Application may incorporate material from -a header file that is part of the Library. You may convey such object -code under terms of your choice, provided that, if the incorporated -material is not limited to numerical parameters, data structure -layouts and accessors, or small macros, inline functions and templates -(ten or fewer lines in length), you do both of the following: - - a) Give prominent notice with each copy of the object code that the - Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the object code with a copy of the GNU GPL and this license - document. - - 4. Combined Works. - - You may convey a Combined Work under terms of your choice that, -taken together, effectively do not restrict modification of the -portions of the Library contained in the Combined Work and reverse -engineering for debugging such modifications, if you also do each of -the following: - - a) Give prominent notice with each copy of the Combined Work that - the Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the Combined Work with a copy of the GNU GPL and this license - document. - - c) For a Combined Work that displays copyright notices during - execution, include the copyright notice for the Library among - these notices, as well as a reference directing the user to the - copies of the GNU GPL and this license document. - - d) Do one of the following: - - 0) Convey the Minimal Corresponding Source under the terms of this - License, and the Corresponding Application Code in a form - suitable for, and under terms that permit, the user to - recombine or relink the Application with a modified version of - the Linked Version to produce a modified Combined Work, in the - manner specified by section 6 of the GNU GPL for conveying - Corresponding Source. - - 1) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (a) uses at run time - a copy of the Library already present on the user's computer - system, and (b) will operate properly with a modified version - of the Library that is interface-compatible with the Linked - Version. - - e) Provide Installation Information, but only if you would otherwise - be required to provide such information under section 6 of the - GNU GPL, and only to the extent that such information is - necessary to install and execute a modified version of the - Combined Work produced by recombining or relinking the - Application with a modified version of the Linked Version. (If - you use option 4d0, the Installation Information must accompany - the Minimal Corresponding Source and Corresponding Application - Code. If you use option 4d1, you must provide the Installation - Information in the manner specified by section 6 of the GNU GPL - for conveying Corresponding Source.) - - 5. Combined Libraries. - - You may place library facilities that are a work based on the -Library side by side in a single library together with other library -facilities that are not Applications and are not covered by this -License, and convey such a combined library under terms of your -choice, if you do both of the following: - - a) Accompany the combined library with a copy of the same work based - on the Library, uncombined with any other library facilities, - conveyed under the terms of this License. - - b) Give prominent notice with the combined library that part of it - is a work based on the Library, and explaining where to find the - accompanying uncombined form of the same work. - - 6. Revised Versions of the GNU Lesser General Public License. - - The Free Software Foundation may publish revised and/or new versions -of the GNU Lesser 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 -Library as you received it specifies that a certain numbered version -of the GNU Lesser General Public License "or any later version" -applies to it, you have the option of following the terms and -conditions either of that published version or of any later version -published by the Free Software Foundation. If the Library as you -received it does not specify a version number of the GNU Lesser -General Public License, you may choose any version of the GNU Lesser -General Public License ever published by the Free Software Foundation. - - If the Library as you received it specifies that a proxy can decide -whether future versions of the GNU Lesser General Public License shall -apply, that proxy's public statement of acceptance of any version is -permanent authorization for you to choose that version for the -Library. - -END GNU LGPL 3.0 diff --git a/LICENSE b/LICENSE index 5763ada..62e7122 100644 --- a/LICENSE +++ b/LICENSE @@ -2,26 +2,22 @@ VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations. Application to SAR Backprojection. -Version 1.0 (2015-12-04) - Copyright (C) 2015 Reservoir Labs Inc. -All rights reserved. +Copyright (C) 2021-22 Andrew W. Appel and Ariel Kellison -This software and each of its files are free software. With the -exception of patches/interval.patch (which you can redistribute and/or -modify under the terms of CeCILL-C, version 1.0, reproduced verbatim -in extenso in cecill-c-1.0.txt), you can redistribute them and/or modify -them under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License (GNU GPL -v3), or (at your option) any later version. A verbatim copy of the -GNU GPL v3 is included in gpl-3.0.txt. +This software and each of its files are free software. You can +redistribute them and/or modify them under the terms of the GNU +General Public License as published by the Free Software Foundation, +either version 3 of the License (GNU GPL v3), or (at your option) any +later version. A verbatim copy of the GNU GPL v3 is included in +gpl-3.0.txt. This software 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 GPL v3 (and CeCILL-C for patches/interval.patch) for more details. -This work is sponsored in part by DARPA MTO as part of the Power +This work was sponsored in part by DARPA MTO as part of the Power Efficiency Revolution for Embedded Computing Technologies (PERFECT) program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The views and conclusions contained in this work are those of the authors @@ -41,9 +37,5 @@ Computations. In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs) 2016. - -VCFloat requires third-party libraries listed in ACKS along with their -copyright information. - -VCFloat depends on third-party libraries listed in ACKS along with -their copyright and licensing information. +VCFloat requires uses third-party libraries listed in ACKS, which +have various licenses of their own. diff --git a/cecill-c-1.0.txt b/cecill-c-1.0.txt deleted file mode 100644 index 3d2a819..0000000 --- a/cecill-c-1.0.txt +++ /dev/null @@ -1,517 +0,0 @@ - -CeCILL-C FREE SOFTWARE LICENSE AGREEMENT - - - Notice - -This Agreement is a Free Software license agreement that is the result -of discussions between its authors in order to ensure compliance with -the two main principles guiding its drafting: - - * firstly, compliance with the principles governing the distribution - of Free Software: access to source code, broad rights granted to - users, - * secondly, the election of a governing law, French law, with which - it is conformant, both as regards the law of torts and - intellectual property law, and the protection that it offers to - both authors and holders of the economic rights over software. - -The authors of the CeCILL-C (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) -license are: - -Commissariat à l'Energie Atomique - CEA, a public scientific, technical -and industrial research establishment, having its principal place of -business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. - -Centre National de la Recherche Scientifique - CNRS, a public scientific -and technological establishment, having its principal place of business -at 3 rue Michel-Ange, 75794 Paris cedex 16, France. - -Institut National de Recherche en Informatique et en Automatique - -INRIA, a public scientific and technological establishment, having its -principal place of business at Domaine de Voluceau, Rocquencourt, BP -105, 78153 Le Chesnay cedex, France. - - - Preamble - -The purpose of this Free Software license agreement is to grant users -the right to modify and re-use the software governed by this license. - -The exercising of this right is conditional upon the obligation to make -available to the community the modifications made to the source code of -the software so as to contribute to its evolution. - -In consideration of access to the source code and the rights to copy, -modify and redistribute granted by the license, users are provided only -with a limited warranty and the software's author, the holder of the -economic rights, and the successive licensors only have limited liability. - -In this respect, the risks associated with loading, using, modifying -and/or developing or reproducing the software by the user are brought to -the user's attention, given its Free Software status, which may make it -complicated to use, with the result that its use is reserved for -developers and experienced professionals having in-depth computer -knowledge. Users are therefore encouraged to load and test the -suitability of the software as regards their requirements in conditions -enabling the security of their systems and/or data to be ensured and, -more generally, to use and operate it in the same conditions of -security. This Agreement may be freely reproduced and published, -provided it is not altered, and that no provisions are either added or -removed herefrom. - -This Agreement may apply to any or all software for which the holder of -the economic rights decides to submit the use thereof to its provisions. - - - Article 1 - DEFINITIONS - -For the purpose of this Agreement, when the following expressions -commence with a capital letter, they shall have the following meaning: - -Agreement: means this license agreement, and its possible subsequent -versions and annexes. - -Software: means the software in its Object Code and/or Source Code form -and, where applicable, its documentation, "as is" when the Licensee -accepts the Agreement. - -Initial Software: means the Software in its Source Code and possibly its -Object Code form and, where applicable, its documentation, "as is" when -it is first distributed under the terms and conditions of the Agreement. - -Modified Software: means the Software modified by at least one -Integrated Contribution. - -Source Code: means all the Software's instructions and program lines to -which access is required so as to modify the Software. - -Object Code: means the binary files originating from the compilation of -the Source Code. - -Holder: means the holder(s) of the economic rights over the Initial -Software. - -Licensee: means the Software user(s) having accepted the Agreement. - -Contributor: means a Licensee having made at least one Integrated -Contribution. - -Licensor: means the Holder, or any other individual or legal entity, who -distributes the Software under the Agreement. - -Integrated Contribution: means any or all modifications, corrections, -translations, adaptations and/or new functions integrated into the -Source Code by any or all Contributors. - -Related Module: means a set of sources files including their -documentation that, without modification to the Source Code, enables -supplementary functions or services in addition to those offered by the -Software. - -Derivative Software: means any combination of the Software, modified or -not, and of a Related Module. - -Parties: mean both the Licensee and the Licensor. - -These expressions may be used both in singular and plural form. - - - Article 2 - PURPOSE - -The purpose of the Agreement is the grant by the Licensor to the -Licensee of a non-exclusive, transferable and worldwide license for the -Software as set forth in Article 5 hereinafter for the whole term of the -protection granted by the rights over said Software. - - - Article 3 - ACCEPTANCE - -3.1 The Licensee shall be deemed as having accepted the terms and -conditions of this Agreement upon the occurrence of the first of the -following events: - - * (i) loading the Software by any or all means, notably, by - downloading from a remote server, or by loading from a physical - medium; - * (ii) the first time the Licensee exercises any of the rights - granted hereunder. - -3.2 One copy of the Agreement, containing a notice relating to the -characteristics of the Software, to the limited warranty, and to the -fact that its use is restricted to experienced users has been provided -to the Licensee prior to its acceptance as set forth in Article 3.1 -hereinabove, and the Licensee hereby acknowledges that it has read and -understood it. - - - Article 4 - EFFECTIVE DATE AND TERM - - - 4.1 EFFECTIVE DATE - -The Agreement shall become effective on the date when it is accepted by -the Licensee as set forth in Article 3.1. - - - 4.2 TERM - -The Agreement shall remain in force for the entire legal term of -protection of the economic rights over the Software. - - - Article 5 - SCOPE OF RIGHTS GRANTED - -The Licensor hereby grants to the Licensee, who accepts, the following -rights over the Software for any or all use, and for the term of the -Agreement, on the basis of the terms and conditions set forth hereinafter. - -Besides, if the Licensor owns or comes to own one or more patents -protecting all or part of the functions of the Software or of its -components, the Licensor undertakes not to enforce the rights granted by -these patents against successive Licensees using, exploiting or -modifying the Software. If these patents are transferred, the Licensor -undertakes to have the transferees subscribe to the obligations set -forth in this paragraph. - - - 5.1 RIGHT OF USE - -The Licensee is authorized to use the Software, without any limitation -as to its fields of application, with it being hereinafter specified -that this comprises: - - 1. permanent or temporary reproduction of all or part of the Software - by any or all means and in any or all form. - - 2. loading, displaying, running, or storing the Software on any or - all medium. - - 3. entitlement to observe, study or test its operation so as to - determine the ideas and principles behind any or all constituent - elements of said Software. This shall apply when the Licensee - carries out any or all loading, displaying, running, transmission - or storage operation as regards the Software, that it is entitled - to carry out hereunder. - - - 5.2 RIGHT OF MODIFICATION - -The right of modification includes the right to translate, adapt, -arrange, or make any or all modifications to the Software, and the right -to reproduce the resulting software. It includes, in particular, the -right to create a Derivative Software. - -The Licensee is authorized to make any or all modification to the -Software provided that it includes an explicit notice that it is the -author of said modification and indicates the date of the creation thereof. - - - 5.3 RIGHT OF DISTRIBUTION - -In particular, the right of distribution includes the right to publish, -transmit and communicate the Software to the general public on any or -all medium, and by any or all means, and the right to market, either in -consideration of a fee, or free of charge, one or more copies of the -Software by any means. - -The Licensee is further authorized to distribute copies of the modified -or unmodified Software to third parties according to the terms and -conditions set forth hereinafter. - - - 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION - -The Licensee is authorized to distribute true copies of the Software in -Source Code or Object Code form, provided that said distribution -complies with all the provisions of the Agreement and is accompanied by: - - 1. a copy of the Agreement, - - 2. a notice relating to the limitation of both the Licensor's - warranty and liability as set forth in Articles 8 and 9, - -and that, in the event that only the Object Code of the Software is -redistributed, the Licensee allows effective access to the full Source -Code of the Software at a minimum during the entire period of its -distribution of the Software, it being understood that the additional -cost of acquiring the Source Code shall not exceed the cost of -transferring the data. - - - 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE - -When the Licensee makes an Integrated Contribution to the Software, the -terms and conditions for the distribution of the resulting Modified -Software become subject to all the provisions of this Agreement. - -The Licensee is authorized to distribute the Modified Software, in -source code or object code form, provided that said distribution -complies with all the provisions of the Agreement and is accompanied by: - - 1. a copy of the Agreement, - - 2. a notice relating to the limitation of both the Licensor's - warranty and liability as set forth in Articles 8 and 9, - -and that, in the event that only the object code of the Modified -Software is redistributed, the Licensee allows effective access to the -full source code of the Modified Software at a minimum during the entire -period of its distribution of the Modified Software, it being understood -that the additional cost of acquiring the source code shall not exceed -the cost of transferring the data. - - - 5.3.3 DISTRIBUTION OF DERIVATIVE SOFTWARE - -When the Licensee creates Derivative Software, this Derivative Software -may be distributed under a license agreement other than this Agreement, -subject to compliance with the requirement to include a notice -concerning the rights over the Software as defined in Article 6.4. -In the event the creation of the Derivative Software required modification -of the Source Code, the Licensee undertakes that: - - 1. the resulting Modified Software will be governed by this Agreement, - 2. the Integrated Contributions in the resulting Modified Software - will be clearly identified and documented, - 3. the Licensee will allow effective access to the source code of the - Modified Software, at a minimum during the entire period of - distribution of the Derivative Software, such that such - modifications may be carried over in a subsequent version of the - Software; it being understood that the additional cost of - purchasing the source code of the Modified Software shall not - exceed the cost of transferring the data. - - - 5.3.4 COMPATIBILITY WITH THE CeCILL LICENSE - -When a Modified Software contains an Integrated Contribution subject to -the CeCILL license agreement, or when a Derivative Software contains a -Related Module subject to the CeCILL license agreement, the provisions -set forth in the third item of Article 6.4 are optional. - - - Article 6 - INTELLECTUAL PROPERTY - - - 6.1 OVER THE INITIAL SOFTWARE - -The Holder owns the economic rights over the Initial Software. Any or -all use of the Initial Software is subject to compliance with the terms -and conditions under which the Holder has elected to distribute its work -and no one shall be entitled to modify the terms and conditions for the -distribution of said Initial Software. - -The Holder undertakes that the Initial Software will remain ruled at -least by this Agreement, for the duration set forth in Article 4.2. - - - 6.2 OVER THE INTEGRATED CONTRIBUTIONS - -The Licensee who develops an Integrated Contribution is the owner of the -intellectual property rights over this Contribution as defined by -applicable law. - - - 6.3 OVER THE RELATED MODULES - -The Licensee who develops a Related Module is the owner of the -intellectual property rights over this Related Module as defined by -applicable law and is free to choose the type of agreement that shall -govern its distribution under the conditions defined in Article 5.3.3. - - - 6.4 NOTICE OF RIGHTS - -The Licensee expressly undertakes: - - 1. not to remove, or modify, in any manner, the intellectual property - notices attached to the Software; - - 2. to reproduce said notices, in an identical manner, in the copies - of the Software modified or not; - - 3. to ensure that use of the Software, its intellectual property - notices and the fact that it is governed by the Agreement is - indicated in a text that is easily accessible, specifically from - the interface of any Derivative Software. - -The Licensee undertakes not to directly or indirectly infringe the -intellectual property rights of the Holder and/or Contributors on the -Software and to take, where applicable, vis-à-vis its staff, any and all -measures required to ensure respect of said intellectual property rights -of the Holder and/or Contributors. - - - Article 7 - RELATED SERVICES - -7.1 Under no circumstances shall the Agreement oblige the Licensor to -provide technical assistance or maintenance services for the Software. - -However, the Licensor is entitled to offer this type of services. The -terms and conditions of such technical assistance, and/or such -maintenance, shall be set forth in a separate instrument. Only the -Licensor offering said maintenance and/or technical assistance services -shall incur liability therefor. - -7.2 Similarly, any Licensor is entitled to offer to its licensees, under -its sole responsibility, a warranty, that shall only be binding upon -itself, for the redistribution of the Software and/or the Modified -Software, under terms and conditions that it is free to decide. Said -warranty, and the financial terms and conditions of its application, -shall be subject of a separate instrument executed between the Licensor -and the Licensee. - - - Article 8 - LIABILITY - -8.1 Subject to the provisions of Article 8.2, the Licensee shall be -entitled to claim compensation for any direct loss it may have suffered -from the Software as a result of a fault on the part of the relevant -Licensor, subject to providing evidence thereof. - -8.2 The Licensor's liability is limited to the commitments made under -this Agreement and shall not be incurred as a result of in particular: -(i) loss due the Licensee's total or partial failure to fulfill its -obligations, (ii) direct or consequential loss that is suffered by the -Licensee due to the use or performance of the Software, and (iii) more -generally, any consequential loss. In particular the Parties expressly -agree that any or all pecuniary or business loss (i.e. loss of data, -loss of profits, operating loss, loss of customers or orders, -opportunity cost, any disturbance to business activities) or any or all -legal proceedings instituted against the Licensee by a third party, -shall constitute consequential loss and shall not provide entitlement to -any or all compensation from the Licensor. - - - Article 9 - WARRANTY - -9.1 The Licensee acknowledges that the scientific and technical -state-of-the-art when the Software was distributed did not enable all -possible uses to be tested and verified, nor for the presence of -possible defects to be detected. In this respect, the Licensee's -attention has been drawn to the risks associated with loading, using, -modifying and/or developing and reproducing the Software which are -reserved for experienced users. - -The Licensee shall be responsible for verifying, by any or all means, -the suitability of the product for its requirements, its good working -order, and for ensuring that it shall not cause damage to either persons -or properties. - -9.2 The Licensor hereby represents, in good faith, that it is entitled -to grant all the rights over the Software (including in particular the -rights set forth in Article 5). - -9.3 The Licensee acknowledges that the Software is supplied "as is" by -the Licensor without any other express or tacit warranty, other than -that provided for in Article 9.2 and, in particular, without any warranty -as to its commercial value, its secured, safe, innovative or relevant -nature. - -Specifically, the Licensor does not warrant that the Software is free -from any error, that it will operate without interruption, that it will -be compatible with the Licensee's own equipment and software -configuration, nor that it will meet the Licensee's requirements. - -9.4 The Licensor does not either expressly or tacitly warrant that the -Software does not infringe any third party intellectual property right -relating to a patent, software or any other property right. Therefore, -the Licensor disclaims any and all liability towards the Licensee -arising out of any or all proceedings for infringement that may be -instituted in respect of the use, modification and redistribution of the -Software. Nevertheless, should such proceedings be instituted against -the Licensee, the Licensor shall provide it with technical and legal -assistance for its defense. Such technical and legal assistance shall be -decided on a case-by-case basis between the relevant Licensor and the -Licensee pursuant to a memorandum of understanding. The Licensor -disclaims any and all liability as regards the Licensee's use of the -name of the Software. No warranty is given as regards the existence of -prior rights over the name of the Software or as regards the existence -of a trademark. - - - Article 10 - TERMINATION - -10.1 In the event of a breach by the Licensee of its obligations -hereunder, the Licensor may automatically terminate this Agreement -thirty (30) days after notice has been sent to the Licensee and has -remained ineffective. - -10.2 A Licensee whose Agreement is terminated shall no longer be -authorized to use, modify or distribute the Software. However, any -licenses that it may have granted prior to termination of the Agreement -shall remain valid subject to their having been granted in compliance -with the terms and conditions hereof. - - - Article 11 - MISCELLANEOUS - - - 11.1 EXCUSABLE EVENTS - -Neither Party shall be liable for any or all delay, or failure to -perform the Agreement, that may be attributable to an event of force -majeure, an act of God or an outside cause, such as defective -functioning or interruptions of the electricity or telecommunications -networks, network paralysis following a virus attack, intervention by -government authorities, natural disasters, water damage, earthquakes, -fire, explosions, strikes and labor unrest, war, etc. - -11.2 Any failure by either Party, on one or more occasions, to invoke -one or more of the provisions hereof, shall under no circumstances be -interpreted as being a waiver by the interested Party of its right to -invoke said provision(s) subsequently. - -11.3 The Agreement cancels and replaces any or all previous agreements, -whether written or oral, between the Parties and having the same -purpose, and constitutes the entirety of the agreement between said -Parties concerning said purpose. No supplement or modification to the -terms and conditions hereof shall be effective as between the Parties -unless it is made in writing and signed by their duly authorized -representatives. - -11.4 In the event that one or more of the provisions hereof were to -conflict with a current or future applicable act or legislative text, -said act or legislative text shall prevail, and the Parties shall make -the necessary amendments so as to comply with said act or legislative -text. All other provisions shall remain effective. Similarly, invalidity -of a provision of the Agreement, for any reason whatsoever, shall not -cause the Agreement as a whole to be invalid. - - - 11.5 LANGUAGE - -The Agreement is drafted in both French and English and both versions -are deemed authentic. - - - Article 12 - NEW VERSIONS OF THE AGREEMENT - -12.1 Any person is authorized to duplicate and distribute copies of this -Agreement. - -12.2 So as to ensure coherence, the wording of this Agreement is -protected and may only be modified by the authors of the License, who -reserve the right to periodically publish updates or new versions of the -Agreement, each with a separate number. These subsequent versions may -address new issues encountered by Free Software. - -12.3 Any Software distributed under a given version of the Agreement may -only be subsequently distributed under the same version of the Agreement -or a subsequent version. - - - Article 13 - GOVERNING LAW AND JURISDICTION - -13.1 The Agreement is governed by French law. The Parties agree to -endeavor to seek an amicable solution to any disagreements or disputes -that may arise during the performance of the Agreement. - -13.2 Failing an amicable solution within two (2) months as from their -occurrence, and unless emergency proceedings are necessary, the -disagreements or disputes shall be referred to the Paris Courts having -jurisdiction, by the more diligent Party. - - -Version 1.0 dated 2006-09-05. diff --git a/clean_external_libs.sh b/clean_external_libs.sh deleted file mode 100755 index 25e53c4..0000000 --- a/clean_external_libs.sh +++ /dev/null @@ -1,51 +0,0 @@ -#!/bin/bash -# -# VCFloat: A Unified Coq Framework for Verifying C Programs with -# Floating-Point Computations. Application to SAR Backprojection. -# -# Version 1.0 (2015-12-04) -# -# Copyright (C) 2015 Reservoir Labs Inc. -# All rights reserved. -# -# This file, which is part of VCFloat, is free software. You can -# redistribute it and/or modify it under the terms of the GNU General -# Public License as published by the Free Software Foundation, either -# version 3 of the License (GNU GPL v3), or (at your option) any later -# version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt. -# -# This file 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 LICENSE for -# more details about the use and redistribution of this file and the -# whole VCFloat library. -# -# This work is sponsored in part by DARPA MTO as part of the Power -# Efficiency Revolution for Embedded Computing Technologies (PERFECT) -# program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The -# views and conclusions contained in this work are those of the authors -# and should not be interpreted as representing the official policies, -# either expressly or implied, of the DARPA or the -# U.S. Government. Distribution Statement "A" (Approved for Public -# Release, Distribution Unlimited.) -# -# -# If you are using or modifying VCFloat in your work, please consider -# citing the following paper: -# -# Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard -# Lethin. -# A Unified Coq Framework for Verifying C Programs with Floating-Point -# Computations. -# In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs) -# 2016. -# -# -# VCFloat requires third-party libraries listed in ACKS along with their -# copyright information. -# -# VCFloat depends on third-party libraries listed in ACKS along with -# their copyright and licensing information. -# -rm -rf compcert* mathcomp* ssreflect* flocq* interval* -chmod +x get_external_libs.sh diff --git a/configure b/configure deleted file mode 100755 index 8c75bb4..0000000 --- a/configure +++ /dev/null @@ -1,160 +0,0 @@ -#!/bin/bash -# -# VCFloat: A Unified Coq Framework for Verifying C Programs with -# Floating-Point Computations. Application to SAR Backprojection. -# -# Version 1.0 (2015-12-04) -# -# Copyright (C) 2015 Reservoir Labs Inc. -# All rights reserved. -# -# This file, which is part of VCFloat, is free software. You can -# redistribute it and/or modify it under the terms of the GNU General -# Public License as published by the Free Software Foundation, either -# version 3 of the License (GNU GPL v3), or (at your option) any later -# version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt. -# -# This file 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 LICENSE for -# more details about the use and redistribution of this file and the -# whole VCFloat library. -# -# This work is sponsored in part by DARPA MTO as part of the Power -# Efficiency Revolution for Embedded Computing Technologies (PERFECT) -# program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The -# views and conclusions contained in this work are those of the authors -# and should not be interpreted as representing the official policies, -# either expressly or implied, of the DARPA or the -# U.S. Government. Distribution Statement "A" (Approved for Public -# Release, Distribution Unlimited.) -# -# -# If you are using or modifying VCFloat in your work, please consider -# citing the following paper: -# -# Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard -# Lethin. -# A Unified Coq Framework for Verifying C Programs with Floating-Point -# Computations. -# In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs) -# 2016. -# -# -# VCFloat requires third-party libraries listed in ACKS along with their -# copyright information. -# -# VCFloat depends on third-party libraries listed in ACKS along with -# their copyright and licensing information. -# - - -USAGE=" -Usage: $0 - -Options: ---rcoqlib : specify the absolute to R-CoqLib's root directory - By default, it is initialized to the rcoqlib/ subdir - of the current directory, as installed by - get_external_libs.sh --h: display this list of options ---help: display this list of options -" - -RCOQLIB=`pwd`/rcoqlib - -while [ -n "$1" ] -do - arg="$1" - shift - case "$arg" in - (-h|--help) - echo "$USAGE" - exit 0 - ;; - (--rcoqlib) - RCOQLIB="$1" - shift - ;; - (*) - echo Invalid argument: "$arg" - echo "$USAGE" - exit 1 - ;; - esac -done - -if [ -z "$RCOQLIB" ] -then - echo Please specify the absolute path to R-CoqLib, using --rcoqlib. - echo - echo "$USAGE" - exit 1 -fi - -if [ ! -d compcert ] -then - echo Please get the external libraries first - echo "(e.g., by get_external_libs.sh)" - exit 1 -fi - -MOREOPTS=-no-native-compiler -MAKEOPTS= -for f in $MOREOPTS -do - MAKEOPTS="$MAKEOPTS -arg $f" -done - -OPTS="-R $RCOQLIB/rcoqlib rcoqlib -R $PWD/ssreflect/theories Ssreflect -R $PWD/mathcomp/theories MathComp -R $PWD/flocq/src Flocq -R $PWD/interval/src Interval -I $PWD/ssreflect/src" - -LIBS="compcert vcfloat" - -FILES= -FULLOPTS="$OPTS" -for f in $LIBS -do - OPTS="$OPTS -R $f $f" - FULLOPTS="$FULLOPTS -R $PWD/$f $f" - for g in $f/*.v $f/*/*.v - do - [ -e "$g" ] && FILES="$FILES $g" - done -done - -cat > coqopts < run-coqide.sh <> dir-locals <> dir-locals -done - -for f in $LIBS -do - { - echo "((nil . ((coq-load-path . (" - cat dir-locals - echo ")))))" - } > $f/.dir-locals.el -done diff --git a/get_external_libs.sh b/get_external_libs.sh deleted file mode 100755 index 52e6dc0..0000000 --- a/get_external_libs.sh +++ /dev/null @@ -1,167 +0,0 @@ -#!/bin/bash -# -# VCFloat: A Unified Coq Framework for Verifying C Programs with -# Floating-Point Computations. Application to SAR Backprojection. -# -# Version 1.0 (2015-12-04) -# -# Copyright (C) 2015 Reservoir Labs Inc. -# All rights reserved. -# -# This file, which is part of VCFloat, is free software. You can -# redistribute it and/or modify it under the terms of the GNU General -# Public License as published by the Free Software Foundation, either -# version 3 of the License (GNU GPL v3), or (at your option) any later -# version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt. -# -# This file 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 LICENSE for -# more details about the use and redistribution of this file and the -# whole VCFloat library. -# -# This work is sponsored in part by DARPA MTO as part of the Power -# Efficiency Revolution for Embedded Computing Technologies (PERFECT) -# program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The -# views and conclusions contained in this work are those of the authors -# and should not be interpreted as representing the official policies, -# either expressly or implied, of the DARPA or the -# U.S. Government. Distribution Statement "A" (Approved for Public -# Release, Distribution Unlimited.) -# -# -# If you are using or modifying VCFloat in your work, please consider -# citing the following paper: -# -# Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard -# Lethin. -# A Unified Coq Framework for Verifying C Programs with Floating-Point -# Computations. -# In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs) -# 2016. -# -# -# VCFloat requires third-party libraries listed in ACKS along with their -# copyright information. -# -# VCFloat depends on third-party libraries listed in ACKS along with -# their copyright and licensing information. -# -# External libraries needed by our work: -# R-CoqLib, CompCert, Flocq and Coq-Interval -# and their dependencies -# -# We assume that Coq 8.5beta2 (with real numbers), git, wget, autoconf -# and automake are already installed and in the PATH. Nothing else is -# needed. -# -# NOTE: This script is not required to be run from the full-scale -# submission VM. Everything is already installed and compiled. -# - -# Get and build R-CoqLib -if [ ! -d rcoqlib ] -then - git clone 'https://github.com/reservoirlabs/rcoqlib' rcoqlib || exit 1 - pushd rcoqlib || exit 1 - ./configure || exit 1 - make $* || exit 1 - popd || exit 1 -fi - -# Get CompCert Clight. -# NOTE: Since we are not compiling the whole CompCert, -# we do not need to use the copy of Flocq that is -# distributed with CompCert. - -if [ ! -d compcert ] -then - CC=compcert-2.4 - rm -rf $CC.tgz $CC compcert.aux - git clone 'https://github.com/AbsInt/CompCert.git' $CC || exit 1 - mkdir compcert.aux || exit 1 - pushd $CC || exit 1 - git checkout 5dd15440 || exit 1 - popd || exit 1 - cp -t compcert.aux $CC/{ia32/Archi,exportclight/Clightdefs,common/{AST,Errors,Events,Globalenvs,Memdata,Memory,Memtype,Smallstep,Values},cfrontend/{Clight,Cop,Ctypes},lib/{Axioms,Coqlib,Fappli_IEEE_extra,Floats,Integers,Intv,Maps}}.v || exit 1 - pushd compcert.aux || exit 1 - patch -p1 < ../patches/compcert.patch || exit 1 - popd || exit 1 - rm -rf $CC - mv compcert.aux compcert || exit 1 - true -else - true -fi - -# Get and build Ssreflect -SSR=ssreflect-1.5.coq85beta2 -if [ ! -d ssreflect ] -then - rm -rf $SSR.tar.gz $SSR - wget "http://ssr.msr-inria.inria.fr/FTP/$SSR.tar.gz" || exit 1 - tar xf $SSR.tar.gz || exit 1 - rm -f $SSR.tar.gz - mv $SSR ssreflect || exit 1 -else - true -fi -make -C ssreflect $* || exit 1 - -# Get and build MathComp -MC=mathcomp-1.5.coq85beta2 -if [ ! -d mathcomp ] -then - rm -rf $MC.tar.gz $MC - wget "http://ssr.msr-inria.inria.fr/FTP/$MC.tar.gz" || exit 1 - tar xf $MC.tar.gz || exit 1 - rm -f $MC.tar.gz - pushd $MC || exit 1 - echo "-R ../ssreflect/theories Ssreflect" >> Make || exit 1 - echo "-I ../ssreflect/src" >> Make || exit 1 - popd || exit 1 - mv $MC mathcomp || exit 1 -else - true -fi -make -C mathcomp $* || exit 1 - -# Get and build Flocq -if [ ! -d flocq ] -then - rm -rf flocq.aux - git clone 'https://gforge.inria.fr/git/flocq/flocq.git' flocq.aux || exit 1 - pushd flocq.aux || exit 1 - git checkout bcbcde24 || exit 1 - ./autogen.sh || exit 1 - ./configure || exit 1 - popd || exit 1 - mv flocq.aux flocq || exit 1 -else - true -fi -pushd flocq || exit 1 -./remake || exit 1 -popd || exit 1 - -# Get and build Coq-Interval -if [ ! -d interval ] -then - rm -rf interval.aux - git clone https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git interval.aux || exit 1 - pushd interval.aux || exit 1 - git checkout 81f1f918 || exit 1 - patch -p1 < ../patches/interval.patch || exit 1 - ./autogen.sh || exit 1 -COQC='coqc -R ../flocq/src Flocq -I ../ssreflect/src -R ../ssreflect/theories Ssreflect -R ../mathcomp/theories MathComp' ./configure || exit 1 - popd || exit 1 - mv interval.aux interval || exit 1 -else - true -fi -pushd interval || exit 1 -./remake || exit 1 -popd || exit 1 - -# Everything is installed. Disable this file -chmod -x $0 || exit 1 diff --git a/patches/compcert.patch b/patches/compcert.patch deleted file mode 100644 index d671bcf..0000000 --- a/patches/compcert.patch +++ /dev/null @@ -1,509 +0,0 @@ -# VCFloat: A Unified Coq Framework for Verifying C Programs with -# Floating-Point Computations. Application to SAR Backprojection. -# -# Version 1.0 (2015-12-04) -# -# Copyright (C) 2015 Reservoir Labs Inc. -# All rights reserved. -# -# This file, which is part of VCFloat, is free software. You can -# redistribute it and/or modify it under the terms of the GNU General -# Public License as published by the Free Software Foundation, either -# version 3 of the License (GNU GPL v3), or (at your option) any later -# version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt. -# -# This file 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 LICENSE for -# more details about the use and redistribution of this file and the -# whole VCFloat library. -# -# This work is sponsored in part by DARPA MTO as part of the Power -# Efficiency Revolution for Embedded Computing Technologies (PERFECT) -# program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The -# views and conclusions contained in this work are those of the authors -# and should not be interpreted as representing the official policies, -# either expressly or implied, of the DARPA or the -# U.S. Government. Distribution Statement "A" (Approved for Public -# Release, Distribution Unlimited.) -# -# -# If you are using or modifying VCFloat in your work, please consider -# citing the following paper: -# -# Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard -# Lethin. -# A Unified Coq Framework for Verifying C Programs with Floating-Point -# Computations. -# In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs) -# 2016. -# -# -# VCFloat requires third-party libraries listed in ACKS along with their -# copyright information. -# -# VCFloat depends on third-party libraries listed in ACKS along with -# their copyright and licensing information. ---- a/Archi.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Archi.v 2015-05-29 13:05:32.466278503 -0400 -@@ -17,8 +17,8 @@ - (** Architecture-dependent parameters for IA32 *) - - Require Import ZArith. --Require Import Fappli_IEEE. --Require Import Fappli_IEEE_bits. -+Require Import Flocq.Appli.Fappli_IEEE. -+Require Import Flocq.Appli.Fappli_IEEE_bits. - - Definition big_endian := false. - -@@ -26,13 +26,13 @@ - Notation align_float64 := 4%Z (only parsing). - - Program Definition default_pl_64 : bool * nan_pl 53 := -- (true, nat_iter 51 xO xH). -+ (true, Fcore_Zaux.iter_nat xO 51 xH). - - Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := - false. (**r always choose first NaN *) - - Program Definition default_pl_32 : bool * nan_pl 24 := -- (true, nat_iter 22 xO xH). -+ (true, Fcore_Zaux.iter_nat xO 22 xH). - - Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := - false. (**r always choose first NaN *) ---- a/AST.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/AST.v 2015-05-29 13:45:17.649271910 -0400 -@@ -19,7 +19,7 @@ - Require Import Coqlib. - Require String. - Require Import Errors. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - - Set Implicit Arguments. -@@ -100,12 +100,13 @@ - calling conventions for the function. *) - - Record calling_convention : Type := mkcallconv { -- cc_vararg: bool; -- cc_structret: bool -+ cc_vararg: bool; (**r variable-arity function *) -+ cc_unproto: bool; (**r old-style unprototyped function *) -+ cc_structret: bool (**r function returning a struct *) - }. - - Definition cc_default := -- {| cc_vararg := false; cc_structret := false |}. -+ {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. - - Record signature : Type := mksignature { - sig_args: list typ; ---- a/Clightdefs.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Clightdefs.v 2015-05-29 15:51:18.296098977 -0400 -@@ -17,7 +17,7 @@ - - Require Export List. - Require Export ZArith. --Require Export Integers. -+Require Export compcert.Integers. - Require Export Floats. - Require Export AST. - Require Export Ctypes. ---- a/Clight.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Clight.v 2015-05-29 12:48:21.953015627 -0400 -@@ -20,7 +20,7 @@ - Require Import Coqlib. - Require Import Errors. - Require Import Maps. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Import AST. ---- a/Cop.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Cop.v 2015-05-29 14:00:44.766474897 -0400 -@@ -17,7 +17,7 @@ - - Require Import Coqlib. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Import Memory. ---- a/Coqlib.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Coqlib.v 2015-05-29 12:54:31.693475445 -0400 -@@ -51,7 +51,7 @@ - Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. - Proof. auto. Qed. - --Ltac exploit x := -+Ltac eexploit x := ( - refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) -@@ -86,7 +86,10 @@ - || refine (modusponens _ _ (x _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _) _) - || refine (modusponens _ _ (x _ _) _) -- || refine (modusponens _ _ (x _) _). -+ || refine (modusponens _ _ (x _) _) -+). -+ -+Ltac exploit x := eexploit x; shelve_unifiable. - - (** * Definitions and theorems over the type [positive] *) - ---- a/Events.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Events.v 2015-05-29 13:55:54.130101686 -0400 -@@ -18,7 +18,7 @@ - Require Import Coqlib. - Require Intv. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Import Memory. ---- a/Fappli_IEEE_extra.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Fappli_IEEE_extra.v 2015-05-29 13:32:25.248259985 -0400 -@@ -20,15 +20,15 @@ - Require Import Psatz. - Require Import Bool. - Require Import Eqdep_dec. --Require Import Fcore. --Require Import Fcore_digits. --Require Import Fcalc_digits. --Require Import Fcalc_ops. --Require Import Fcalc_round. --Require Import Fcalc_bracket. --Require Import Fprop_Sterbenz. --Require Import Fappli_IEEE. --Require Import Fappli_rnd_odd. -+Require Import Flocq.Core.Fcore. -+Require Import Flocq.Core.Fcore_digits. -+Require Import Flocq.Calc.Fcalc_digits. -+Require Import Flocq.Calc.Fcalc_ops. -+Require Import Flocq.Calc.Fcalc_round. -+Require Import Flocq.Calc.Fcalc_bracket. -+Require Import Flocq.Prop.Fprop_Sterbenz. -+Require Import Flocq.Appli.Fappli_IEEE. -+Require Import Flocq.Appli.Fappli_rnd_odd. - - Local Open Scope Z_scope. - -@@ -63,10 +63,10 @@ - - Definition is_finite_pos0 (f: binary_float) : bool := - match f with -- | B754_zero s => negb s -- | B754_infinity _ => false -- | B754_nan _ _ => false -- | B754_finite _ _ _ _ => true -+ | B754_zero _ _ s => negb s -+ | B754_infinity _ _ _ => false -+ | B754_nan _ _ _ _ => false -+ | B754_finite _ _ _ _ _ _ => true - end. - - Lemma Bsign_pos0: -@@ -693,10 +693,10 @@ - - Definition ZofB (f: binary_float): option Z := - match f with -- | B754_finite s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z -- | B754_finite s m 0 _ => Some (cond_Zopp s (Zpos m)) -- | B754_finite s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z -- | B754_zero _ => Some 0%Z -+ | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z -+ | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) -+ | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z -+ | B754_zero _ _ _ => Some 0%Z - | _ => None - end. - -@@ -949,7 +949,7 @@ - - revert H H0. fold emin. fold fexp. - set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x). - set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y). -- rewrite (Rmult_comm ry rx). destruct Rlt_bool. -+ rewrite (Rmult_comm ry rx). destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode) (rx * ry))) (bpow radix2 emax)). - + intros (A1 & A2 & A3) (B1 & B2 & B3). - apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto. - rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm. -@@ -1002,9 +1002,9 @@ - Remark Bexact_inverse_mantissa_value: - Zpos Bexact_inverse_mantissa = 2 ^ (prec - 1). - Proof. -- assert (REC: forall n, Z.pos (nat_iter n xO xH) = 2 ^ (Z.of_nat n)). -+ assert (REC: forall n, Z.pos (nat_rect (fun _ => positive) xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)). - { induction n. reflexivity. -- simpl nat_iter. transitivity (2 * Z.pos (nat_iter n xO xH)). reflexivity. -+ simpl nat_rect. transitivity (2 * Z.pos (nat_rect (fun _ => positive) xH (fun _ => xO) n)). reflexivity. - rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. - change (2 ^ 1) with 2. ring. } - red in prec_gt_0_. -@@ -1015,12 +1015,12 @@ - Remark Bexact_inverse_mantissa_digits2_pos: - Z.pos (digits2_pos Bexact_inverse_mantissa) = prec. - Proof. -- assert (DIGITS: forall n, digits2_pos (nat_iter n xO xH) = Pos.of_nat (n+1)). -+ assert (DIGITS: forall n, digits2_pos (nat_rect _ xH (fun _ => xO) n) = Pos.of_nat (n+1)). - { induction n; simpl. auto. rewrite IHn. destruct n; auto. } - red in prec_gt_0_. - unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS. - rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega. -- destruct prec; try discriminate. rewrite NPeano.Nat.sub_add. -+ destruct prec; try discriminate. rewrite Nat.sub_add. - simpl. rewrite Pos2Nat.id. auto. - simpl. zify; omega. - Qed. -@@ -1039,7 +1039,7 @@ - - Program Definition Bexact_inverse (f: binary_float) : option binary_float := - match f with -- | B754_finite s m e B => -+ | B754_finite _ _ s m e B => - if positive_eq_dec m Bexact_inverse_mantissa then - let e' := -e - (prec - 1) * 2 in - if Z_le_dec emin e' then -@@ -1129,10 +1129,10 @@ - - Definition Bconv (conv_nan: bool -> nan_pl prec1 -> bool * nan_pl prec2) (md: mode) (f: binary_float1) : binary_float2 := - match f with -- | B754_nan s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl -- | B754_infinity s => B754_infinity _ _ s -- | B754_zero s => B754_zero _ _ s -- | B754_finite s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s -+ | B754_nan _ _ s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl -+ | B754_infinity _ _ s => B754_infinity _ _ s -+ | B754_zero _ _ s => B754_zero _ _ s -+ | B754_finite _ _ s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s - end. - - Theorem Bconv_correct: ---- a/Floats.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Floats.v 2015-05-29 13:44:10.285183004 -0400 -@@ -17,11 +17,11 @@ - (** Formalization of floating-point numbers, using the Flocq library. *) - - Require Import Coqlib. --Require Import Integers. --Require Import Fappli_IEEE. --Require Import Fappli_IEEE_bits. --Require Import Fappli_IEEE_extra. --Require Import Fcore. -+Require Import compcert.Integers. -+Require Import Flocq.Appli.Fappli_IEEE. -+Require Import Flocq.Appli.Fappli_IEEE_bits. -+Require Import compcert.Fappli_IEEE_extra. -+Require Import Flocq.Core.Fcore. - Require Import Program. - Require Archi. - -@@ -203,7 +203,7 @@ - (** Transform a Nan payload to a quiet Nan payload. *) - - Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 := -- Pos.lor pl (nat_iter 51 xO xH). -+ Pos.lor pl (iter_nat xO 51 xH). - Next Obligation. - destruct pl. - simpl. rewrite Z.ltb_lt in *. -@@ -239,12 +239,14 @@ - - Definition expand_pl (pl: nan_pl 24) : nan_pl 53. - Proof. -- refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _). -+ refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _); - abstract ( -- destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_pos; -- fold (Fcore_digits.digits2_pos x); -+ destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_rect, Fcore_digits.digits2_pos; -+ fold Fcore_digits.digits2_pos; - rewrite Z.ltb_lt in *; -- zify; omega). -+ zify; -+ omega -+ ). - Defined. - - Definition of_single_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53) := -@@ -257,7 +259,7 @@ - Proof. - refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _). - abstract ( -- destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter; -+ destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_rect; - rewrite Z.ltb_lt in *; - assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) = - (Fcore_digits.digits2_pos x - 1)%positive) -@@ -284,12 +286,12 @@ - - Definition binop_pl (x y: binary64) : bool*nan_pl 53 := - match x, y with -- | B754_nan s1 pl1, B754_nan s2 pl2 => -+ | B754_nan _ _ s1 pl1, B754_nan _ _ s2 pl2 => - if Archi.choose_binop_pl_64 s1 pl1 s2 pl2 - then (s2, transform_quiet_pl pl2) - else (s1, transform_quiet_pl pl1) -- | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) -- | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) -+ | B754_nan _ _ s1 pl1, _ => (s1, transform_quiet_pl pl1) -+ | _, B754_nan _ _ s2 pl2 => (s2, transform_quiet_pl pl2) - | _, _ => Archi.default_pl_64 - end. - -@@ -659,7 +661,11 @@ - rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned. - change (Int.unsigned ox8000_0000) with Int.half_modulus. - unfold sub. rewrite BofZ_minus. -- unfold of_int. f_equal. omega. -+ unfold of_int. -+ match goal with -+ |- _ _ _ _ _ ?a = _ _ _ _ _ ?b => cut (a = b); [ intro L; rewrite <- L; reflexivity | ] -+ end. -+ omega. - apply integer_representable_n; auto; smart_omega. - apply integer_representable_n; auto; smart_omega. - Qed. -@@ -768,7 +774,10 @@ - with ((xh - 2^20) * 2^32) - by (compute_this p; compute_this Int.half_modulus; ring). - unfold add. rewrite BofZ_plus. -- unfold of_long. f_equal. -+ unfold of_long. -+ match goal with -+ |- _ _ _ _ _ ?a = _ _ _ _ _ ?b => cut (a = b); [ intro L; rewrite <- L; reflexivity | ] -+ end. - rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''. - fold xh; fold xl. compute_this (two_p 32); ring. - apply integer_representable_n2p; auto. -@@ -925,7 +934,7 @@ - (** ** NaN payload manipulations *) - - Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 := -- Pos.lor pl (nat_iter 22 xO xH). -+ Pos.lor pl (Fcore_Zaux.iter_nat xO 22 xH). - Next Obligation. - destruct pl. - simpl. rewrite Z.ltb_lt in *. -@@ -949,12 +958,12 @@ - - Definition binop_pl (x y: binary32) : bool*nan_pl 24 := - match x, y with -- | B754_nan s1 pl1, B754_nan s2 pl2 => -+ | B754_nan _ _ s1 pl1, B754_nan _ _ s2 pl2 => - if Archi.choose_binop_pl_32 s1 pl1 s2 pl2 - then (s2, transform_quiet_pl pl2) - else (s1, transform_quiet_pl pl1) -- | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) -- | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) -+ | B754_nan _ _ s1 pl1, _ => (s1, transform_quiet_pl pl1) -+ | _, B754_nan _ _ s2 pl2 => (s2, transform_quiet_pl pl2) - | _, _ => Archi.default_pl_32 - end. - ---- a/Globalenvs.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Globalenvs.v 2015-05-29 13:54:44.390011625 -0400 -@@ -40,7 +40,7 @@ - Require Import Errors. - Require Import Maps. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Import Memory. ---- a/Integers.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Integers.v 2015-05-29 12:59:58.877875912 -0400 -@@ -3576,8 +3576,8 @@ - intros. - destruct (andb_prop _ _ H1). clear H1. - destruct (andb_prop _ _ H2). clear H2. -- exploit proj_sumbool_true. eexact H1. intro A; clear H1. -- exploit proj_sumbool_true. eexact H4. intro B; clear H4. -+ generalize (@proj_sumbool_true _ _ _ H1). intro A; clear H1. -+ generalize (@proj_sumbool_true _ _ _ H4). intro B; clear H4. - assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1). - destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto. - clear H3. ---- a/Intv.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Intv.v 2015-05-29 13:48:26.889520518 -0400 -@@ -248,7 +248,7 @@ - destruct H2. congruence. auto. - Qed. - Next Obligation. -- exists wildcard'0; split; auto. omega. -+ exists wildcard'; split; auto. omega. - Qed. - Next Obligation. - exists (hi - 1); split; auto. omega. ---- a/Memdata.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Memdata.v 2015-05-29 13:49:21.925592509 -0400 -@@ -19,7 +19,7 @@ - Require Import Coqlib. - Require Archi. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - ---- a/Memory.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Memory.v 2015-05-29 13:52:19.745824184 -0400 -@@ -33,7 +33,7 @@ - Require Import Maps. - Require Archi. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Export Memdata. -@@ -1505,7 +1505,8 @@ - try discriminate. - rewrite pred_dec_true. - decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. -- apply getN_setN_same. -+ apply getN_setN_same. -+ inv STORE; simpl. - red; eauto with mem. - Qed. - ---- a/Memtype.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Memtype.v 2015-05-29 13:50:31.365683146 -0400 -@@ -25,7 +25,7 @@ - - Require Import Coqlib. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - Require Import Values. - Require Import Memdata. ---- a/Smallstep.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Smallstep.v 2015-05-29 13:58:58.298338567 -0400 -@@ -24,7 +24,7 @@ - Require Import Coqlib. - Require Import Events. - Require Import Globalenvs. --Require Import Integers. -+Require Import compcert.Integers. - - Set Implicit Arguments. - ---- a/Values.v 2015-10-18 17:57:03.354368623 -0400 -+++ b/Values.v 2015-05-29 13:45:50.117314684 -0400 -@@ -18,7 +18,7 @@ - - Require Import Coqlib. - Require Import AST. --Require Import Integers. -+Require Import compcert.Integers. - Require Import Floats. - - Definition block : Type := positive. diff --git a/patches/interval.patch b/patches/interval.patch deleted file mode 100644 index de60122..0000000 --- a/patches/interval.patch +++ /dev/null @@ -1,97 +0,0 @@ -# VCFloat: A Unified Coq Framework for Verifying C Programs with -# Floating-Point Computations. Application to SAR Backprojection. -# -# Version 1.0 (2015-12-04) -# -# Copyright (C) 2015 Reservoir Labs Inc. -# All rights reserved. -# -# This file, which is part of VCFloat, is free software. You can -# redistribute it and/or modify it under the terms of CeCILL-C, -# version 1.0. A verbatim copy of CeCILL-C is included in -# cecill-c-1.0.txt. -# -# This file 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 LICENSE for -# more details about the use and redistribution of this file and the -# whole R-CoqLib library. -# -# This file is a modification of Coq-Interval version 1.1.0, which is -# Copyright (C) 2007-2015 Guillaume Melquiond. All rights -# reserved. See ACKS for more copyright and licensing information -# about Coq-Interval. -# -diff --git a/src/Interval_tactic.v b/src/Interval_tactic.v -index a4f5eec..1ed03b8 100644 ---- a/src/Interval_tactic.v -+++ b/src/Interval_tactic.v -@@ -436,7 +436,7 @@ Ltac xalgorithm_pre := - idtac - | |- (?a <> ?b)%R => - apply Rminus_not_eq -- | _ => fail 100 "Goal is not an inequality with floating-point bounds." -+ | _ => fail 1 "Goal is not an inequality with floating-point bounds." - end. - - Ltac xalgorithm_post lx := -@@ -587,7 +587,7 @@ Ltac get_bounds l prec := - | H: Rle x ?b |- _ => idtac - | H: Rle (Rabs x) ?b |- _ => idtac - end ; -- fail 100 "Atom" x "is neither a floating-point value nor bounded by floating-point values." -+ fail 3 "Atom" x "is neither a floating-point value nor bounded by floating-point values." - | _ => - constr:(A.Bproof x (I.bnd F.nan F.nan) (conj I I), @Some R x) - end -@@ -732,7 +732,7 @@ Ltac do_interval vars prec depth eval_tac := - vm_cast_no_check (refl_equal true) - end - end)) || -- fail 100 "Numerical evaluation failed to conclude. You may want to adjust some parameters.". -+ fail 0 "Numerical evaluation failed to conclude. You may want to adjust some parameters.". - - Ltac do_interval_eval bounds output formula prec depth n := - refine (interval_helper_evaluate bounds output formula prec n _). -@@ -750,7 +750,7 @@ Ltac tuple_to_list params l := - match params with - | pair ?a ?b => tuple_to_list a (b :: l) - | ?b => constr:(b :: l) -- | ?z => fail 100 "Unknown tactic parameter" z "." -+ | ?z => fail 1 "Unknown tactic parameter" z "." - end. - - Ltac do_interval_parse params := -@@ -762,20 +762,20 @@ Ltac do_interval_parse params := - | cons (i_bisect_diff ?x) ?t => aux (cons x nil) prec depth do_interval_bisect_diff t - | cons (i_bisect_taylor ?x ?d) ?t => aux (cons x nil) prec depth ltac:(do_interval_bisect_taylor d) t - | cons (i_depth ?d) ?t => aux vars prec d eval_tac t -- | cons ?h _ => fail 100 "Unknown tactic parameter" h "." -+ | cons ?h _ => fail 1 "Unknown tactic parameter" h "." - end in - aux (@nil R) 30%nat 15%nat do_interval_eval params. - - Ltac do_interval_generalize t b := - match eval vm_compute in (I.convert b) with -- | Inan => fail 100 "Nothing known about" t -+ | Inan => fail 1 "Nothing known about" t - | Ibnd ?l ?u => - match goal with - | |- ?P => - match l with - | Xnan => - match u with -- | Xnan => fail 100 "Nothing known about" t -+ | Xnan => fail 4 "Nothing known about" t - | Xreal ?u => refine ((_ : (t <= u)%R -> P) _) - end - | Xreal ?l => -@@ -836,7 +836,7 @@ Ltac do_interval_intro_parse t_ extend params_ := - | cons (i_bisect_diff ?x) ?t => aux (cons x nil) prec depth do_interval_intro_bisect_diff t - | cons (i_bisect_taylor ?x ?d) ?t => aux (cons x nil) prec depth ltac:(do_interval_intro_bisect_taylor d) t - | cons (i_depth ?d) ?t => aux vars prec d eval_tac t -- | cons ?h _ => fail 100 "Unknown tactic parameter" h "." -+ | cons ?h _ => fail 1 "Unknown tactic parameter" h "." - end in - aux (@nil R) 30%nat 5%nat do_interval_intro_eval params_. -