From 1dab60950cfc26a22b598d5b3f7c543f3cbbbf7f Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 9 Feb 2024 09:10:50 +0100
Subject: [PATCH] Add headers
---
.../ast_queries/current_loc.ml | 24 +++++++++++++++++-
.../ast_queries/current_loc.mli | 25 +++++++++++++++++--
2 files changed, 46 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_queries/current_loc.ml b/src/kernel_services/ast_queries/current_loc.ml
index 14ad5f1cc00..c3c8dcbe115 100644
--- a/src/kernel_services/ast_queries/current_loc.ml
+++ b/src/kernel_services/ast_queries/current_loc.ml
@@ -1,8 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
include State_builder.Ref
(Cil_datatype.Location)
(struct
let dependencies = []
- let name = "CurrentLoc"
+ let name = "Current_loc"
let default () = Cil_datatype.Location.unknown
end)
diff --git a/src/kernel_services/ast_queries/current_loc.mli b/src/kernel_services/ast_queries/current_loc.mli
index c54e25bb39c..824f0b08719 100644
--- a/src/kernel_services/ast_queries/current_loc.mli
+++ b/src/kernel_services/ast_queries/current_loc.mli
@@ -1,12 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
(** A reference to the current location. If you are careful to set this to
the current location then you can use some built-in logging functions that
will print the location.
*)
-
include State_builder.Ref with type data = Filepath.position * Filepath.position
(** [with_loc loc f x] set the current location to [loc], which can be used
- with [CurrentLoc.get ()] or via the option [~current] in Log functions.
+ with [Current_loc.get ()] or via the option [~current] in Log functions.
The old location is saved and set back after exectution of [f x]. If [f x]
raises an exception, it is caught and re-raised after setting the location
to its old value.
--
GitLab