diff --git a/proofs/meta_model.why b/proofs/meta_model.why index 1e87a44e223f7c59c6f75e0edb262e026b31a52f..502744e6f567dd3c5d9d0e90c6f8f632fe9146c0 100644 --- a/proofs/meta_model.why +++ b/proofs/meta_model.why @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's MetACSL plug-in. *) +(* *) +(* Copyright (C) 2018-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file LICENSE) *) +(* *) +(**************************************************************************) + module Meta_Base use set.Fset as S use fmap.Fmap as M