diff --git a/src/kernel_services/ast_queries/current_loc.ml b/src/kernel_services/ast_queries/current_loc.ml
index 14ad5f1cc00e9237c61b6e319b564972f1b8308f..c3c8dcbe115c7585068fab0375f7161982a2eac5 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 c54e25bb39c5ad20df31ce8a7d743bb4ce522c3c..824f0b08719284da1162565e6ccd77cd16abd328 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.