From 9ccb6a24541b3a06b600a70791950eecd46d1806 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jan 2018 09:50:10 +0100 Subject: 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/ --- LICENSE | 21 +++++--- Makefile.menhir | 3 ++ arm/extractionMachdep.v | 3 ++ backend/Json.ml | 109 +++++++++++++++++++++++++++++++++++++ backend/JsonAST.ml | 124 +++++++++++++++++++++++++++++++++++++++++++ backend/JsonAST.mli | 16 ++++++ common/PrintAST.ml | 3 ++ common/Switchaux.ml | 3 ++ configure | 3 ++ cparser/handcrafted.messages | 3 ++ extraction/extraction.v | 3 ++ lib/Json.ml | 109 ------------------------------------- lib/JsonAST.ml | 124 ------------------------------------------- lib/JsonAST.mli | 16 ------ lib/Lattice.v | 1 - lib/Ordered.v | 1 - lib/Readconfig.mll | 15 ++++++ powerpc/extractionMachdep.v | 3 ++ riscV/extractionMachdep.v | 3 ++ x86/extractionMachdep.v | 3 ++ 20 files changed, 309 insertions(+), 257 deletions(-) create mode 100644 backend/Json.ml create mode 100644 backend/JsonAST.ml create mode 100644 backend/JsonAST.mli delete mode 100644 lib/Json.ml delete mode 100644 lib/JsonAST.ml delete mode 100644 lib/JsonAST.mli 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/backend/Json.ml b/backend/Json.ml new file mode 100644 index 00000000..b8f66c08 --- /dev/null +++ b/backend/Json.ml @@ -0,0 +1,109 @@ +(* *********************************************************************) +(* *) +(* 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 "@[{" + +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 "@[["; + 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/backend/JsonAST.ml b/backend/JsonAST.ml new file mode 100644 index 00000000..73cac31e --- /dev/null +++ b/backend/JsonAST.ml @@ -0,0 +1,124 @@ +(* *********************************************************************) +(* *) +(* 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/backend/JsonAST.mli b/backend/JsonAST.mli new file mode 100644 index 00000000..c6fd80c9 --- /dev/null +++ b/backend/JsonAST.mli @@ -0,0 +1,16 @@ +(* *********************************************************************) +(* *) +(* 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/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/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 "@[{" - -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 "@[["; - 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 *) 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. *) (* *) (* *********************************************************************) -- cgit