diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f958082d4b04d4d907094cd9ea3fefcb985d5284..264239138bb9d1bc00fe45a8bac7a0e0fd433de1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -59,6 +59,31 @@ let valid_sid = false
 open Cil_types
 open Cil_datatype
 
+(* Maps the start and end positions of a function declaration or definition
+   (including its possible contract) to its name. *)
+module FuncLocs = struct
+  include
+    State_builder.List_ref
+      (Datatype.Triple
+         (Cil_datatype.Position)(Cil_datatype.Position)(Datatype.String)
+      )
+      (struct
+        let name = "FuncLocs"
+        let dependencies = [ Kernel.Files.self ]
+      end)
+
+  let add_loc ?spec loc1 loc2 funcname =
+    let startpos =
+      match spec with
+      | None -> fst loc1
+      | Some (_, spec_loc) -> fst spec_loc
+    in
+    let endpos = snd loc2 in
+    add (startpos, endpos, funcname)
+end
+
+let func_locs () = FuncLocs.get ()
+
 let stripUnderscore s =
   if String.length s = 1 then begin
     if s = "_" then
@@ -8613,12 +8638,14 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * C
     List.exists (fun (_,el) -> List.exists is_fc_stdlib el) a
   in
   (* Make a first version of the varinfo *)
+  let vi_loc = convLoc cloc in
   let vi = makeVarInfoCabs ~ghost ~isformal:false ~referenced:islibc
-      ~isglobal:true ~isgenerated (convLoc cloc) (t,s,b,attr_list) (n,ndt,a)
+      ~isglobal:true ~isgenerated vi_loc (t,s,b,attr_list) (n,ndt,a)
   in
   (* Add the variable to the environment before doing the initializer
    * because it might refer to the variable itself *)
   if isFunctionType vi.vtype then begin
+    FuncLocs.add_loc ?spec:logic_spec (CurrentLoc.get ()) vi_loc n;
     if inite != Cabs.NO_INIT  then
       Kernel.error ~once:true ~current:true
         "Function declaration with initializer (%s)\n" vi.vname;
@@ -9240,6 +9267,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
       Kernel.debug ~dkey:Kernel.dkey_typing_global
         "Definition of %s at %a\n" n Cil_printer.pp_location idloc;
       CurrentLoc.set idloc;
+      FuncLocs.add_loc ?spec loc1 endloc n;
       IH.clear callTempVars;
 
       (* Make the fundec right away, and we'll populate it later. We
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index 44ea2ddf74785720d77ef8af20e9510925f8866b..f15e3a97b31a45f205d88aad2d1c1a375f4b208a 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -280,6 +280,22 @@ val stmtFallsThrough: Cil_types.stmt -> bool
 
 val fieldsToInit: Cil_types.compinfo -> string option -> Cil_types.offset list
 
+(**
+   Returns a mapping (pos_start, pos_end, funcname) for each function
+   declaration and definition, spanning the entire function, including
+   its specification (if it has one).
+
+   Currently, for function declarations, the location ends at the function
+   name, before the formal parameter list. For definitions, it spans until the
+   closing brace.
+
+   Note that the list is _not_ sorted, and must be further processed
+   for efficient data retrieval.
+
+   @since Frama-C+dev
+*)
+val func_locs : unit -> (Filepath.position * Filepath.position * string) list
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/tests/syntax/func_locs.i b/tests/syntax/func_locs.i
new file mode 100644
index 0000000000000000000000000000000000000000..9bde496168fe2aa66a3b12a9963fbfa61147fbb0
--- /dev/null
+++ b/tests/syntax/func_locs.i
@@ -0,0 +1,36 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+   STDOPT: +"-no-print"
+*/
+
+
+//@ assigns \nothing;
+void with_spec() {
+}
+
+int gx;
+
+/*@
+  requires req: a >= 0 || gx == 0;
+  assigns \result \from a;
+  ensures ens: \result == a;
+ */
+int id(int a);
+
+/*@
+  requires req: a >= 0;
+*/
+int id(int a);
+
+int decl_no_spec(); int id(int a);
+
+int def_no_spec() {
+  return 2;
+}
+
+/*@
+  requires \true;
+*/
+int main() {
+  return 0;
+}
diff --git a/tests/syntax/func_locs.ml b/tests/syntax/func_locs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e28f0429b68ca220b12e37f15c4417edc32179c6
--- /dev/null
+++ b/tests/syntax/func_locs.ml
@@ -0,0 +1,9 @@
+let run () =
+  List.iter (fun (pos1, pos2, fname) ->
+      Format.printf "%a - %a -> %s@."
+        Cil_datatype.Position.pp_with_col pos1
+        Cil_datatype.Position.pp_with_col pos2
+        fname
+    ) (Cabs2cil.func_locs ())
+
+let () = Db.Main.extend run
diff --git a/tests/syntax/oracle/func_locs.res.oracle b/tests/syntax/oracle/func_locs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8fd4ca099e2fa45737df2beec4c827b0473d0f65
--- /dev/null
+++ b/tests/syntax/oracle/func_locs.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing func_locs.i (no preprocessing)
+[kernel] func_locs.i:20: Warning: 
+  found two contracts (old location: func_locs.i:13). Merging them
+func_locs.i:31 char 3 - func_locs.i:36 char 1 -> main
+func_locs.i:27 char 4 - func_locs.i:29 char 1 -> def_no_spec
+func_locs.i:25 char 20 - func_locs.i:25 char 26 -> id
+func_locs.i:25 char 0 - func_locs.i:25 char 16 -> decl_no_spec
+func_locs.i:20 char 3 - func_locs.i:23 char 6 -> id
+func_locs.i:13 char 3 - func_locs.i:18 char 6 -> id
+func_locs.i:7 char 3 - func_locs.i:9 char 1 -> with_spec