diff --git a/src/plugins/e-acsl/functions.ml b/src/plugins/e-acsl/functions.ml
index 189208b355b0e7c3a1f4e39f1bea6bfb9d3b27c1..cd0f3e2b502b4415f50e4a43d1db0013b0cb4d4e 100644
--- a/src/plugins/e-acsl/functions.ml
+++ b/src/plugins/e-acsl/functions.ml
@@ -23,8 +23,9 @@
 open Cil_types
 
 (* ************************************************************************** *)
-(* Misc functions {{{ *)
+(* Misc functions *)
 (* ************************************************************************** *)
+
 (* return true if the string s starts with prefix p and false otherwise *)
 let startswith p s =
   let lp = String.length p in
@@ -42,23 +43,21 @@ let strip_prefix p s =
   else
     s
 
-let get_fname_exp = function
-  | { enode = Lval(Var(vi), _) } -> vi.vname
-  | _ -> ""
-
-let is_fn f exp = f (get_fname_exp exp)
-
 (* True if a named function has a definition and false otherwise *)
-let has_fundef exp =
-  let recognize fname =
-    try let _ = Globals.Functions.find_def_by_name fname in true
-    with Not_found -> false
-  in
-  is_fn recognize exp
-(* }}} *)
+let has_fundef exp = match exp.enode with
+  | Lval(Var vi, _) ->
+    let kf =
+      try Globals.Functions.get vi
+      with Not_found -> Options.fatal "[has_fundef] not a function"
+    in
+    Kernel_function.is_definition kf
+  | Lval _ (* function pointer *) ->
+    false
+  | _ ->
+    Options.fatal "[has_fundef] not a left-value: '%a'" Printer.pp_exp exp
 
 (* ************************************************************************** *)
-(* RTL functions {{{ *)
+(* RTL functions *)
 (* ************************************************************************** *)
 
 module RTL: sig
@@ -116,10 +115,9 @@ end = struct
     | "strncmp" | "memcpy"  | "memset" | "memcmp" | "memmove" -> true
     | _ -> false
 end
-(* }}} *)
 
 (* ************************************************************************** *)
-(* Libc functions {{{ *)
+(* Libc functions *)
 (* ************************************************************************** *)
 
 module Libc: sig
@@ -143,36 +141,33 @@ module Libc: sig
   val get_printf_argument_str: loc:location -> string -> exp list -> exp
   val actual_alloca: string
 end = struct
+
   let is_dyn_alloc_name name =
     name = "malloc" || name = "realloc" || name = "calloc"
 
   let is_dyn_free_name name = name = "free" || name = "cfree"
 
   let is_vla_alloc_name name = name = "__fc_vla_alloc"
-
   let is_vla_free_name name = name = "__fc_vla_free"
 
-  let is_alloca_name name = name = "alloca" || name = "__builtin_alloca"
-
   let actual_alloca = "__builtin_alloca"
+  let is_alloca_name name = name = "alloca" || name = actual_alloca
 
   let is_memcpy_name name = name = "memcpy"
-
   let is_memset_name name = name = "memset"
 
-  let is_dyn_alloc exp = is_fn is_dyn_alloc_name exp
-
-  let is_dyn_free exp = is_fn is_dyn_free_name exp
-
-  let is_vla_alloc exp = is_fn is_vla_alloc_name exp
-
-  let is_vla_free exp = is_fn is_vla_free_name exp
+  let apply_fn f exp = match exp.enode with
+    | Lval(Var vi, _) -> f vi.vname
+    | Lval _  (* function pointer *) -> false
+    | _ -> Options.fatal "[Functions.Rtl.apply_fn] not a left-value"
 
-  let is_alloca exp = is_fn is_alloca_name exp
-
-  let is_memcpy exp = is_fn is_memcpy_name exp
-
-  let is_memset exp = is_fn is_memset_name exp
+  let is_dyn_alloc exp = apply_fn is_dyn_alloc_name exp
+  let is_dyn_free exp = apply_fn is_dyn_free_name exp
+  let is_vla_alloc exp = apply_fn is_vla_alloc_name exp
+  let is_vla_free exp = apply_fn is_vla_free_name exp
+  let is_alloca exp = apply_fn is_alloca_name exp
+  let is_memcpy exp = apply_fn is_memcpy_name exp
+  let is_memset exp = apply_fn is_memset_name exp
 
   let printf_fmt_position = function
     | "printf" -> 1
@@ -181,8 +176,7 @@ end = struct
     | _ -> 0
 
   let is_printf_name name = printf_fmt_position name <> 0
-
-  let is_printf exp = is_fn is_printf_name exp
+  let is_printf exp = apply_fn is_printf_name exp
 
   let get_printf_argument_str ~loc fn args =
     assert (is_printf_name fn);
@@ -200,7 +194,8 @@ end = struct
       | IULong -> "L" (* [unsigned long] *)
       | ILongLong -> "r" (* [long long] *)
       | IULongLong -> "R" (* [unsigned long long] *)
-      (* _Bool, char and short (either signed or unsigned are promoted to int) *)
+      (* _Bool, char and short (either signed or unsigned are promoted to
+         int) *)
       | IBool | IChar | ISChar | IUChar | IShort | IUShort -> "d"
     in
     (* get a character representing an floating point type *)
@@ -241,4 +236,3 @@ end = struct
       exps
     in Cil.mkString ~loc param_str
 end
-(* }}} *)
diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index 8c1a382e052cfff54637d2f9a91864deae594228..c5c05a20f398b9beed37c13d640a8aaec35b26de 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -22,9 +22,6 @@
 
 open Cil_types
 
