diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml index 4ec9f22c99e0e7620659bd5eee9ec60410685709..4cd772eb9d94d9e2807329208e4fa0b58ce1ff26 100644 --- a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml +++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + open Cil_types let emitter = diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.mli b/src/kernel_services/ast_transformations/inline_stmt_contracts.mli index ac1d10dc55bcb9631b8a6074572badf09e14109d..5bb3bdd9fa4fc3ecb2288e18abf275ea4bb12d3b 100644 --- a/src/kernel_services/ast_transformations/inline_stmt_contracts.mli +++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.mli @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + (** transforms requires and ensures of statement contracts into assert. This transformation is done after cleanup *)