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/

6 files changed, 15 insertions, 251 deletions

diff --git a/lib/Json.ml b/lib/Json.ml
deleted file mode 100644
index b8f66c08..00000000
--- a/lib/Json.ml
+++ /dev/null
@@ -1,109 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
-(*                                                                     *)
-(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
-(*  is distributed under the terms of the INRIA Non-Commercial         *)
-(*  License Agreement.                                                 *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Format
-open Camlcoq
-
-
-(* Simple functions for JSON printing *)
-
-(* Print a string as json string *)
-let pp_jstring oc s =
-  fprintf oc "\"%s\"" s
-
-(* Print a bool as json bool *)
-let pp_jbool oc = fprintf oc "%B"
-
-(* Print an int as json int *)
-let pp_jint oc = fprintf oc "%d"
-
-(* Print an int32 as json int *)
-let pp_jint32 oc = fprintf oc "%ld"
-
-(* Print optional value *)
-let pp_jopt pp_elem oc = function
-  | None -> output_string oc "null"
-  | Some i -> pp_elem oc i
-
-(* Print opening and closing curly braces for json dictionaries *)
-let pp_jobject_start pp =
-  fprintf pp "@[<v 1>{"
-
-let pp_jobject_end pp =
-  fprintf pp "@;<0 -1>}@]"
-
-(* Print a member of a json dictionary *)
-let pp_jmember ?(first=false) pp name pp_mem mem =
-  let sep = if first then "" else "," in
-  fprintf pp "%s@ \"%s\": %a" sep name pp_mem mem
-
-(* Print singleton object *)
-let pp_jsingle_object pp name pp_mem mem =
-  pp_jobject_start pp;
-  pp_jmember ~first:true pp name pp_mem mem;
-  pp_jobject_end pp
-
-(* Print a list as json array *)
-let pp_jarray elem pp l =
-  match l with
-  | []  ->  fprintf pp "[]";
-  | hd::tail ->
-    fprintf pp "@[<v 1>[";
-    fprintf pp "%a" elem hd;
-    List.iter (fun l -> fprintf pp ",@ %a" elem l) tail;
-  fprintf pp "@;<0 -1>]@]"
-
-(* Helper functions for printing coq integer and floats *)
-let pp_int pp i =
-  fprintf pp "%ld" (camlint_of_coqint i)
-
-let pp_int64 pp i =
-  fprintf pp "%Ld" (camlint64_of_coqint i)
-
-let pp_float32 pp f =
-  fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f))
-
-let pp_float64 pp f =
-  fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f))
-
-let pp_z pp z =
-  fprintf pp "%s" (Z.to_string z)
-
-(* Helper functions for printing assembler constructs *)
-let pp_atom pp a =
-  pp_jstring pp (extern_atom a)
-
-let pp_atom_constant pp a =
-  pp_jsingle_object pp "Atom" pp_atom a
-
-let pp_int_constant pp i =
-  pp_jsingle_object pp "Integer" pp_int i
-
-let pp_float64_constant pp f =
-  pp_jsingle_object pp "Float" pp_float64 f
-
-let pp_float32_constant pp f =
-  pp_jsingle_object pp "Float" pp_float32 f
-
-let id = ref 0
-
-let next_id () =
-  let tmp = !id in
-  incr id;
-  tmp
-
-let reset_id () =
-  id := 0
-
-let pp_id_const pp () =
-  let i = next_id () in
-  pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i
diff --git a/lib/JsonAST.ml b/lib/JsonAST.ml
deleted file mode 100644
index 73cac31e..00000000
--- a/lib/JsonAST.ml
+++ /dev/null
@@ -1,124 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
-(*          Michael Schmidt, AbsInt Angewandte Informatik GmbH         *)
-(*                                                                     *)
-(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
-(*  is distributed under the terms of the INRIA Non-Commercial         *)
-(*  License Agreement.                                                 *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Asm
-open AST
-open C2C
-open Json
-open Format
-open Sections
-
-
-let pp_storage pp static =
-  pp_jstring pp (if static then "Static" else "Extern")
-
-let pp_section pp sec =
-  let pp_simple name =
-    pp_jsingle_object pp "Section Name" pp_jstring name
-  and pp_complex name init =
-    pp_jobject_start pp;
-    pp_jmember ~first:true pp "Section Name" pp_jstring name;
-    pp_jmember pp "Init" pp_jbool init;
-    pp_jobject_end pp in
-  match sec with
-  | Section_text -> pp_simple "Text"
-  | Section_data init -> pp_complex "Data" init
-  | Section_small_data init -> pp_complex "Small Data" init
-  | Section_const init -> pp_complex "Const" init
-  | Section_small_const init -> pp_complex "Small Const" init
-  | Section_string -> pp_simple "String"
-  | Section_literal -> pp_simple "Literal"
-  | Section_jumptable -> pp_simple "Jumptable"
-  | Section_user (s,w,e) ->
-    pp_jobject_start pp;
-    pp_jmember ~first:true pp "Section Name" pp_jstring s;
-    pp_jmember pp "Writable" pp_jbool w;
-    pp_jmember pp "Executable" pp_jbool e;
-    pp_jobject_end pp
-  | Section_debug_info _
-  | Section_debug_abbrev
-  | Section_debug_line _
-  | Section_debug_loc
-  | Section_debug_ranges
-  | Section_debug_str
-  | Section_ais_annotation -> () (* There should be no info in the debug sections *)
-
-let pp_int_opt pp = function
-  | None -> fprintf pp "0"
-  | Some i -> fprintf pp "%d" i
-
-let pp_fundef pp_inst pp (name,fn) =
-  let alignment = atom_alignof name
-  and inline = atom_inline name = Inline
-  and static = atom_is_static name
-  and c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in
-  pp_jobject_start pp;
-  pp_jmember ~first:true pp "Fun Name" pp_atom name;
-  pp_jmember pp "Fun Storage Class" pp_storage static;
-  pp_jmember pp "Fun Alignment" pp_int_opt alignment;
-  pp_jmember pp "Fun Section Code" pp_section c_section;
-  pp_jmember pp "Fun Section Literals" pp_section l_section;
-  pp_jmember pp "Fun Section Jumptable" pp_section j_section;
-  pp_jmember pp "Fun Inline" pp_jbool inline;
-  pp_jmember pp "Fun Code" pp_inst fn.fn_code;
-  pp_jobject_end pp
-
-let pp_init_data pp = function
-  | Init_int8 ic -> pp_jsingle_object pp "Init_int8" pp_int ic
-  | Init_int16 ic -> pp_jsingle_object pp "Init_int16" pp_int ic
-  | Init_int32 ic -> pp_jsingle_object pp "Init_int32" pp_int ic
-  | Init_int64 lc -> pp_jsingle_object pp "Init_int64" pp_int64 lc
-  | Init_float32 f -> pp_jsingle_object pp "Init_float32" pp_float32 f
-  | Init_float64 f -> pp_jsingle_object pp "Init_float64" pp_float64 f
-  | Init_space z -> pp_jsingle_object pp "Init_space" pp_z z
-  | Init_addrof (p,i) ->
-    let pp_addr_of pp (p,i) =
-      pp_jobject_start pp;
-      pp_jmember ~first:true pp "Addr" pp_atom p;
-      pp_jmember  pp "Offset" pp_int i;
-      pp_jobject_end pp  in
-    pp_jsingle_object pp "Init_addrof" pp_addr_of (p,i)
-
-let pp_vardef pp (name,v) =
-  let alignment = atom_alignof name
-  and static = atom_is_static name
-  and section = match  (atom_sections name) with [s] -> s | _ -> assert false in(* Should only have one section *)
-  pp_jobject_start pp;
-  pp_jmember ~first:true pp "Var Name" pp_atom name;
-  pp_jmember pp "Var Readonly" pp_jbool v.gvar_readonly;
-  pp_jmember pp "Var Volatile" pp_jbool v.gvar_volatile;
-  pp_jmember pp "Var Storage Class" pp_storage static;
-  pp_jmember pp "Var Alignment" pp_int_opt alignment;
-  pp_jmember pp "Var Section" pp_section section;
-  pp_jmember pp "Var Init" (pp_jarray pp_init_data) v.gvar_init;
-  pp_jobject_end pp
-
-let pp_program pp pp_inst prog =
-  let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
-      match def with
-      | Gfun (Internal f) ->
-        if not (atom_is_iso_inline_definition ident) then
-          vars,(ident,f)::funs
-        else
-          vars,funs
-      | Gvar v -> (ident,v)::vars,funs
-      | _ -> vars,funs) ([],[]) prog.prog_defs in
-  pp_jobject_start pp;
-  pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;
-  pp_jmember pp "Functions" (pp_jarray (pp_fundef pp_inst)) prog_funs;
-  pp_jobject_end pp
-
-let pp_mnemonics pp mnemonic_names =
-  let mnemonic_names = List.sort (String.compare) mnemonic_names in
-  let new_line pp () = pp_print_string pp "\n" in
-  pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
diff --git a/lib/JsonAST.mli b/lib/JsonAST.mli
deleted file mode 100644
index c6fd80c9..00000000
--- a/lib/JsonAST.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
-(*                                                                     *)
-(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
-(*  is distributed under the terms of the INRIA Non-Commercial         *)
-(*  License Agreement.                                                 *)
-(*                                                                     *)
-(* *********************************************************************)
-
-
-
-val pp_program : Format.formatter -> (Format.formatter  -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
-val pp_mnemonics : Format.formatter -> string list -> unit
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 *)