-val get_fname_exp: exp -> string
-(** Provided that [exp] captures a function name return that name *)
-
 val has_fundef: exp -> bool
 (** @return [true] if a function whose name is given via [exp] is defined and
     [false] otherwise *)
@@ -34,25 +31,27 @@ val has_fundef: exp -> bool
 (* ************************************************************************** *)
 
 module RTL: sig
+
   val mk_api_name: string -> string
   (** Prefix a name (of a variable or a function) with a string that identifies
-      it as belonging to the public API of E-ACSL runtime library ([__e_acsl_])
-  *)
+      it as belonging to the public API of E-ACSL runtime library *)
 
   val mk_temporal_name: string -> string
   (** Prefix a name (of a variable or a function) with a string that identifies
       it as belonging to the public API of E-ACSL runtime library dealing
-      with temporal analysis ([__e_acsl_temporal_]). *)
+      with temporal analysis. *)
 
   val mk_gen_name: string -> string
   (** Prefix a name (of a variable or a function) with a string indicating
-      that this name has been generated during instrumentation phase.
-      ([__gen_e_acsl_]) *)
+      that this name has been generated during instrumentation phase. *)
 
   val is_generated_name: string -> bool
   (** @return [true] if the prefix of the given name indicates that it has been
      generated by E-ACSL instrumentation (see [mk_gen_name] function). *)
 
+  val is_generated_kf: kernel_function -> bool
+  (** Same as [is_generated_name] but for kernel functions *)
+
   val is_rtl_name: string -> bool
   (** @return [true] if the prefix of the given name indicates that it
       belongs to the public API of the E-ACSL Runtime Library *)
@@ -61,9 +60,6 @@ module RTL: sig
   (** Same as [is_generated_name] but indicates that the name represents a local
       variable that replaced a literal string. *)
 
-  val is_generated_kf: kernel_function -> bool
-  (** Same as [is_generated_name] but for kernel functions *)
-
   val get_original_name: kernel_function -> string
   (** Retrieve the name of the kernel function and strip prefix that indicates
       that it has been generated by the instrumentation. *)
@@ -75,13 +71,15 @@ module RTL: sig
   val has_rtl_replacement: string -> bool
   (** Given the name of C library function return true if there is a drop-in
       replacement function for it in the RTL. *)
-end
+
+end (* Rtl *)
 
 (* ************************************************************************** *)
 (** {2 Libc} Operations on functions belonging to standard library *)
 (* ************************************************************************** *)
 
 module Libc: sig
+
   val is_memcpy: exp -> bool
   (** Return [true] if [exp] captures a function name that matches [memcpy] or
       an equivalent function *)
