Resynchronize the LICENSE file and the license headers in individual files (#45)

Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file.  OVer the years those two markings got inconsistent.

This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.

Some build-related files were dual-licensed but some others were not.  Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v

Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed.  Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/

17 files changed, 60 insertions, 8 deletions

diff --git a/LICENSE b/LICENSE
index 2353de49..5c7d7294 100644
--- a/LICENSE
+++ b/LICENSE
@@ -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.     *)
 (*                                                                     *)
 (* *********************************************************************)
diff --git a/configure b/configure
index cf0582ac..13d9c57a 100755
--- a/configure
+++ b/configure
@@ -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.     *)
 (*                                                                     *)
 (* *********************************************************************)