diff options
| -rw-r--r-- | Makefile.menhir | 12 | ||||
| -rw-r--r-- | cparser/ErrorReports.ml | 15 | ||||
| -rw-r--r-- | cparser/ErrorReports.mli | 15 | ||||
| -rw-r--r-- | cparser/GNUmakefile | 12 | ||||
| -rw-r--r-- | cparser/deLexer.ml | 15 | ||||
| -rw-r--r-- | cparser/handcrafted.messages | 12 | ||||
| -rw-r--r-- | cparser/pre_parser.mly | 1 | ||||
| -rw-r--r-- | cparser/tests/generated/Makefile | 12 |
8 files changed, 94 insertions, 0 deletions
diff --git a/Makefile.menhir b/Makefile.menhir index 82f44e5f..74bd14e2 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# François Pottier, 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 INRIA Non-Commercial License Agreement. # +# # +####################################################################### + # This is a Makefile fragment for Menhir-specific aspects. # Executable. diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml index 445b8412..a271ece1 100644 --- a/cparser/ErrorReports.ml +++ b/cparser/ErrorReports.ml @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* François Pottier, 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. *) +(* *) +(* *********************************************************************) + open Lexing open Pre_parser.MenhirInterpreter module S = MenhirLib.General (* Streams *) diff --git a/cparser/ErrorReports.mli b/cparser/ErrorReports.mli index e4296e69..f803a08b 100644 --- a/cparser/ErrorReports.mli +++ b/cparser/ErrorReports.mli @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* François Pottier, 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. *) +(* *) +(* *********************************************************************) + (* This module is in charge of reporting a syntax error after the pre_parser has failed. *) diff --git a/cparser/GNUmakefile b/cparser/GNUmakefile index d08ef178..c2792301 100644 --- a/cparser/GNUmakefile +++ b/cparser/GNUmakefile @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# François Pottier, 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 INRIA Non-Commercial License Agreement. # +# # +####################################################################### + # This is a development Makefile. # It is meant to be used by developers who wish to modify the pre_parser. diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml index 7ecfca0c..00308e4b 100644 --- a/cparser/deLexer.ml +++ b/cparser/deLexer.ml @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* François Pottier, 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. *) +(* *) +(* *********************************************************************) + (* [delex] converts a terminal symbol (represented as a symbolic string) to a concrete string, which the lexer would accept. *) diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages index 1d78360a..ba2031d7 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# François Pottier, 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 INRIA Non-Commercial License Agreement. # +# # +####################################################################### + # This file contains a complete list of sentences that cause the pre_parser to # detect an error. diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 1de726be..25e7a745 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -3,6 +3,7 @@ /* The Compcert verified compiler */ /* */ /* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt */ +/* François Pottier, INRIA Paris-Rocquencourt */ /* */ /* Copyright Institut National de Recherche en Informatique et en */ /* Automatique. All rights reserved. This file is distributed */ diff --git a/cparser/tests/generated/Makefile b/cparser/tests/generated/Makefile index 12a65e11..fb6e7610 100644 --- a/cparser/tests/generated/Makefile +++ b/cparser/tests/generated/Makefile @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# François Pottier, 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 INRIA Non-Commercial License Agreement. # +# # +####################################################################### + .PHONY: all clean SOURCES := $(wildcard *.c) |