Update LICENSE file and headers for dual-licensed files.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 55 insertions, 402 deletions

diff --git a/LICENSE b/LICENSE
index 5fec6cb..1f8776d 100644
--- a/LICENSE
+++ b/LICENSE
@@ -15,30 +15,41 @@ the INRIA Non-Commercial License Agreement and under the Free Software
 Foundation GNU General Public License, either version 2 or (at your
 option) any later version:
 
-    backend/Cminor.v                 common/AST.v              
-    backend/CMlexer.mli              common/Errors.v      
-    backend/CMlexer.mll              common/Events.v      
-    backend/CMparser.mly             common/Globalenvs.v  
-    backend/CMtypecheck.ml           common/Mem.v         
-    backend/CMtypecheck.mli          common/Smallstep.v   
-    cfrontend/C2C.ml                 common/Switch.v      
-    cfrontend/Cop.v                  common/Values.v      
-    cfrontend/Ctypes.v               lib/Coqlib.v         
-    cfrontend/Csem.v                 lib/Floats.v         
-    cfrontend/Csyntax.v              lib/Integers.v       
-    cfrontend/Cstrategy.v            lib/Maps.v           
-    cfrontend/Clight.v               lib/Parmov.v         
-    cfrontend/PrintCsyntax.ml        lib/Camlcoq.ml       
-    cfrontend/PrintClight.ml  
-    exportclight/Clightdefs.v       
-    exportclight/ExportClight.ml
-
-    all files in the runtime/ directory
-    all files in the cparser/ directory 
+  all files in the lib/ directory
+
+  common/AST.v
+  common/Behaviors.v
+  common/Errors.v
+  common/Events.v
+  common/Globalenvs.v
+  common/Memdata.v
+  common/Memory.v
+  common/Memtype.v
+  common/Smallstep.v
+  common/Switch.v
+  common/Values.v
+
+  cfrontend/Clight.v
+  cfrontend/ClightBigstep.v
+  cfrontend/Cop.v
+  cfrontend/Csem.v
+  cfrontend/Cstrategy.v
+  cfrontend/Csyntax.v
+  cfrontend/Ctypes.v
+
+  backend/Cminor.v
+  backend/CMlexer.mli
+  backend/CMlexer.mll
+  backend/CMparser.mly
+  backend/CMtypecheck.ml
+  backend/CMtypecheck.mli
+
+  all files in the cparser/ directory 
         (except those listed below which are under a BSD license)
 
-A copy of the GNU General Public License version 2 is included below.
+  all files in the exportclight/ directory
 
+A copy of the GNU General Public License version 2 is included below.
 The choice between the two licenses for the files listed above is left
 to the user.  If you opt for the GNU General Public License, these
 files are free software and can be used both in commercial and
@@ -52,6 +63,10 @@ terms of the GNU Lesser General Public Licence, either version 3 of
 the licence, or (at your option) any later version.  A copy of the GNU
 Lesser General Public Licence version 3 is included below.
 
+The files contained in the runtime/ directory and its subdirectories
+are Copyright 2013 INRIA and distributed under the terms of the BSD
+license, included below.
+
 Finally, the following files are taken from the CIL library:
     cparser/Cabs.ml
     cparser/Lexer.mli
@@ -496,7 +511,7 @@ Public License instead of this License.
 
 ----------------------------------------------------------------------
 
-                   BSD License for the CIL library
+                   BSD License
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 1e82059..2bc5839 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -6,6 +6,10 @@
 (*                                                                     *)
 (*  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 INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)
diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
index 5f5cc51..eab427b 100644
--- a/lib/FSetAVLplus.v
+++ b/lib/FSetAVLplus.v
@@ -6,6 +6,9 @@
 (*                                                                     *)
 (*  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.     *)
 (*                                                                     *)
 (* *********************************************************************)
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
deleted file mode 100644
index 77f5d84..0000000
--- a/lib/Inclusion.v
+++ /dev/null
@@ -1,380 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Tactics to reason about list inclusion. *)
-
-(** This file (contributed by Laurence Rideau) defines a tactic [in_tac]
-  to reason over list inclusion.  It expects goals of the following form:
-<<
-  id : In x l1
-  ============================
-     In x l2
->>
-and succeeds if it can prove that [l1] is included in [l2].  
-The lists [l1] and [l2] must belong to the following sub-language [L]
-<<
-  L ::= L++L | E | E::L
->>
-The tactic uses no extra fact.
-
-A second tactic, [incl_tac], handles goals of the form
-<<
-  =============================
-    incl l1 l2
->>
-*)
-
-Require Import List.
-Require Import Bool.
-Require Import ArithRing.
-
-Ltac all_app e :=
-  match e with
-  | cons ?x nil => constr:(cons x nil)
-  | cons ?x ?tl => 
-      let v := all_app tl in constr:(app (cons x nil) v)
-  | app ?e1 ?e2 =>
-    let v1 := all_app e1 with v2 := all_app e2 in
-    constr:(app v1 v2)
-  | _ => e
-  end.
-
-(** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem
-  are taken from the CoqArt book, chapt. 16. *)
-
-Inductive bin : Type := node : bin->bin->bin | leaf : nat->bin.
-
-Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
-  match t with
-  | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin)
-  | x => node x fin
-  end.
-
-Fixpoint flatten (t:bin) : bin :=
-  match t with
-  | node t1 t2 => flatten_aux t1 (flatten t2)
-  | x => x
-  end.
-
-Fixpoint nat_le_bool (n m:nat){struct m} : bool :=
-  match n, m with
-  | O, _ => true
-  | S _, O => false
-  | S n, S m => nat_le_bool n m
-  end.
-
-Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin :=
-  match t with
-  | leaf m => 
-    if nat_le_bool n m then
-       node (leaf n)(leaf m)
-    else
-       node (leaf m)(leaf n)
-  | node (leaf m) t' =>
-    if nat_le_bool n m then node (leaf n) t else node (leaf m)(insert_bin n t')
-  | t => node (leaf n) t
-  end.
-
-Fixpoint sort_bin (t:bin) : bin :=
-  match t with
-  | node (leaf n) t' => insert_bin n (sort_bin t')
-  | t => t
-  end.
-
-Section assoc_eq.
- Variables (A : Type)(f : A->A->A).
- Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z.
-
- Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
-   match t with
-   | node t1 t2 => f (bin_A l def t1)(bin_A l def t2)
-   | leaf n => nth n l def
-   end.
-
- Theorem flatten_aux_valid_A :
-  forall (l:list A)(def:A)(t t':bin),
-   f (bin_A l def t)(bin_A l def t') = bin_A l def (flatten_aux t t').
- Proof.
-  intros l def t; elim t; simpl; auto.
-  intros t1 IHt1 t2 IHt2 t';  rewrite <- IHt1; rewrite <- IHt2.
-  symmetry; apply assoc.
- Qed.
-
- Theorem flatten_valid_A :
-  forall (l:list A)(def:A)(t:bin),
-    bin_A l def t = bin_A l def (flatten t).
- Proof.
-  intros l def t; elim t; simpl; trivial.
-  intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2.
-  trivial.
- Qed.
-
-End assoc_eq.
-
-Ltac compute_rank l n v :=
-  match l with
-  | (cons ?X1 ?X2) =>
-    let tl := constr:X2 in
-    match constr:(X1 = v) with
-    | (?X1 = ?X1) => n
-    | _ => compute_rank tl (S n) v
-    end
-  end.
-
-Ltac term_list_app l v :=
-  match v with
-  | (app ?X1 ?X2) =>
-    let l1 := term_list_app l X2 in term_list_app l1 X1
-  | ?X1 => constr:(cons X1 l)
-  end.
-
-Ltac model_aux_app l v :=
-  match v with
-  | (app ?X1 ?X2) =>
-    let r1 := model_aux_app l X1 with r2 := model_aux_app l X2 in
-      constr:(node r1 r2)
-  | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n)
-  | _ => constr:(leaf 0)
-  end.
-
-Theorem In_permute_app_head :
-  forall A:Type, forall r:A, forall x y l:list A,
-   In r (x++y++l) -> In r (y++x++l).
-intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)).
-repeat rewrite ass_app; auto with datatypes.
-Qed.
-
-Theorem insert_bin_included : 
-  forall x:nat, forall t2:bin,
-  forall (A:Type) (r:A) (l:list (list A))(def:list A), 
-     In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) ->
-     In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)).
-intros x t2; induction t2.
-intros A r l def.
-destruct t2_1 as [t2_11 t2_12|y].
-simpl.
-repeat rewrite app_ass.
-auto.
-simpl; repeat rewrite app_ass.
-simpl; case (nat_le_bool x y); simpl.
-auto.
-intros H; apply In_permute_app_head.
-elim in_app_or with (1:= H); clear H; intros H.
-apply in_or_app; left; assumption.
-apply in_or_app; right;apply (IHt2_2 A r l);assumption.
-intros A r l def; simpl.
-case (nat_le_bool x n); simpl.
-auto.
-intros H.
-rewrite (app_nil_end (nth x l def)) in H.
-rewrite (app_nil_end (nth n l def)).
-apply In_permute_app_head; assumption.
-Qed.
-
-Theorem in_or_insert_bin :
-  forall (n:nat) (t2:bin) (A:Type)(r:A)(l:list (list A)) (def:list A),
-  In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) ->
-  In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)).
-intros n t2 A r l def; induction t2.
-destruct t2_1 as [t2_11 t2_12| y].
-simpl; apply in_or_app.
-simpl; case (nat_le_bool n y); simpl.
-intros H.
-apply in_or_app.
-exact H.
-intros [H|H].
-apply in_or_app; right; apply IHt2_2; auto.
-elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
-simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto.
-Qed.
-
-Theorem sort_included :
-  forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
-    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) ->
-    In r (bin_A (list A) (app (A:=A)) l def t).
-induction t.
-destruct t1.
-simpl;intros; assumption.
-intros A r l def H; simpl in H; apply insert_bin_included.
-generalize (insert_bin_included _ _ _ _ _ _ H); clear H; intros H.
-simpl in H.
-elim in_app_or with (1 := H);clear H; intros H;
-apply in_or_insert_bin; auto.
-simpl;intros;assumption.
-Qed.
-
-Theorem sort_included2 :
-  forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
-    In r (bin_A (list A) (app (A:=A)) l def t) ->
-    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)).
-induction t.
-destruct t1.
-simpl; intros; assumption.
-intros A r l def H; simpl in H.
-simpl; apply in_or_insert_bin.
-elim in_app_or with (1:= H); auto.
-simpl; auto.
-Qed.
-
-Theorem in_remove_head :
-  forall (A:Type)(x:A)(l1 l2 l3:list A),
-  In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3).
-intros A x l1 l2 l3 H H1.
-elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
-Qed.
-
-Fixpoint check_all_leaves (n:nat)(t:bin) {struct t} : bool :=
-  match t with
-    leaf n1 => nateq n n1
-  | node t1 t2 => andb (check_all_leaves n t1)(check_all_leaves n t2)
-  end.
-
-Fixpoint remove_all_leaves (n:nat)(t:bin){struct t} : bin :=
-  match t with
-    leaf n => leaf n
-  | node (leaf n1) t2 =>
-    if nateq n n1 then remove_all_leaves n t2 else t
-  | _ => t
-  end.
-
-Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool :=
-  match t1 with
-    leaf n => check_all_leaves n t2
-  | node (leaf n1) t1' =>
-     check_all_leaves n1 t2 || test_inclusion t1' (remove_all_leaves n1 t2)
-  | _ => false
-  end.
-
-Theorem check_all_leaves_sound :
-  forall x t2,
-    check_all_leaves x t2 = true ->
-    forall (A:Type)(r:A)(l:list(list A))(def:list A),
-    In r (bin_A (list A) (app (A:=A)) l def t2) ->
-    In r (nth x l def).
-intros x t2; induction t2; simpl.
-destruct (check_all_leaves x t2_1);
-destruct (check_all_leaves x t2_2); simpl; intros Heq; try discriminate.
-intros A r l def H; elim in_app_or with (1:= H); clear H; intros H; auto.
-intros Heq A r l def; rewrite (nateq_prop x n); auto.
-rewrite Heq; unfold Is_true; auto.
-Qed.
-
-Theorem remove_all_leaves_sound :
-  forall x t2,
-  forall (A:Type)(r:A)(l:list(list A))(def:list A),
-  In r (bin_A (list A) (app(A:=A)) l def t2) ->
-  In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/
-  In r (nth x l def).
-intros x t2; induction t2; simpl.
-destruct t2_1.
-simpl; auto.
-intros A r l def.
-generalize (refl_equal (nateq x n)); pattern (nateq x n) at -1;
- case (nateq x n); simpl; auto.
-intros Heq_nateq.
-assert (Heq_xn : x=n).
-apply nateq_prop; rewrite Heq_nateq;unfold Is_true;auto.
-rewrite Heq_xn.
-intros H; elim in_app_or with (1:= H); auto.
-clear H; intros H.
-rewrite Heq_xn in IHt2_2; auto.
-auto.
-Qed.
-
-Theorem test_inclusion_sound :
-  forall t1 t2:bin,
-  test_inclusion t1 t2 = true ->
-  forall (A:Type)(r:A)(l:list(list A))(def:list A),
-  In r (bin_A (list A)(app(A:=A)) l def t2) ->
-  In r (bin_A (list A)(app(A:=A)) l def t1).
-intros t1; induction t1.
-destruct t1_1 as [t1_11 t1_12|x].
-simpl; intros; discriminate.
-simpl; intros t2 Heq A r l def H.
-assert 
- (check_all_leaves x t2 = true \/ 
-  test_inclusion t1_2 (remove_all_leaves x t2) = true).
-destruct (check_all_leaves x t2);
-destruct (test_inclusion t1_2 (remove_all_leaves x t2));
-simpl in Heq; try discriminate Heq; auto.
-elim H0; clear H0; intros H0.
-apply in_or_app; left; apply check_all_leaves_sound with (1:= H0); auto.
-elim remove_all_leaves_sound with (x:=x)(1:= H); intros H'.
-apply in_or_app; right; apply IHt1_2 with (1:= H0); auto.
-apply in_or_app; auto.
-simpl; apply check_all_leaves_sound.
-Qed.
-
-Theorem inclusion_theorem :
-  forall t1 t2 : bin,
-    test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true ->
-    forall (A:Type)(r:A)(l:list(list A))(def:list A),
-    In r (bin_A (list A) (app(A:=A)) l def t2) ->
-    In r (bin_A (list A) (app(A:=A)) l def t1).
-intros t1 t2 Heq A r l def H.
-rewrite flatten_valid_A with (t:= t1)(1:= (ass_app (A:= A))).
-apply sort_included.
-apply test_inclusion_sound with (t2 := sort_bin (flatten t2)).
-assumption.
-apply sort_included2.
-rewrite <- flatten_valid_A with (1:= (ass_app (A:= A))).
-assumption.
-Qed.
-
-Ltac in_tac :=
-  match goal with
-  | id : In ?x nil |- _ => elim id
-  | id : In ?x ?l1 |- In ?x ?l2 =>
-    let t := type of x in
-    let v1 := all_app l1 in
-    let v2 := all_app l2 in
-    (let l := term_list_app (nil (A:=list t)) v2 in
-     let term1 := model_aux_app l v1 with
-         term2 := model_aux_app l v2 in
-        (change (In x (bin_A (list t) (app(A:=t)) l (nil(A:=t)) term2));
-        apply inclusion_theorem with (t2:= term1);[apply refl_equal|exact id]))
-  end.
-
-Ltac incl_tac :=
-  match goal with
-  |- incl _ _ => intro; intro; in_tac
-  end.
-   
-(* Usage examples.
-
-Theorem ex1 : forall x y z:nat, forall l1 l2 : list nat,
-   In x (y::l1++l2) -> In x (l2++z::l1++(y::nil)).
-intros.
-in_tac.
-Qed.
-
-Fixpoint mklist (f:nat->nat)(n:nat){struct n} : list nat :=
- match n with 0 => nil | S p => mklist f p++(f p::nil) end.
-
-(* At the time of writing these lines, this example takes about 5 seconds
-     for 40 elements and 22 seconds for 60 elements.
-   A variant to the example is to replace mklist f p++(f p::nil) with
-   f p::mklist f p, in this case the time is 6 seconds for 40 elements and
-   35 seconds for 60 elements. *)
-
-Theorem ex2 : 
-  forall x : nat, In x (mklist (fun y => y) 40) ->
-     In x (mklist (fun y => (40 - 1) - y) 40).
-lazy beta iota zeta delta [mklist minus].
-intros.
-in_tac.
-Qed.
-
-(* The tactic could be made more efficient by using binary trees and
-   numbers of type positive instead of lists and natural numbers. *)
-
-*)
diff --git a/lib/Iteration.v b/lib/Iteration.v
index f2e85ec..f3507fe 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -6,6 +6,9 @@
 (*                                                                     *)
 (*  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.     *)
 (*                                                                     *)
 (* *********************************************************************)
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 3fc0d4c..d7adede 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -6,6 +6,10 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  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.     *)
 (*                                                                     *)
 (* *********************************************************************)
diff --git a/lib/Ordered.v b/lib/Ordered.v
index 026671a..5d02586 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -6,6 +6,10 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  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.     *)
 (*                                                                     *)
 (* *********************************************************************)