From 877b4347139b187bb2e5151526ae17307d246a12 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 27 Jan 2008 11:19:58 +0000 Subject: Ajout license, README, copyright notices git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 12 ++++++++++++ cfrontend/Cminorgenproof.v | 12 ++++++++++++ cfrontend/Csem.v | 15 +++++++++++++++ cfrontend/Csharpminor.v | 12 ++++++++++++ cfrontend/Cshmgen.v | 12 ++++++++++++ cfrontend/Cshmgenproof1.v | 12 ++++++++++++ cfrontend/Cshmgenproof2.v | 12 ++++++++++++ cfrontend/Cshmgenproof3.v | 12 ++++++++++++ cfrontend/Csyntax.v | 15 +++++++++++++++ cfrontend/Ctyping.v | 12 ++++++++++++ 10 files changed, 126 insertions(+) (limited to 'cfrontend') 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. -- cgit