Skip to content
Snippets Groups Projects
Commit 1dab6095 authored by Thibault Martin's avatar Thibault Martin Committed by Virgile Prevosto
Browse files

Add headers

parent db48dc01
No related branches found
No related tags found
No related merge requests found
(**************************************************************************)
(* *)
(* 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 include State_builder.Ref
(Cil_datatype.Location) (Cil_datatype.Location)
(struct (struct
let dependencies = [] let dependencies = []
let name = "CurrentLoc" let name = "Current_loc"
let default () = Cil_datatype.Location.unknown let default () = Cil_datatype.Location.unknown
end) end)
......
(**************************************************************************)
(* *)
(* 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 (** 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 the current location then you can use some built-in logging functions that
will print the location. will print the location.
*) *)
include State_builder.Ref with type data = Filepath.position * Filepath.position 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_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] 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 raises an exception, it is caught and re-raised after setting the location
to its old value. to its old value.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment