From ac9f96ec4cef00b18b327f0302f3fb0b5646d037 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <guillaume.melquiond@inria.fr> Date: Mon, 25 Jun 2018 10:02:04 +0200 Subject: [PATCH] Add missing headers. --- examples/use_api/transform.ml | 10 ++++++++++ misc/headache_config.txt | 1 + src/jessie/literals.mll | 2 +- src/mlw/cakeml_printer.ml | 1 + src/mlw/ml_printer.mli | 11 +++++++++++ src/mlw/mlinterp.ml | 11 +++++++++++ src/mlw/mlinterp.mli | 11 +++++++++++ src/transform/abstract_quantifiers.ml | 11 +++++++++++ src/transform/eliminate_symbol.ml | 2 +- src/transform/eliminate_unknown_lsymbols.ml | 11 +++++++++++ src/transform/eliminate_unknown_types.ml | 11 +++++++++++ src/transform/matching.ml | 10 ++++++++++ src/transform/reflection.ml | 11 +++++++++++ src/transform/reflection.mli | 11 +++++++++++ src/util/debug_optim.ml | 11 +++++++++++ 15 files changed, 123 insertions(+), 2 deletions(-) diff --git a/examples/use_api/transform.ml b/examples/use_api/transform.ml index 62e5cc228..02fb3b38d 100644 --- a/examples/use_api/transform.ml +++ b/examples/use_api/transform.ml @@ -1,3 +1,13 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) open Why3 diff --git a/misc/headache_config.txt b/misc/headache_config.txt index 01cba0886..885ec8e9c 100644 --- a/misc/headache_config.txt +++ b/misc/headache_config.txt @@ -2,6 +2,7 @@ | "META.in" -> no | "extmap.ml[i]?" -> no | "literals.mll" -> no +| "report.ml[i]?" -> no # Objective Caml source | ".*\\.ml[il4]?" -> frame width:62 open:"(*" line:"*" close:"*)" | ".*\\.ml[il4]?\\.in" -> frame width:62 open:"(*" line:"*" close:"*)" diff --git a/src/jessie/literals.mll b/src/jessie/literals.mll index c6381410c..bd70e9053 100644 --- a/src/jessie/literals.mll +++ b/src/jessie/literals.mll @@ -3,7 +3,7 @@ (* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2012 *) -(* CEA (Commissariat � l'�nergie atomique et aux �nergies *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* INRIA (Institut National de Recherche en Informatique et en *) (* Automatique) *) diff --git a/src/mlw/cakeml_printer.ml b/src/mlw/cakeml_printer.ml index 50d617f79..b5d83079f 100644 --- a/src/mlw/cakeml_printer.ml +++ b/src/mlw/cakeml_printer.ml @@ -8,6 +8,7 @@ (* on linking described in file LICENSE. *) (* *) (********************************************************************) + open Compile open Format open Ident diff --git a/src/mlw/ml_printer.mli b/src/mlw/ml_printer.mli index 5359b291a..b80838e6e 100644 --- a/src/mlw/ml_printer.mli +++ b/src/mlw/ml_printer.mli @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Pp open Printer open Mltree diff --git a/src/mlw/mlinterp.ml b/src/mlw/mlinterp.ml index 7322593ea..1d6df16bc 100644 --- a/src/mlw/mlinterp.ml +++ b/src/mlw/mlinterp.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Term open Ty open Decl diff --git a/src/mlw/mlinterp.mli b/src/mlw/mlinterp.mli index 4bb8b2694..73fc03244 100644 --- a/src/mlw/mlinterp.mli +++ b/src/mlw/mlinterp.mli @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Wstdlib type value = diff --git a/src/transform/abstract_quantifiers.ml b/src/transform/abstract_quantifiers.ml index 7530b3cf6..4ae305ad3 100644 --- a/src/transform/abstract_quantifiers.ml +++ b/src/transform/abstract_quantifiers.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Term open Decl diff --git a/src/transform/eliminate_symbol.ml b/src/transform/eliminate_symbol.ml index 68e6385ea..17fad1913 100644 --- a/src/transform/eliminate_symbol.ml +++ b/src/transform/eliminate_symbol.ml @@ -1,7 +1,7 @@ (********************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) -(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) diff --git a/src/transform/eliminate_unknown_lsymbols.ml b/src/transform/eliminate_unknown_lsymbols.ml index 0ebaa5232..9a7007bee 100644 --- a/src/transform/eliminate_unknown_lsymbols.ml +++ b/src/transform/eliminate_unknown_lsymbols.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Term open Decl open Theory diff --git a/src/transform/eliminate_unknown_types.ml b/src/transform/eliminate_unknown_types.ml index 9ec9f4ba3..549737206 100644 --- a/src/transform/eliminate_unknown_types.ml +++ b/src/transform/eliminate_unknown_types.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Term open Decl open Theory diff --git a/src/transform/matching.ml b/src/transform/matching.ml index 74c49048f..1b565de9c 100644 --- a/src/transform/matching.ml +++ b/src/transform/matching.ml @@ -1,3 +1,13 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) open Ident open Ty diff --git a/src/transform/reflection.ml b/src/transform/reflection.ml index 0ddaecccf..c6cfdcbb7 100644 --- a/src/transform/reflection.ml +++ b/src/transform/reflection.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Term open Ty open Decl diff --git a/src/transform/reflection.mli b/src/transform/reflection.mli index 52ec39219..e7a8c2d7e 100644 --- a/src/transform/reflection.mli +++ b/src/transform/reflection.mli @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + val reflection_by_lemma: Decl.prsymbol -> Env.env -> Task.task Trans.tlist val reflection_by_function: bool -> string -> Env.env -> Task.task Trans.tlist diff --git a/src/util/debug_optim.ml b/src/util/debug_optim.ml index 1d5e22a0f..585f07732 100644 --- a/src/util/debug_optim.ml +++ b/src/util/debug_optim.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + open Parsetree open Ast_mapper open Asttypes -- GitLab