diff options
| -rw-r--r-- | LICENSE | 21 | ||||
| -rw-r--r-- | Makefile.menhir | 3 | ||||
| -rw-r--r-- | arm/extractionMachdep.v | 3 | ||||
| -rw-r--r-- | backend/Json.ml (renamed from lib/Json.ml) | 0 | ||||
| -rw-r--r-- | backend/JsonAST.ml (renamed from lib/JsonAST.ml) | 0 | ||||
| -rw-r--r-- | backend/JsonAST.mli (renamed from lib/JsonAST.mli) | 0 | ||||
| -rw-r--r-- | common/PrintAST.ml | 3 | ||||
| -rw-r--r-- | common/Switchaux.ml | 3 | ||||
| -rwxr-xr-x | configure | 3 | ||||
| -rw-r--r-- | cparser/handcrafted.messages | 3 | ||||
| -rw-r--r-- | extraction/extraction.v | 3 | ||||
| -rw-r--r-- | lib/Lattice.v | 1 | ||||
| -rw-r--r-- | lib/Ordered.v | 1 | ||||
| -rw-r--r-- | lib/Readconfig.mll | 15 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 3 | ||||
| -rw-r--r-- | riscV/extractionMachdep.v | 3 | ||||
| -rw-r--r-- | x86/extractionMachdep.v | 3 |
17 files changed, 60 insertions, 8 deletions
@@ -26,26 +26,35 @@ option) any later version: all files in the common/ directory + cfrontend/C2C.ml cfrontend/Clight.v cfrontend/ClightBigstep.v cfrontend/Cop.v + cfrontend/CPragmas.ml cfrontend/Csem.v cfrontend/Cstrategy.v cfrontend/Csyntax.v cfrontend/Ctypes.v cfrontend/Ctyping.v + cfrontend/PrintClight.ml + cfrontend/PrintCsyntax.ml backend/Cminor.v - - arm/Archi.v - ia32/Archi.v - powerpc/Archi.v + backend/PrintCminor.ml all files in the cparser/ directory all files in the exportclight/ directory + the Archi.v, CBuiltins.ml, and extractionMachdep.v files + in directories arm, powerpc, riscV, x86, x86_32, x86_64 + + extraction/extraction.v + + configure Makefile + Makefile.extr + Makefile.menhir A copy of the GNU General Public License version 2 is included below. The choice between the two licenses for the files listed above is left @@ -56,13 +65,13 @@ Public License. The files contained in the flocq/ directory and its subdirectories are taken from the Flocq project, http://flocq.gforge.inria.fr/ -These files are Copyright 2010-2013 INRIA and distributed under the +These files are Copyright 2010-2017 INRIA and distributed under the terms of the GNU Lesser General Public Licence, either version 3 of the licence, or (at your option) any later version. A copy of the GNU Lesser General Public Licence version 3 is included below. The files contained in the runtime/ directory and its subdirectories -are Copyright 2013-2014 INRIA and distributed under the terms of the BSD +are Copyright 2013-2017 INRIA and distributed under the terms of the BSD 3-clause license, included below. ---------------------------------------------------------------------- diff --git a/Makefile.menhir b/Makefile.menhir index 1530536f..98bfc750 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -6,6 +6,9 @@ # # # Copyright Institut National de Recherche en Informatique et en # # Automatique. All rights reserved. This file is distributed # +# under the terms of the GNU General Public License as published by # +# the Free Software Foundation, either version 2 of the License, or # +# (at your option) any later version. This file is also distributed # # under the terms of the INRIA Non-Commercial License Agreement. # # # ####################################################################### diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index 9d243413..a82cf749 100644 --- a/arm/extractionMachdep.v +++ b/arm/extractionMachdep.v @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/lib/Json.ml b/backend/Json.ml index b8f66c08..b8f66c08 100644 --- a/lib/Json.ml +++ b/backend/Json.ml diff --git a/lib/JsonAST.ml b/backend/JsonAST.ml index 73cac31e..73cac31e 100644 --- a/lib/JsonAST.ml +++ b/backend/JsonAST.ml diff --git a/lib/JsonAST.mli b/backend/JsonAST.mli index c6fd80c9..c6fd80c9 100644 --- a/lib/JsonAST.mli +++ b/backend/JsonAST.mli diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 883d101a..e477957a 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 35f58aa7..4035e299 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -8,6 +8,9 @@ # # # Copyright Institut National de Recherche en Informatique et en # # Automatique. All rights reserved. This file is distributed # +# under the terms of the GNU General Public License as published by # +# the Free Software Foundation, either version 2 of the License, or # +# (at your option) any later version. This file is also distributed # # under the terms of the INRIA Non-Commercial License Agreement. # # # ####################################################################### diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages index 0af01a61..567fdd6b 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -7,6 +7,9 @@ # # # Copyright Institut National de Recherche en Informatique et en # # Automatique. All rights reserved. This file is distributed # +# under the terms of the GNU General Public License as published by # +# the Free Software Foundation, either version 2 of the License, or # +# (at your option) any later version. This file is also distributed # # under the terms of the INRIA Non-Commercial License Agreement. # # # ####################################################################### diff --git a/extraction/extraction.v b/extraction/extraction.v index c5751e2b..a47a7237 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/lib/Lattice.v b/lib/Lattice.v index b7ae837b..85fc03f3 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -6,7 +6,6 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) diff --git a/lib/Ordered.v b/lib/Ordered.v index c333cc50..bcf24cbd 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -6,7 +6,6 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index 6cb3409d..e71c8fb7 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + { (* Recording key=val bindings *) diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index b5ae048d..7482435f 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v index 81cfc88c..c9a1040a 100644 --- a/riscV/extractionMachdep.v +++ b/riscV/extractionMachdep.v @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v index 14cb6447..a29553e8 100644 --- a/x86/extractionMachdep.v +++ b/x86/extractionMachdep.v @@ -6,6 +6,9 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) |