@@ -145,11 +143,11 @@ module Libc: sig
      arguments. *)
 
   val get_printf_argument_str: loc:location -> string -> exp list -> exp
-  (** Given the name of a printf-like function ([string]) and the list
-      of its variadic arguments [exp list] return a literal string expression
-      where each character describes the type of an argument from a list.
-      Such characters are also called abbreviated types. Conversion between
-      abbreviated and C types characters is as follows:
+  (** Given the name of a printf-like function and the list of its variadic
+      arguments return a literal string expression where each character
+      describes the type of an argument from a list. Such characters are also
+      called abbreviated types. Conversion between abbreviated and C types
+      characters is as follows:
          -  "b" -> [_Bool]
          -  "c" -> [signed char]
          -  "C" -> [unsigned char]
@@ -171,4 +169,5 @@ module Libc: sig
   val actual_alloca: string
   (** The name of an actual [alloca] function used at link-time.
       In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)
-end
+
+end (* Libc *)
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index c9f79e1c7ec85a483adbeb50cf7c45b94ee3f4db..fc01fe56d5a49e656a3aa9406f267a3c675e584d 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -317,15 +317,18 @@ end = struct
 
   (* Update local environment with a statement tracking temporal metadata
      associated with memcpy/memset call *)
-  let call_memxxx current_stmt loc args fname env =
-    if Libc.is_memcpy fname || Libc.is_memset fname then
-      let name = Functions.get_fname_exp fname in
+  let call_memxxx current_stmt loc args fexp env =
+    if Libc.is_memcpy fexp || Libc.is_memset fexp then
+      let name = match fexp.enode with
+        | Lval(Var vi, _) -> vi.vname
+        | _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
+      in
       let stmt = Misc.mk_call ~loc (RTL.mk_temporal_name name) args in
       Env.add_stmt ~before:current_stmt ~post:false env stmt
     else
       env
 
-  let instr current_stmt ret fname args loc env =
+  let instr current_stmt ret fexp args loc env =
     (* Add function calls to reset_parameters and reset_return before each
        function call regardless. They are not really required, as if the
        instrumentation is correct then the right parameters will be saved
@@ -340,15 +343,15 @@ end = struct
     let env = Env.add_stmt ~before:current_stmt ~post:false env stmt in
     (* Push parameters with either a call to a function pointer or a function
         definition otherwise there is no point. *)
-    let has_def = Functions.has_fundef fname in
+    let has_def = Functions.has_fundef fexp in
     let env =
-      if Cil.isFunctionType (Cil.typeOf fname) || has_def then
+      if Cil.isFunctionType (Cil.typeOf fexp) || has_def then
         save_params current_stmt loc args env
       else
         env
     in
     (* Handle special cases of memcpy/memset *)
-    let env = call_memxxx current_stmt loc args fname env in
+    let env = call_memxxx current_stmt loc args fexp env in
     (* Memory allocating functions have no definitions so below expression
        should capture them *)
     let alloc = not has_def in
@@ -386,10 +389,10 @@ end = struct
       match li with
       | AssignInit init ->
         handle_init current_stmt NoOffset loc vi init env
-      | ConsInit(fname, args, _) ->
+      | ConsInit(fexp, args, _) ->
         let ret = Some (Cil.var vi) in
-        let fname = Cil.evar ~loc fname in
-        Function_call.instr current_stmt ret fname args loc env
+        let fexp = Cil.evar ~loc fexp in
+        Function_call.instr current_stmt ret fexp args loc env
     else env
 end
 (* }}} *)
@@ -446,8 +449,8 @@ let handle_return_stmt loc ret env =
 let handle_instruction current_stmt instr env =
   match instr with
   | Set(lv, exp, loc) -> set_instr current_stmt loc lv exp env
-  | Call(ret, fname, args, loc) ->
-    Function_call.instr current_stmt ret fname args loc env
+  | Call(ret, fexp, args, loc) ->
+    Function_call.instr current_stmt ret fexp args loc env
   | Local_init(vi, li, loc) -> Local_init.instr current_stmt vi li loc env
   | Asm _ -> Options.warning ~once:true ~current:true "@[Analysis is\
 potentially incorrect in presence of assembly code.@]"; env