From 9e8ef50d61017a85e31589edb48c4a0fed99a15b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 29 Aug 2024 16:26:22 +0200
Subject: [PATCH] add missing headers
---
.../inline_stmt_contracts.ml | 22 +++++++++++++++++++
.../inline_stmt_contracts.mli | 22 +++++++++++++++++++
2 files changed, 44 insertions(+)
diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
index 4ec9f22c99..4cd772eb9d 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 ac1d10dc55..5bb3bdd9fa 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
*)
--
GitLab