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 --- backend/Allocation.v | 12 ++++++++++++ backend/Allocproof.v | 12 ++++++++++++ backend/Alloctyping.v | 12 ++++++++++++ backend/Bounds.v | 12 ++++++++++++ backend/CSE.v | 12 ++++++++++++ backend/CSEproof.v | 12 ++++++++++++ backend/Cminor.v | 15 +++++++++++++++ backend/CminorSel.v | 12 ++++++++++++ backend/Coloring.v | 12 ++++++++++++ backend/Coloringproof.v | 12 ++++++++++++ backend/Constprop.v | 12 ++++++++++++ backend/Constpropproof.v | 12 ++++++++++++ backend/Conventions.v | 12 ++++++++++++ backend/InterfGraph.v | 12 ++++++++++++ backend/Kildall.v | 12 ++++++++++++ backend/LTL.v | 12 ++++++++++++ backend/LTLin.v | 12 ++++++++++++ backend/LTLintyping.v | 12 ++++++++++++ backend/LTLtyping.v | 12 ++++++++++++ backend/Linear.v | 12 ++++++++++++ backend/Linearize.v | 12 ++++++++++++ backend/Linearizeproof.v | 12 ++++++++++++ backend/Linearizetyping.v | 12 ++++++++++++ backend/Lineartyping.v | 12 ++++++++++++ backend/Locations.v | 12 ++++++++++++ backend/Mach.v | 12 ++++++++++++ backend/Machabstr.v | 12 ++++++++++++ backend/Machabstr2concr.v | 12 ++++++++++++ backend/Machconcr.v | 12 ++++++++++++ backend/Machtyping.v | 12 ++++++++++++ backend/Op.v | 12 ++++++++++++ backend/PPC.v | 12 ++++++++++++ backend/PPCgen.v | 12 ++++++++++++ backend/PPCgenproof.v | 12 ++++++++++++ backend/PPCgenproof1.v | 12 ++++++++++++ backend/PPCgenretaddr.v | 12 ++++++++++++ backend/Parallelmove.v | 12 ++++++++++++ backend/RTL.v | 12 ++++++++++++ backend/RTLbigstep.v | 12 ++++++++++++ backend/RTLgen.v | 12 ++++++++++++ backend/RTLgenproof.v | 12 ++++++++++++ backend/RTLgenspec.v | 12 ++++++++++++ backend/RTLtyping.v | 12 ++++++++++++ backend/Registers.v | 12 ++++++++++++ backend/Reload.v | 12 ++++++++++++ backend/Reloadproof.v | 12 ++++++++++++ backend/Reloadtyping.v | 12 ++++++++++++ backend/Selection.v | 12 ++++++++++++ backend/Selectionproof.v | 12 ++++++++++++ backend/Stacking.v | 12 ++++++++++++ backend/Stackingproof.v | 12 ++++++++++++ backend/Stackingtyping.v | 12 ++++++++++++ backend/Tunneling.v | 12 ++++++++++++ backend/Tunnelingproof.v | 12 ++++++++++++ backend/Tunnelingtyping.v | 12 ++++++++++++ 55 files changed, 663 insertions(+) (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index eab5233d..3a5960be 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.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. *) +(* *) +(* *********************************************************************) + (** Register allocation. *) Require Import Coqlib. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1b5a4156..68d6868c 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.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 the [Allocation] pass (translation from RTL to LTL). *) diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index c0abf0d6..469fd3c3 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.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. *) +(* *) +(* *********************************************************************) + (** Preservation of typing during register allocation. *) Require Import Coqlib. diff --git a/backend/Bounds.v b/backend/Bounds.v index a0f09ce8..0e8b9faf 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.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. *) +(* *) +(* *********************************************************************) + (** Computation of resource bounds forr Linear code. *) Require Import Coqlib. diff --git a/backend/CSE.v b/backend/CSE.v index a7901d61..b7e19c1b 100644 --- a/backend/CSE.v +++ b/backend/CSE.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. *) +(* *) +(* *********************************************************************) + (** Common subexpression elimination over RTL. This optimization proceeds by value numbering over extended basic blocks. *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index d46a39f1..a87cd758 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.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 common subexpression elimination. *) Require Import Coqlib. diff --git a/backend/Cminor.v b/backend/Cminor.v index 1d2eea74..df541a11 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.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 and semantics for the Cminor language. *) Require Import Coqlib. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 859c46e7..35788685 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.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. *) +(* *) +(* *********************************************************************) + (** The Cminor language after instruction selection. *) Require Import Coqlib. diff --git a/backend/Coloring.v b/backend/Coloring.v index 57f7d594..5e91b03c 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.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. *) +(* *) +(* *********************************************************************) + (** Construction and coloring of the interference graph. *) Require Import Coqlib. diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index ce24030d..cea4ce5f 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.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 graph coloring. *) Require Import SetoidList. diff --git a/backend/Constprop.v b/backend/Constprop.v index fecfb19f..18fa589f 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.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. *) +(* *) +(* *********************************************************************) + (** Constant propagation over RTL. This is the first of the two optimizations performed at RTL level. It proceeds by a standard dataflow analysis and the corresponding code transformation. *) diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dfa828bf..e16f322e 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.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 constant propagation. *) Require Import Coqlib. diff --git a/backend/Conventions.v b/backend/Conventions.v index 9d005b34..ea7d448e 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.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. *) +(* *) +(* *********************************************************************) + (** Function calling conventions and other conventions regarding the use of machine registers and stack slots. *) diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 5dc4fe9e..c9891c27 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.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. *) +(* *) +(* *********************************************************************) + (** Representation of interference graphs for register allocation. *) Require Import Coqlib. diff --git a/backend/Kildall.v b/backend/Kildall.v index 41011f2b..b4445aeb 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.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. *) +(* *) +(* *********************************************************************) + (** Solvers for dataflow inequations. *) Require Import Coqlib. diff --git a/backend/LTL.v b/backend/LTL.v index db996ba4..e99e016e 100644 --- a/backend/LTL.v +++ b/backend/LTL.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. *) +(* *) +(* *********************************************************************) + (** The LTL intermediate language: abstract syntax and semantics. LTL (``Location Transfer Language'') is the target language diff --git a/backend/LTLin.v b/backend/LTLin.v index da8719ac..6cf2eb53 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.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. *) +(* *) +(* *********************************************************************) + (** The LTLin intermediate language: abstract syntax and semantcs *) (** The LTLin language is a variant of LTL where control-flow is not diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 06c50f8b..1c0c3f30 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.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 rules for LTLin. *) Require Import Coqlib. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 646edc82..18308b8f 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.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 rules for LTL. *) Require Import Coqlib. diff --git a/backend/Linear.v b/backend/Linear.v index a6e31fb6..b9880ff1 100644 --- a/backend/Linear.v +++ b/backend/Linear.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. *) +(* *) +(* *********************************************************************) + (** The Linear intermediate language: abstract syntax and semantcs *) (** The Linear language is a variant of LTLin where arithmetic diff --git a/backend/Linearize.v b/backend/Linearize.v index 57919b87..42330ed9 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.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. *) +(* *) +(* *********************************************************************) + (** Linearization of the control-flow graph: translation from LTL to LTLin *) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index a625ba75..12d0a1f3 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.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 code linearization *) Require Import Coqlib. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 473b3421..ba547230 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.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. *) +(* *) +(* *********************************************************************) + (** Type preservation for the Linearize pass *) Require Import Coqlib. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index baf522aa..0f5a1ec9 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.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 rules for Linear. *) Require Import Coqlib. diff --git a/backend/Locations.v b/backend/Locations.v index aaefc08c..1373887f 100644 --- a/backend/Locations.v +++ b/backend/Locations.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. *) +(* *) +(* *********************************************************************) + (** Locations are a refinement of RTL pseudo-registers, used to reflect the results of register allocation (file [Allocation]). *) diff --git a/backend/Mach.v b/backend/Mach.v index 05805ec5..f7275041 100644 --- a/backend/Mach.v +++ b/backend/Mach.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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract syntax. Mach is the last intermediate language before generation of assembly diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 0abdd1e1..32a316ae 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract semantics. *) Require Import Coqlib. diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 5349fb50..ffdfb336 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.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. *) +(* *) +(* *********************************************************************) + (** Simulation between the two semantics for the Mach language. *) Require Import Coqlib. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5a095d79..2eb3d478 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: concrete semantics. *) Require Import Coqlib. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 28037cec..5e5f03c4 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.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. *) +(* *) +(* *********************************************************************) + (** Type system for the Mach intermediate language. *) Require Import Coqlib. diff --git a/backend/Op.v b/backend/Op.v index 698b433c..51b5e530 100644 --- a/backend/Op.v +++ b/backend/Op.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. *) +(* *) +(* *********************************************************************) + (** Operators and addressing modes. The abstract syntax and dynamic semantics for the CminorSel, RTL, LTL and Mach languages depend on the following types, defined in this library: diff --git a/backend/PPC.v b/backend/PPC.v index 244c5951..8af2c9be 100644 --- a/backend/PPC.v +++ b/backend/PPC.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 PowerPC assembly language *) Require Import Coqlib. diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 171945de..805d039b 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.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 Mach to PPC. *) Require Import Coqlib. diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 8d6d9342..2b00cfc0 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.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 PPC generation: main proof. *) Require Import Coqlib. diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index c0125fc2..107ea053 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.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 PPC generation: auxiliary results. *) Require Import Coqlib. diff --git a/backend/PPCgenretaddr.v b/backend/PPCgenretaddr.v index f2802ecd..3526865e 100644 --- a/backend/PPCgenretaddr.v +++ b/backend/PPCgenretaddr.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. *) +(* *) +(* *********************************************************************) + (** Predictor for return addresses in generated PPC code. The [return_address_offset] predicate defined here is used in the diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index 3d77b57a..baab2071 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.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 of parallel moves into sequences of individual moves. In this file, we adapt the generic "parallel move" algorithm diff --git a/backend/RTL.v b/backend/RTL.v index b1afc94a..abecd4a7 100644 --- a/backend/RTL.v +++ b/backend/RTL.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. *) +(* *) +(* *********************************************************************) + (** The RTL intermediate language: abstract syntax and semantics. RTL stands for "Register Transfer Language". This is the first diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v index 0ad6e68a..182f5935 100644 --- a/backend/RTLbigstep.v +++ b/backend/RTLbigstep.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. *) +(* *) +(* *********************************************************************) + (** An alternate, mixed-step semantics for the RTL intermediate language. *) Require Import Coqlib. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 52a6c8ae..3cc0eebf 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.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 CminorSel to RTL. *) Require Import Coqlib. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index dd8728fd..e02463a2 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.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 RTL generation. *) Require Import Coqlib. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 94afff85..b8061a3f 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.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 specification of RTL generation *) (** In this module, we define inductive predicates that specify the diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 40567491..a30f9e50 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.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 rules and a type inference algorithm for RTL. *) Require Import Coqlib. diff --git a/backend/Registers.v b/backend/Registers.v index e4b7b000..c3d04d60 100644 --- a/backend/Registers.v +++ b/backend/Registers.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. *) +(* *) +(* *********************************************************************) + (** Pseudo-registers and register states. This library defines the type of pseudo-registers (also known as diff --git a/backend/Reload.v b/backend/Reload.v index 58e17ff5..c5559e35 100644 --- a/backend/Reload.v +++ b/backend/Reload.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. *) +(* *) +(* *********************************************************************) + (** Reloading, spilling, and explication of calling conventions. *) Require Import Coqlib. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index e9ced51f..401ae466 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.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 the [Reload] pass. *) Require Import Coqlib. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 155c174d..3f0ff1ee 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.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. *) +(* *) +(* *********************************************************************) + (** Proof of type preservation for Reload and of correctness of computation of stack bounds for Linear. *) diff --git a/backend/Selection.v b/backend/Selection.v index 0183ee7d..8a69adec 100644 --- a/backend/Selection.v +++ b/backend/Selection.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. *) +(* *) +(* *********************************************************************) + (** Instruction selection *) (** The instruction selection pass recognizes opportunities for using diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 177e3211..e28bfaf3 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.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 instruction selection *) Require Import Coqlib. diff --git a/backend/Stacking.v b/backend/Stacking.v index c19e293f..16595e54 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.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. *) +(* *) +(* *********************************************************************) + (** Layout of activation records; translation from Linear to Mach. *) Require Import Coqlib. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 905570ef..46e19ca9 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.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 the translation from Linear to Mach. *) (** This file proves semantic preservation for the [Stacking] pass. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index fa8a3e2e..aa534ff0 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.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. *) +(* *) +(* *********************************************************************) + (** Type preservation for the [Stacking] pass. *) Require Import Coqlib. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 15f4676d..2f520c61 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.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. *) +(* *) +(* *********************************************************************) + (** Branch tunneling (optimization of branches to branches). *) Require Import Coqlib. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 3777eaa9..d0c95462 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.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 the branch tunneling optimization. *) Require Import Coqlib. diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index c611067c..57e1271d 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.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. *) +(* *) +(* *********************************************************************) + (** Type preservation for the Tunneling pass *) Require Import Coqlib. -- cgit