diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-01-27 11:19:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-01-27 11:19:58 +0000 |
| commit | 877b4347139b187bb2e5151526ae17307d246a12 (patch) | |
| tree | e9e61f8de6ff2fe6c786554b64cd29f22562b456 /cfrontend | |
| parent | e431dcf84d7e1a1106a501d53492b672c9d0b86e (diff) | |
| download | compcert-877b4347139b187bb2e5151526ae17307d246a12.tar.gz compcert-877b4347139b187bb2e5151526ae17307d246a12.zip | |
Ajout license, README, copyright notices
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Cminorgen.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 12 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 15 | ||||
| -rw-r--r-- | cfrontend/Csharpminor.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof1.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 12 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 12 | ||||
| -rw-r--r-- | cfrontend/Csyntax.v | 15 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 12 |
10 files changed, 126 insertions, 0 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 8596ebfa..755aa28c 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from Csharpminor to Cminor. *) Require Import FSets. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ff10bb3e..a158b133 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Correctness proof for Cminor generation. *) Require Import FSets. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 76176163..35d3cce7 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -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. *) +(* *) +(* *********************************************************************) + (** Dynamic semantics for the Clight language *) Require Import Coqlib. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 7afe27f2..ce19f687 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for the Csharpminor language. *) Require Import Coqlib. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 4090c55a..b3369ae2 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Translation from Clight to Csharpminor. *) (** The main transformations performed by this first part are: diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index 9930ef80..87cdb21d 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 1: syntactic properties *) Require Import Coqlib. diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 6b7b5e3c..f6bef93e 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 2: Csharpminor construction functions *) Require Import Coqlib. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 2b2cefbc..a25c5b8b 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Correctness of the C front end, part 3: semantic preservation *) Require Import Coqlib. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 00fdaa55..6680efe2 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -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. *) +(* *) +(* *********************************************************************) + (** Abstract syntax for the Clight language *) Require Import Coqlib. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 72c4edf2..b4dd2904 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** * Typing constraints on C programs *) Require Import Coqlib. |