VCFloat, version 1.0: initial release

.gitignore

@@ -0,0 +1,18 @@
+dir-locals
+Makefile
+*.aux
+.dir-locals.el
+*.glob
+*.v.d
+*.vo
+run-coqide.sh
+*~
+*.tgz
+*.tar.gz
+rcoqlib*/*
+compcert*/*
+ssreflect*/*
+mathcomp*/*
+flocq*/*
+interval*/*
+coqopts

LICENSE

@@ -0,0 +1,49 @@
+
+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 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 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
+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.

README

@@ -0,0 +1,108 @@
+VCFloat: A Unified Coq Framework for Verifying C Programs with
+Floating-Point Computations
+
+Version 1.0 (2015-12-04)
+
+Copyright (C) 2015 Reservoir Labs Inc.
+All rights reserved.
+
+patches/interval.patch is distributed under CeCILL-C, version 1.0. All
+other files of this library are distributed under the GNU General
+Public License, version 3.0, or (at your option) any later
+version. See LICENSE for more legal information on use and
+distribution of VCFloat.
+
+
+For more technical information on VCFloat, you can read Sections 1 to
+4 of our paper published at ACM/SIGPLAN Certified Programs and Proofs
+(CPP) 2016:
+
+Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
+Lethin.
+A Unified Coq Framework for Verifying C Programs with Floating-Point
+Computations
+
+
+Summary of directories (each of which corresponds to its logical path
+with the same names where each path separator is replaced with . ):
+
+  vcfloat/cverif: Verification of CompCert Clight programs (separation
+  logic, etc.)
+
+  vcfloat: VCFloat reasoning framework and tactic
+
+
+Most interesting files:
+
+  vcfloat/FPLang.v: VCFloat floating-point and annotated
+  floating-point calculus
+
+  vcfloat/FPLangOpt.v: further properties about VCFloat
+
+  vcfloat/Clight2FP.v: C to unannotated VCFloat
+
+  vcfloat/Clight2FPOpt.v: VCFloat annotation tactic
+
+
+VCFloat requires Coq 8.5beta2.
+
+
+VCFloat depends on the following further external libraries, which are
+automatically downloaded from their official sources and built during
+VCFloat's building process:
+
+- Reservoir Labs Inc. R-CoqLib version 1.0 (from Reservoir Labs'
+  GitHub at https://github.com/reservoirlabs/rcoqlib )
+
+- CompCert 2.4 (from AbsInt's GitHub at
+  https://github.com/AbsInt/CompCert.git , commit 5dd15440). VCFloat
+  contains a patch from this commit (patches/compcert.patch),
+  distributed under the GNU General Public License, version 3.0 or (at
+  your option) any later version.
+
+- Ssreflect 1.5 (from its official website at
+  http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz )
+
+- Mathematical Components (MathComp) 1.5 (from its official website at
+  http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz )
+
+- Flocq 2.4.0 (from INRIA GForge at
+  https://gforge.inria.fr/git/flocq/flocq.git , commit bcbcde24)
+
+- Coq-Interval 2.0.0 (from INRIA GForge at
+  https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git
+  , commit 81f1f918). VCFloat contains a patch from this commit
+  (patches/interval.patch), distributed under CeCILL-C, version 1.0.
+
+See ACKS for copyright and licensing information about those external
+libraries.
+
+
+Usage: assuming that you already have a standard installation of Coq
+8.5beta2, GNU make, GNU autoconf, GNU automake, and git.
+
+  0. Fetch the external libraries mentioned above, by running the
+     following automatic script:
+
+     ./get_external_libs.sh
+
+     You can provide any further options that you want passed to the
+     `make' commands for Ssreflect and MathComp (e.g. -j)
+
+  1. Configure, by:
+
+     ./configure
+
+  2. Build, by:
+
+     make
+
+  After building, you do not need to move the files anywhere else
+  (and, by the way, `make install' does not work). The build system
+  automatically generates a ./run-coqide.sh script to edit the sources
+  with CoqIDE (if installed on your system), as well as local load
+  path configuration files for Emacs+ProofGeneral (if installed on
+  your system). If you want to compile code against VCFloat, you can
+  have a look at the autogenerated `coqopts' file, to grab the load
+  path options to pass to Coq and its relevant tools (coqc,
+  coq_makefile, etc.)