From e6744b2bf013158c5158580107530eee65b53b35 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 19 Apr 2021 11:26:31 +0200 Subject: Ensure compatibility with future versions of MenhirLib After Menhir version 20210310, the `Fail_pr` constructor of the `parse_result` type becomes `Fail_pr_full` with two extra arguments. This PR enables CompCert to handle both versions of the `parse_result` type in MenhirLib. --- cparser/Parse.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'cparser') diff --git a/cparser/Parse.ml b/cparser/Parse.ml index d9f9aa1c..3ed193f9 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -72,12 +72,13 @@ let preprocessed_file transfs name sourcefile = (fun () -> Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) () with - | Parser.MenhirLibParser.Inter.Fail_pr -> - (* Theoretically impossible : implies inconsistencies - between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" - | Parser.MenhirLibParser.Inter.Timeout_pr -> assert false - | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast) in + | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast + | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending + on the version of Menhir. + Fail_pr{,_full} means that there's an inconsistency + between the pre-parser and the parser. + Timeout_pr means that we ran for 2^50 steps. *) + Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing") in let p1 = Timing.time "Elaboration" Elab.elab_file ast in Diagnostics.check_errors (); Timing.time2 "Emulations" transform_program t p1 name in -- cgit From 45af10b3ac30f8e4f5904824259b04df17e1c6b1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 19 Apr 2021 13:36:23 +0200 Subject: Refactor cparser/Parse.ml - Use pipeline notation `|>` for legibility and better GC behavior (in bytecode at least). - Introduce auxiliary functions. - Remove useless function parameters. - Fix the timing of the "Emulations" pass (because of an extra parameter, what was timed took zero time). --- cparser/Parse.ml | 60 +++++++++++++++++++++++++++----------------------------- 1 file changed, 29 insertions(+), 31 deletions(-) (limited to 'cparser') diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 3ed193f9..542ed0d7 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -17,7 +17,7 @@ module CharSet = Set.Make(struct type t = char let compare = compare end) -let transform_program t p name = +let transform_program t p = let run_pass pass flag p = if CharSet.mem flag t then begin let p = pass p in @@ -26,12 +26,12 @@ let transform_program t p name = end else p in - let p1 = (run_pass StructPassing.program 's' - (run_pass PackedStructs.program 'p' - (run_pass Unblock.program 'b' - (run_pass Bitfields.program 'f' - p)))) in - Rename.program p1 + p + |> run_pass Bitfields.program 'f' + |> run_pass Unblock.program 'b' + |> run_pass PackedStructs.program 'p' + |> run_pass StructPassing.program 's' + |> Rename.program let parse_transformations s = let t = ref CharSet.empty in @@ -52,35 +52,33 @@ let read_file sourcefile = close_in ic; text +let parse_string name text = + let log_fuel = Camlcoq.Nat.of_int 50 in + match + Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text) + with + | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> + (ast: Cabs.definition list) + | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending + on the version of Menhir. + Fail_pr{,_full} means that there's an inconsistency + between the pre-parser and the parser. + Timeout_pr means that we ran for 2^50 steps. *) + Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" + let preprocessed_file transfs name sourcefile = Diagnostics.reset(); + let check_errors x = + Diagnostics.check_errors(); x in (* Reading the whole file at once may seem costly, but seems to be the simplest / most robust way of accessing the text underlying a range of positions. This is used when printing an error message. Plus, I note that reading the whole file into memory leads to a speed increase: "make -C test" speeds up by 3 seconds out of 40 on my machine. *) - let text = read_file sourcefile in - let p = - let t = parse_transformations transfs in - let log_fuel = Camlcoq.Nat.of_int 50 in - let ast : Cabs.definition list = - (match Timing.time "Parsing" - (* The call to Lexer.tokens_stream results in the pre - parsing of the entire file. This is non-negligeabe, - so we cannot use Timing.time2 *) - (fun () -> - Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) () - with - | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast - | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending - on the version of Menhir. - Fail_pr{,_full} means that there's an inconsistency - between the pre-parser and the parser. - Timeout_pr means that we ran for 2^50 steps. *) - Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing") in - let p1 = Timing.time "Elaboration" Elab.elab_file ast in - Diagnostics.check_errors (); - Timing.time2 "Emulations" transform_program t p1 name in - Diagnostics.check_errors(); - p + read_file sourcefile + |> Timing.time2 "Parsing" parse_string name + |> Timing.time "Elaboration" Elab.elab_file + |> check_errors + |> Timing.time2 "Emulations" transform_program (parse_transformations transfs) + |> check_errors -- cgit From 0877e32e0bb836a1b3b34d678f0c68f852c55ff3 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Tue, 20 Apr 2021 02:02:30 +1000 Subject: Elab bitfields: check size of type <=32bit rather than checking rank (#387) When desugaring a bitfield, allow any integral type that is 32 bits or smaller. Previously this was checking the rank of the type rather than the size. This rank check caused issues with standard headers that declare `uint32_t` to be an `unsigned long` rather than an `unsigned int`. Here, any bitfields declared as `uint32_t` were failing to compile even though they are still actually 32 bits. Co-authored-by: Amos Robinson --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 25e4a980..05717d97 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1001,7 +1001,7 @@ and elab_field_group env = function | TInt(ik, _) -> ik | TEnum(_, _) -> enum_ikind | _ -> ILongLong (* trigger next error message *) in - if integer_rank ik > integer_rank IInt then begin + if sizeof_ikind ik > sizeof_ikind IInt then begin error loc "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id; None,env -- cgit From 38b0babd5a642cea8912524debc63edc67fda08b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 2 May 2021 17:14:38 +0200 Subject: Fix spurious error on initialization of struct with flexible array member The following is correct but was causing a "wrong type for array initializer" fatal error. ``` struct s { int n; int d[]; }; void f(void) { struct s x = {0}; } ``` Co-authored-by: Michael Schmidt --- cparser/Unblock.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'cparser') diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index d25f70c6..8530ae01 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -31,6 +31,9 @@ let rec local_initializer env path init k = let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) + (* We accept empty array initializer for flexible array members, which + has size zero *) + | TArray(ty_elt, None, _) when il = [] -> (ty_elt, 0L) | _ -> Diagnostics.fatal_error Diagnostics.no_loc "wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin -- cgit From 320c55590cc30d4ef5b2c1a226f0f940a6bdb445 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 25 Apr 2021 13:57:47 +0200 Subject: Support __builtin_unreachable Not yet used for optimizations. --- cparser/Cflow.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index cc257189..8a2a3fe4 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -23,8 +23,12 @@ open Cutil module StringSet = Set.Make(String) (* Functions declared noreturn by the standard *) +(* We also add our own "__builtin_unreachable" function because, currently, + it is difficult to attach attributes to a built-in function. *) + let std_noreturn_functions = - ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"] + ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"; + "__builtin_unreachable"] (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. -- cgit From 1f35599abe1b82f565a9a1b1ee03f60df362f22d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 2 May 2021 19:19:12 +0200 Subject: Fix evaluation order in emulation of bitfield assignment A bitfield assignment `x.b = f()` is expanded into a read-modify-write on `x.carrier`. Wrong results can occur if `x.carrier` is read before the call to `f()`, and `f` itself modifies a bitfield with the same carrier `x.carrier`. In this temporary fix, we play on the evaluation order implemented by the SimplExpr pass of CompCert (left-to-right for side-effecting subexpression) to make sure the read part of the read-modify-write sequence occurs after the evaluation of the right-hand side. More substantial fixes will be considered later. Fixes: #395 --- cparser/Bitfields.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cparser') diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 7a00f719..6d4050f1 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -267,7 +267,7 @@ let bitfield_extract env bf carrier = unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) { unsigned int mask = ((1U << sz) - 1) << ofs; - return (x & ~mask) | ((y << ofs) & mask); + return ((y << ofs) & mask) | (x & ~mask); } If the bitfield is of type _Bool, the new value (y above) must be converted @@ -284,7 +284,7 @@ let bitfield_assign env bf carrier newval = eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in let newval_masked = ebinint env Oand newval_shifted msk and oldval_masked = ebinint env Oand carrier notmsk in - ebinint env Oor oldval_masked newval_masked + ebinint env Oor newval_masked oldval_masked (* Initialize a bitfield *) -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- cparser/Bitfields.ml | 9 +++++---- cparser/Bitfields.mli | 9 +++++---- cparser/C.mli | 9 +++++---- cparser/Cabs.v | 9 +++++---- cparser/Cabshelper.ml | 9 +++++---- cparser/Ceval.ml | 9 +++++---- cparser/Ceval.mli | 9 +++++---- cparser/Cflow.ml | 9 +++++---- cparser/Cflow.mli | 9 +++++---- cparser/Checks.ml | 9 +++++---- cparser/Checks.mli | 9 +++++---- cparser/Cleanup.ml | 9 +++++---- cparser/Cleanup.mli | 9 +++++---- cparser/Cprint.ml | 9 +++++---- cparser/Cprint.mli | 9 +++++---- cparser/Cutil.ml | 9 +++++---- cparser/Cutil.mli | 9 +++++---- cparser/Diagnostics.ml | 9 +++++---- cparser/Diagnostics.mli | 9 +++++---- cparser/Elab.ml | 9 +++++---- cparser/Elab.mli | 9 +++++---- cparser/Env.ml | 9 +++++---- cparser/Env.mli | 9 +++++---- cparser/ErrorReports.ml | 9 +++++---- cparser/ErrorReports.mli | 9 +++++---- cparser/ExtendedAsm.ml | 9 +++++---- cparser/GCC.ml | 9 +++++---- cparser/GCC.mli | 9 +++++---- cparser/Lexer.mll | 9 +++++---- cparser/Machine.ml | 9 +++++---- cparser/Machine.mli | 9 +++++---- cparser/PackedStructs.ml | 9 +++++---- cparser/Parse.ml | 9 +++++---- cparser/Parse.mli | 9 +++++---- cparser/Parser.vy | 9 +++++---- cparser/Rename.ml | 9 +++++---- cparser/Rename.mli | 9 +++++---- cparser/StructPassing.ml | 9 +++++---- cparser/StructPassing.mli | 9 +++++---- cparser/Transform.ml | 9 +++++---- cparser/Transform.mli | 9 +++++---- cparser/Unblock.ml | 9 +++++---- cparser/Unblock.mli | 9 +++++---- cparser/deLexer.ml | 9 +++++---- cparser/handcrafted.messages | 9 +++++---- cparser/pre_parser.mly | 9 +++++---- cparser/pre_parser_aux.ml | 9 +++++---- cparser/pre_parser_aux.mli | 9 +++++---- 48 files changed, 240 insertions(+), 192 deletions(-) (limited to 'cparser') diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 6d4050f1..ad6e1696 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Bitfields.mli b/cparser/Bitfields.mli index 45899a46..3ac42495 100644 --- a/cparser/Bitfields.mli +++ b/cparser/Bitfields.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/C.mli b/cparser/C.mli index 15717565..763a9277 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cabs.v b/cparser/Cabs.v index ff046cba..accb95a0 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cabshelper.ml b/cparser/Cabshelper.ml index 7cffef08..36f67283 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Ceval.ml b/cparser/Ceval.ml index ecf83779..14f61e06 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Ceval.mli b/cparser/Ceval.mli index 32a0ed91..5b9bb0d7 100644 --- a/cparser/Ceval.mli +++ b/cparser/Ceval.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cflow.ml b/cparser/Cflow.ml index 8a2a3fe4..061e958e 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cflow.mli b/cparser/Cflow.mli index 0de245ae..8348b37e 100644 --- a/cparser/Cflow.mli +++ b/cparser/Cflow.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Checks.ml b/cparser/Checks.ml index 17caf19a..507488f2 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Checks.mli b/cparser/Checks.mli index cfd7b04d..08ce4e9a 100644 --- a/cparser/Checks.mli +++ b/cparser/Checks.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cleanup.ml b/cparser/Cleanup.ml index 63ac8ac1..62b00e04 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cleanup.mli b/cparser/Cleanup.mli index 818a51bc..c469936a 100644 --- a/cparser/Cleanup.mli +++ b/cparser/Cleanup.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cprint.ml b/cparser/Cprint.ml index 9aeec421..93377989 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cprint.mli b/cparser/Cprint.mli index be7ce029..01175d36 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cutil.ml b/cparser/Cutil.ml index 3467c092..2dcf193d 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Cutil.mli b/cparser/Cutil.mli index 2ddee78c..17eb2207 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Diagnostics.ml b/cparser/Diagnostics.ml index 86a5e522..483b0376 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Diagnostics.mli b/cparser/Diagnostics.mli index 0f0a0ea5..1210353f 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Elab.ml b/cparser/Elab.ml index 05717d97..a5b87e2e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Elab.mli b/cparser/Elab.mli index 59c5efc1..bca4f74d 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Env.ml b/cparser/Env.ml index 00806be1..7918c31f 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Env.mli b/cparser/Env.mli index 589a76c7..7c1096cf 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/ErrorReports.ml b/cparser/ErrorReports.ml index e8f0bee5..ac1e17ac 100644 --- a/cparser/ErrorReports.ml +++ b/cparser/ErrorReports.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/ErrorReports.mli b/cparser/ErrorReports.mli index dbaba5ff..c2160b49 100644 --- a/cparser/ErrorReports.mli +++ b/cparser/ErrorReports.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index df2da2a2..d34dd654 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/GCC.ml b/cparser/GCC.ml index 458e51d3..31385b45 100644 --- a/cparser/GCC.ml +++ b/cparser/GCC.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/GCC.mli b/cparser/GCC.mli index f26d12df..0163c98e 100644 --- a/cparser/GCC.mli +++ b/cparser/GCC.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Lexer.mll b/cparser/Lexer.mll index bce0e504..94e490ca 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Machine.ml b/cparser/Machine.ml index 8de4ed07..c47ec594 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Machine.mli b/cparser/Machine.mli index aa99f1aa..f9d347b9 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/PackedStructs.ml b/cparser/PackedStructs.ml index 4c70c7ae..6bea4b92 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Parse.ml b/cparser/Parse.ml index 542ed0d7..d88d439b 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Parse.mli b/cparser/Parse.mli index 433e2e73..c406d96c 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Parser.vy b/cparser/Parser.vy index 93d84ecf..f1abe3d9 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -6,10 +6,11 @@ /* */ /* 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. */ +/* under the terms of the GNU Lesser General Public License as */ +/* published by the Free Software Foundation, either version 2.1 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/Rename.ml b/cparser/Rename.ml index 64412194..96424bf8 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Rename.mli b/cparser/Rename.mli index 818a51bc..c469936a 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/StructPassing.ml b/cparser/StructPassing.ml index 222da367..f1f481d0 100644 --- a/cparser/StructPassing.ml +++ b/cparser/StructPassing.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/StructPassing.mli b/cparser/StructPassing.mli index 45899a46..3ac42495 100644 --- a/cparser/StructPassing.mli +++ b/cparser/StructPassing.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Transform.ml b/cparser/Transform.ml index a57d94c4..2ca235f1 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Transform.mli b/cparser/Transform.mli index 220b7944..c00fd15c 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Unblock.ml b/cparser/Unblock.ml index 8530ae01..4b1f2262 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/Unblock.mli b/cparser/Unblock.mli index e6bea9e4..bd807096 100644 --- a/cparser/Unblock.mli +++ b/cparser/Unblock.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/deLexer.ml b/cparser/deLexer.ml index ee6976d4..e3ab3291 100644 --- a/cparser/deLexer.ml +++ b/cparser/deLexer.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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 23e90b3e..db7318c4 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -7,10 +7,11 @@ # # # 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. # +# under the terms of the GNU Lesser General Public License as # +# published by the Free Software Foundation, either version 2.1 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/pre_parser.mly b/cparser/pre_parser.mly index 4b62b235..cffbd192 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -7,10 +7,11 @@ /* */ /* 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. */ +/* under the terms of the GNU Lesser General Public License as */ +/* published by the Free Software Foundation, either version 2.1 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/pre_parser_aux.ml b/cparser/pre_parser_aux.ml index 4a4953ba..a35305ac 100644 --- a/cparser/pre_parser_aux.ml +++ b/cparser/pre_parser_aux.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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/pre_parser_aux.mli b/cparser/pre_parser_aux.mli index f6b98a95..36e33bc5 100644 --- a/cparser/pre_parser_aux.mli +++ b/cparser/pre_parser_aux.mli @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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 From 9eccbd39710aab5d6bfe021c57f50a1916d37f70 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 1 Jun 2021 14:40:30 +0200 Subject: Support `# 0 ...` preprocessed line directive Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398 --- cparser/Lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 94e490ca..42980d30 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -393,7 +393,7 @@ and string_literal startp accu = parse (* We assume gcc -E syntax but try to tolerate variations. *) and hash = parse | whitespace_char_no_newline + - (decimal_constant as n) + (digit + as n) whitespace_char_no_newline * "\"" ([^ '\n' '\"']* as file) "\"" [^ '\n']* '\n' -- cgit