diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml
index 980326a32fbe9b76d3eb3685b760a8104e46189d..f67f04117572065772b9404fffd676847195177f 100644
--- a/src/plugins/e-acsl/prepare_ast.ml
+++ b/src/plugins/e-acsl/prepare_ast.ml
@@ -50,28 +50,26 @@ let sufficiently_aligned attrs algn =
       should not happen really *)
       assert false
     | _ -> acc
-  ) 0 attrs in
-  if alignment > 0 then true else false
+  ) 0 attrs in alignment > 0
 
 (* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
  * true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
  * of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
 let require_alignment typ attrs algn =
-  if (Cil.bitsSizeOf typ) < algn*8 && not (sufficiently_aligned attrs algn) then
-    true
-  else
-    false
+  Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
 
 class prepare_visitor prj = object (_)
   inherit Visitor.frama_c_copy prj
 
   (* Add align attributes to local variables (required by temporal analysis) *)
   method !vblock _ =
-    if (Temporal.is_enabled ()) then
+    if Temporal.is_enabled () then
       Cil.DoChildrenPost (fun blk ->
         List.iter (fun vi ->
+        (* 4 bytes alignment is required to allow sufficient space for storage
+           of 32-bit timestamps in a 1:1 shadow. *)
           if require_alignment vi.vtype vi.vattr 4; then begin
-            vi.vattr <- Attr("aligned",[AInt(Integer.four)]) :: vi.vattr
+            vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
           end)
         blk.blocals;
       blk)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
index 55db362411c22848166f9fe4974c86782c5c279e..1f00c49e34d5ac6cbe75f831e24122eb0630a5c7 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
@@ -105,8 +105,8 @@ static void describe_run();
 # error "No E-ACSL memory model defined. Aborting compilation"
 #endif
 
-/* Temporal analysis shared by both models.
- * Uses macros differently defined macros */
+/* This header contains temporal analysis shared by both models.
+   It should be here as it uses differently defined macros */
 #include "e_acsl_temporal.h"
 
 #ifdef E_ACSL_WEAK_VALIDITY
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
index 40b7a006c17e9b78f904cf762f14211e5365439f..55ceb6261f913ce8a7f6c0311c9a6bdfa33ec9a5 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
@@ -51,9 +51,11 @@ static uint32_t temporal_timestamp = 2;
 
 struct temporal_parameter {
   void *ptr;
+  /* Number all members such that there is no `0` which potentially
+     corresponds to an invalid number */
   enum {
     TBlockN = 10,
-    TReferentN = 20,
+    TReferentN  = 20,
     TCopy = 30
   } temporal_flow;
 };
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 94101e24955198fce58609d2e54b8303fd14e488..f1a03d0df9b027b55c47504fea78c2c4a2f677b1 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -1234,7 +1234,7 @@ static int heap_initialized(uintptr_t addr, long len) {
 #ifdef E_ACSL_TEMPORAL
 static uint32_t heap_temporal_info(uintptr_t addr, int origin) {
   /* NOTE: No checking for allocated blocks, since an invalid
-     timestamp is zero and ununsed memory is nullified then an invalid
+     timestamp is zero and unused memory is nullified then an invalid
      timestamp is also returned for allocated memory */
   if (origin) {
     uintptr_t *aligned_shadow = (uintptr_t*)ALIGNED_HEAP_SHADOW(addr);
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index 6ecaacaa95e5b30596f746491e883a75d9e4c127..e6314460f697aceb8983d8b72703b0a085a166d1 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -24,7 +24,7 @@ open Cil_types
 open Cil_datatype
 
 (* ************************************************************************** *)
-(** {Configuration} {{{ *)
+(* Configuration {{{ *)
 (* ************************************************************************** *)
 
 let current_stmt = ref Cil.dummyStmt
@@ -33,223 +33,230 @@ let generate = ref false
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Types} {{{ *)
+(* Types {{{ *)
 (* ************************************************************************** *)
 
 (* Type of identifier tracked by a LHS referent number *)
 type flow =
-  | Direct (* take BlockID of RHS *)
-  | Indirect (* take ReferentID of RHS *)
+  | Direct (* take origin number of RHS  *)
+  | Indirect (* take referent number of RHS *)
   | Copy (* Copy shadow from RHS to LHS *)
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Miscellaneous} {{{ *)
+(* Miscellaneous {{{ *)
 (* ************************************************************************** *)
 
 (* Generate a function name in the temporal analysis name space, i.e., prefixed
    by [__e_acsl_temporal_ + function name].
    NOTE: Further on, all analysis function names are used without prefix *)
-let mk_api_name name =
-  let fname = "temporal_" ^ name in Misc.mk_api_name fname
+let mk_api_name name = Misc.mk_api_name ("temporal_" ^ name)
 
-let is_alloc_name fn =
-  fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
+let is_alloc_name fn = fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
 
-let is_memcpy_name fn =
-  fn = "memcpy"
+let is_memcpy_name fn = fn = "memcpy"
 
-let is_memset_name fn =
-  fn = "memset"
+let is_memset_name fn = fn = "memset"
 
-let is_fn fname f =
-  match fname with
-  | { enode = Lval(Var(vi), _) } when f vi.vname -> true
-  | _ -> false
+let get_fname = function
+  | { enode = Lval(Var(vi), _) } -> vi.vname
+  | _ -> ""
 
-let is_alloc fvi =
-  is_fn fvi is_alloc_name
+let is_fn f fname = f (get_fname fname)
 
-let is_memcpy fvi =
-  is_fn fvi is_memcpy_name
+let is_alloc fvi = is_fn is_alloc_name fvi
 
-let is_memset fvi =
-  is_fn fvi is_memset_name
+let is_memcpy fvi = is_fn is_memcpy_name fvi
+
+let is_memset fvi = is_fn is_memset_name fvi
 
 (* True if a named function has a definition and false otherwise *)
 let has_fundef fname =
   let recognize fn =
-    try
-      let _ = Globals.Functions.find_def_by_name fn in true
-    with
-      Not_found -> false
-  in is_fn fname recognize
+    try let _ = Globals.Functions.find_def_by_name fn in true
+    with Not_found -> false
+  in
+  is_fn recognize fname
 
 (* Shortcuts for SA in Mmodel_analysis *)
 let must_model_exp exp env =
   let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
-    Mmodel_analysis.must_model_exp ~bhv ~kf exp
+  Mmodel_analysis.must_model_exp ~bhv ~kf exp
 
 let must_model_lval lv env =
   let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
-    Mmodel_analysis.must_model_lval ~bhv ~kf lv
+  Mmodel_analysis.must_model_lval ~bhv ~kf lv
 
 let must_model_vi vi env =
   let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
-    Mmodel_analysis.must_model_vi ~bhv ~kf vi
+  Mmodel_analysis.must_model_vi ~bhv ~kf vi
 
 (* }}} *)
 
 (*  ************************************************************************* *)
-(** {Analysis function calls} {{{ *)
+(* Generate analysis function calls {{{ *)
 (* ************************************************************************** *)
 
-(* Generate either
-  - [store_nblock(lhs, rhs)], or
-  - [store_nreferent(lhs, rhs)]
-function call based on the value of [flow] *)
-let mk_store_reference ~loc flow lhs rhs =
-  let fname = match flow with
-    | Direct -> "store_nblock"
-    | Indirect -> "store_nreferent"
-    | Copy -> failwith "Copy flow type in mk_store_reference"
-  in
-  Misc.mk_call ~loc (mk_api_name fname) [ Cil.mkAddrOf ~loc lhs; rhs ]
-
-(* Generate a [save_*_parameter] call *)
-let mk_save_param ~loc flow lhs pos =
-  let infix = match flow with
-    | Direct -> "nblock"
-    | Indirect -> "nreferent"
-    | Copy -> "copy"
-  in
-  let fname = "save_" ^ infix ^ "_parameter" in
-  Misc.mk_call ~loc (mk_api_name fname) [ lhs ; Cil.integer ~loc pos ]
-
-(* Generate [pull_parameter] call *)
-let mk_pull_param ~loc vi pos =
-  let exp = Cil.mkAddrOfVi vi in
-  let fname = mk_api_name "pull_parameter" in
-  let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
-  Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz  ]
-
-(* Generate [(save|pull)_return(lhs, param_no)] call *)
-let mk_handle_return_referent ?(save=true) ~loc lhs =
-  let fname = match save with
-    | true -> "save_return"
-    | false -> "pull_return"
-  in
-  (* TODO: Returning structs is unsupported so far *)
-  ignore(match (Cil.typeOf lhs) with
-    | TPtr _  -> ()
-    | _ -> failwith "Struct in return");
-  Misc.mk_call ~loc (mk_api_name fname) [ lhs ]
-
-(* Generate [reset_return()] call *)
-let mk_reset_return_referent ~loc =
-  Misc.mk_call ~loc (mk_api_name "reset_return") []
-
-(* Generate [memcpy(lhs, rhs, size)] function call assuming that [lhs = rhs]
-   represents an assignment of struct to a struct, that is, both sides are left
-   values and we need to use addressof for both sides *)
-let mk_temporal_memcpy_struct ~loc lhs rhs =
-  let fname  = mk_api_name "memcpy" in
-  let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
-  let lhs = Cil.mkAddrOf ~loc lhs in
-  Misc.mk_call ~loc fname [ lhs; rhs;  size ]
+module Mk: sig
+  (* Generate either
+      - [store_nblock(lhs, rhs)], or
+      - [store_nreferent(lhs, rhs)]
+     function call based on the value of [flow] *)
+  val store_reference: loc:location -> flow -> lval -> exp -> stmt
+
+  (* Generate a [save_*_parameter] call *)
+  val save_param: loc:location -> flow -> exp -> int -> stmt
+
+  (* Generate [pull_parameter] call *)
+  val pull_param: loc:location -> varinfo -> int -> stmt
+
+  (* Generate [(save|pull)_return(lhs, param_no)] call *)
+  val handle_return_referent: save:bool -> loc:location -> exp -> stmt
+
+  (* Generate [reset_return()] call *)
+  val reset_return_referent: loc:location -> stmt
+
+  (* Generate [memcpy(lhs, rhs, size)] function call assuming that [lhs = rhs]
+     represents an assignment of struct to a struct, that is, both sides are left
+     values and we need to use addressof for both sides *)
+  val temporal_memcpy_struct: loc:location -> lval -> exp -> stmt
+end = struct
+
+  let store_reference ~loc flow lhs rhs =
+    let fname = match flow with
+      | Direct -> "store_nblock"
+      | Indirect -> "store_nreferent"
+      | Copy -> Options.fatal "Copy flow type in store_reference"
+    in
+    Misc.mk_call ~loc (mk_api_name fname) [ Cil.mkAddrOf ~loc lhs; rhs ]
+
+  let save_param ~loc flow lhs pos =
+    let infix = match flow with
+      | Direct -> "nblock"
+      | Indirect -> "nreferent"
+      | Copy -> "copy"
+    in
+    let fname = "save_" ^ infix ^ "_parameter" in
+    Misc.mk_call ~loc (mk_api_name fname) [ lhs ; Cil.integer ~loc pos ]
+
+  let pull_param ~loc vi pos =
+    let exp = Cil.mkAddrOfVi vi in
+    let fname = mk_api_name "pull_parameter" in
+    let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
+    Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz  ]
+
+  let handle_return_referent ~save ~loc lhs =
+    let fname = match save with
+      | true -> "save_return"
+      | false -> "pull_return"
+    in
+    (* TODO: Returning structs is unsupported so far *)
+    (match (Cil.typeOf lhs) with
+      | TPtr _ -> ()
+      | _ -> Error.not_yet "Struct in return");
+    Misc.mk_call ~loc (mk_api_name fname) [ lhs ]
+
+  let reset_return_referent ~loc =
+    Misc.mk_call ~loc (mk_api_name "reset_return") []
+
+  let temporal_memcpy_struct ~loc lhs rhs =
+    let fname  = mk_api_name "memcpy" in
+    let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
+    Misc.mk_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs;  size ]
+end
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle assignments} {{{ *)
+(* Handle assignments {{{ *)
 (* ************************************************************************** *)
 
 (* Given an lvalue [lhs] representing LHS of an assignment, and an expression
-  [rhs] representing its RHS compute addresses compute a triple (l,r,f), such
-  that:
+  [rhs] representing its RHS compute triple (l,r,f), such that:
    - lval [l] and exp [r] are addresses of a pointer and a memory block, and
    - flow [f] indicates how to update the meta-data of [l] using information
     stored by [r]. The values of [f] indicate the following
      + Direct - referent number of [l] is assigned the referent number of [r]
-     + Indirect - referent number of [l] is assigned the block number of [r]
+     + Indirect - referent number of [l] is assigned the origin number of [r]
      + Copy - metadata of [r] is copied to metadata of [l] *)
-let rec assign_aux ?(ltype) lhs rhs loc =
+let assign ?(ltype) lhs rhs loc =
+  (* Do not use [Extlib.opt_conv] here, application of the [None] part should
+     not be evaluated at this point, as otherwise it will lead to an exception
+     via [Cil.typeOfLval] later *)
   let ltype = match ltype with
     | Some l -> l
     | None -> (Cil.typeOfLval lhs)
   in
-  match ltype with
+  match Cil.unrollType ltype with
   | TPtr _  ->
     let base, _ = Misc.ptr_index rhs in
     let rhs, flow =
       (match base.enode with
       | AddrOf _
       | StartOf _  -> rhs, Direct
-      | Const _  -> base, Direct
       (* Unary operator describes !, ~ or -: treat it same as Const since
          it implies integer or logical operations. This case is rare but
          happens: for instance in Gap SPEC CPU benchmark the returned pointer
          is assigned -1 (for whatever bizarre reason) *)
-      | UnOp _ -> base, Direct
+      | Const _  | UnOp _ -> base, Direct
       (* Special case for literal strings which E-ACSL rewrites into
-         global variables: take the block number of a string *)
-      | Lval(Var(vi), _) when Misc.is_generated_varinfo vi -> base, Direct
-      (* Lvalue can be of different type than a pointer, for instance for
-         the case when address is taken by value.
+         global variables: take the origin number of a string *)
+      | Lval(Var vi, _) when Misc.is_generated_varinfo vi -> base, Direct
+      (* Lvalue of a pointer type can be a cast of an integral type, for
+         instance for the case when address is taken by value (shown via the
+         following example).
            uintptr_t addr = ...;
            char *p = (char* )addr;
-         If this is the case then the analysis assumes that pointer is
-         unavailable and takes the block number of address and the referent
-         number of a pointer otherwise *)
-      | Lval(lv) ->
-        if Cil.isPointerType (Cil.typeOfLval  lv) then
+         If this is the case then the analysis takes the value of a variable. *)
+      | Lval lv ->
+        if Cil.isPointerType (Cil.unrollType (Cil.typeOfLval lv)) then
           Cil.mkAddrOf ~loc lv, Indirect
         else
           rhs, Direct
-      (* Binary operation which yields an integer (of FP) type.
+      (* Binary operation which yields an integer (or FP) type.
          Since LHS is of pointer type we assume that the whole integer
          expression computes to an address for which there is no
-         outer container, so the only thing to do is to take block number *)
+         outer container, so the only thing to do is to take origin number *)
       | BinOp(op, _, _, _) ->
-        (* Make sure there are no be pointer operations here *)
-        ignore((match op with
+        (* Make sure there are no pointer operations here *)
+        (match op with
           | MinusPI | PlusPI | IndexPI -> assert false
-          | _ -> ()));
+          | _ -> ());
         base, Direct
       | _ -> assert false)
     in Some (lhs, rhs, flow)
-  | TNamed(info, _) ->
-    assign_aux ~ltype:info.ttype lhs rhs loc
+  | TNamed _ ->
+    assert false
   | TInt _  | TFloat _  | TEnum _  -> None
-  | TComp _   ->
-    let rhs = (match rhs.enode with
+  | TComp _ ->
+    let rhs = match rhs.enode with
     | AddrOf _  -> rhs
-    | Lval(lv) -> Cil.mkAddrOf ~loc lv
-    | _ -> assert false) in
-    Some (lhs, rhs, Copy)
+    | Lval lv -> Cil.mkAddrOf ~loc lv
+    | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
+    | UnOp _ | BinOp _ | CastE _ | StartOf _ | Info _ ->
+      Options.abort "unsupported RHS %a" Printer.pp_exp rhs
+    in Some (lhs, rhs, Copy)
   (* va_list is a builtin type, we assume it has no pointers here and treat
      it as a "big" integer rather than a struct *)
   | TBuiltin_va_list _ -> None
   | TArray _ -> Some (lhs, rhs, Direct)
   (* void type should not happen as we are dealing with assignments *)
-  | TVoid _ -> failwith "Void type in assignment"
-  | TFun _ -> failwith "TFun type in assignment"
+  | TVoid _ -> Options.fatal "Void type in assignment"
+  | TFun _ -> Options.fatal "TFun type in assignment"
 
 (* Generate a statement tracking temporal metadata associated with assignment
    [lhs] = [rhs], where lhs is a left value and [rhs] is an expression. *)
 let mk_stmt_from_assign loc lhs rhs =
-  match (assign_aux lhs rhs loc) with
+  match assign lhs rhs loc with
   | Some (lhs, rhs, flow) ->
     let stmt = (match flow with
-      | Direct | Indirect ->
-        mk_store_reference ~loc flow lhs rhs
-      | Copy ->
-        mk_temporal_memcpy_struct ~loc lhs rhs)
+      | Direct | Indirect -> Mk.store_reference ~loc flow lhs rhs
+      | Copy -> Mk.temporal_memcpy_struct ~loc lhs rhs)
     in Some stmt
   | None -> None
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle Set instructions} {{{ *)
+(* Handle Set instructions {{{ *)
 (* ************************************************************************** *)
 
 (* Update local environment with a statement tracking temporal metadata
@@ -265,168 +272,181 @@ let set_instr ?(post=false) loc lhs rhs fenv =
 let set_instr ?(post=false) loc lhs rhs fenv =
   if must_model_lval lhs !fenv then
     set_instr ~post loc lhs rhs fenv
-
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle Call instructions} {{{ *)
+(* Handle Call instructions {{{ *)
 (* ************************************************************************** *)
 
-(* Track function arguments: export referents of arguments to a global
-   structure so they can be retrieved once that function is called *)
-let save_params loc args fenv =
-  List.iteri
-    (fun index param ->
-      let dummy_lv = Mem(param),NoOffset in
-      let ltype = Cil.typeOf param in
-      let vals = assign_aux ~ltype dummy_lv param loc in
-      Extlib.may
-        (fun (_, rhs, flow) ->
-          if must_model_exp param !fenv then begin
-            let stmt = mk_save_param ~loc flow rhs index in
-            fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt
-          end)
-        vals)
-    args
-
-(* Update local environment with a statement tracking temporal metadata
-   associated with assignment [ret] = [func(args)]. *)
-let call_with_ret ?(alloc=false) loc ret fenv =
-  let rhs = Cil.new_exp ~loc (Lval(ret)) in
-  let vals = assign_aux ret rhs loc in
-  (* Track referent numbers of assignments via function calls *)
-  Extlib.may
-    (fun (lhs, rhs, flow) ->
-      let flow, rhs = match flow with
-        | Indirect when alloc -> Direct, (Misc.mk_deref ~loc rhs)
-        | _ -> flow, rhs
-      in
-      let stmt =
-        if alloc then
-          mk_store_reference ~loc flow lhs rhs
-        else
-          mk_handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
-      in
-      fenv := Env.add_stmt ~before:!current_stmt ~post:true !fenv stmt)
-    vals
+module Function_call: sig
+  (* Top-level handler for Call instructions *)
+  val instr: lval option -> exp -> exp list -> location -> Env.t ref -> unit
+end = struct
+
+  (* Track function arguments: export referents of arguments to a global
+     structure so they can be retrieved once that function is called *)
+  let save_params loc args fenv =
+    List.iteri
+      (fun index param ->
+        let lv = Mem(param), NoOffset in
+        let ltype = Cil.typeOf param in
+        let vals = assign ~ltype lv param loc in
+        Extlib.may
+          (fun (_, rhs, flow) ->
+            if must_model_exp param !fenv then begin
+              let stmt = Mk.save_param ~loc flow rhs index in
+              fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt
+            end)
+          vals)
+      args
+
+  (* Update local environment with a statement tracking temporal metadata
+     associated with assignment [ret] = [func(args)]. *)
+  let call_with_ret ?(alloc=false) loc ret fenv =
+    let rhs = Cil.new_exp ~loc (Lval ret) in
+    let vals = assign ret rhs loc in
+    (* Track referent numbers of assignments via function calls.
+       Library functions (i.e., with no source code available) that return
+       values are considered to be functions that allocate memory. They are
+       considered so because they need to be handled exactly as memory
+       allocating functions, that is the referent of the returned pointer is
+       assigned the origin number associated with the return value. For
+       instance, for some [p = call();] [store_nblock( *p,..)] is appended.
+       Note that for this we need [Direct] flow and also dereference the
+       pointer to get its number. This is done in the following statement
+       (where variable [alloc] indicates whether a function is a
+       memory-allocating function or not).
+
+       Alternatively, if a function does not allocate memory and its body has
+       been instrumented, then information about referent numbers should be
+       stored in the internal data structure and it is retrieved using
+       [pull_return] added via a call to [Mk.handle_return_referent] *)
+    Extlib.may
+      (fun (lhs, rhs, flow) ->
+        let flow, rhs = match flow with
+          | Indirect when alloc -> Direct, (Misc.mk_deref ~loc rhs)
+          | _ -> flow, rhs
+        in
+        let stmt =
+          if alloc then
+            Mk.store_reference ~loc flow lhs rhs
+          else
+            Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
+        in
+        fenv := Env.add_stmt ~before:!current_stmt ~post:true !fenv stmt)
+      vals
+
+  (* Update local environment with a statement tracking temporal metadata
+     associated with memcpy/memset call *)
+  let call_memxxx loc args fname fenv =
+    if is_memcpy fname || is_memset fname then begin
+      let stmt = Misc.mk_call ~loc (mk_api_name (get_fname fname)) args in
+      fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
+    end
 
-(* Update local environment with a statement tracking temporal metadata
-   associated with a memcpy call *)
-let call_memcpy loc args fname fenv =
-  if (is_memcpy fname) then begin
-    let stmt = Misc.mk_call ~loc (mk_api_name "memcpy") args in
+  let instr ret fname args loc fenv =
+    (* 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
+       and the right parameter will be pulled at runtime. In practice, however,
+       it makes sense to make this somewhat-debug-level-call. In production mode
+       the implementation of the function should be empty and compiler should
+       be able to optimize that code out. *)
+    let stmt = Misc.mk_call ~loc (mk_api_name "reset_parameters") [] in
     fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
-  end
-
-(* Update local environment with a statement tracking temporal metadata
-   associated with a memset call. *)
-let call_memset loc args fname fenv =
-  if (is_memset fname) then begin
-    let stmt = Misc.mk_call ~loc (mk_api_name "memset") args in
+    let stmt = Mk.reset_return_referent ~loc in
     fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
-  end
-
-(* Top-level handler for Call instructions *)
-let call_instr ret fname args loc fenv =
-  (* Add function calls to reset_parameters and reset_return before each
-     function call regardless. They are is not really required, as if the
-     instrumentation is correct then the right parameters will be saved
-     and the right parameter will be pulled at runtime. In practice, however,
-     it makes sense to make this somewhat-debug-level-call. In production mode
-     the implementation of the function should be empty and compiler should
-     be able to optimize that code out. *)
-  let stmt = Misc.mk_call ~loc (mk_api_name "reset_parameters") [] in
-  fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
-  let stmt = mk_reset_return_referent ~loc in
-  fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
-  (* Push parameters with either a call to a function pointer or a function
-      definition otherwise there is no point. *)
-  if Cil.isFunctionType (Cil.typeOf fname) || has_fundef fname then begin
-    save_params loc args fenv
-  end;
-  (* Handle special cases of memcpy and memset *)
-  call_memcpy loc args fname fenv;
-  call_memset loc args fname fenv;
-  let alloc = is_alloc fname || not (has_fundef fname) in
-  Extlib.may
-    (fun lhs ->
-      if must_model_lval lhs !fenv then call_with_ret ~alloc loc lhs fenv)
-    ret
+    (* Push parameters with either a call to a function pointer or a function
+        definition otherwise there is no point. *)
+    if Cil.isFunctionType (Cil.typeOf fname) || has_fundef fname then begin
+      save_params loc args fenv
+    end;
+    (* Handle special cases of memcpy/memset *)
+    call_memxxx loc args fname fenv;
+    let alloc = is_alloc fname || not (has_fundef fname) in
+    Extlib.may
+      (fun lhs ->
+        if must_model_lval lhs !fenv then call_with_ret ~alloc loc lhs fenv)
+      ret
+end
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle Local_init instructions} {{{ *)
+(* Handle Local_init instructions {{{ *)
 (* ************************************************************************** *)
-let rec handle_local_init_aux ?(offset=NoOffset) loc vi init fenv =
-  match init with
-  | SingleInit(exp) ->
-    set_instr ~post:true loc (Var(vi), offset) exp fenv
-  | CompoundInit(_, inits) ->
-    List.iter
-      (fun (off, init) ->
-        let off = Cil.addOffset off offset in
-        handle_local_init_aux ~offset:off loc vi init fenv)
-      inits
-
-let handle_local_init loc vi init fenv =
-  handle_local_init_aux loc vi init fenv
-
-let local_init_instr vi li loc fenv =
-  match li with
-  | AssignInit(init) ->
-    handle_local_init loc vi init fenv
-  | ConsInit(fname, args, _) ->
-    let ret = Some (Var(vi), NoOffset) in
-    let fname = Cil.evar ~loc fname in
-    call_instr ret fname args loc fenv
-
-(* Top-level handler for Local_init instructions *)
-let local_init_instr vi li loc fenv =
-  if must_model_vi vi !fenv then
-    local_init_instr vi li loc fenv
+module Local_init: sig
+  (* Top-level handler for Local_init instructions *)
+  val instr: varinfo -> local_init -> location -> Env.t ref -> unit
+end = struct
+
+  let rec handle_init offset loc vi init fenv =
+    match init with
+    | SingleInit exp ->
+      set_instr ~post:true loc (Var vi, offset) exp fenv
+    | CompoundInit(_, inits) ->
+      List.iter
+        (fun (off, init) ->
+          let offset = Cil.addOffset off offset in
+          handle_init offset loc vi init fenv)
+        inits
+
+  let instr vi li loc fenv =
+    match li with
+    | AssignInit init ->
+      handle_init NoOffset loc vi init fenv
+    | ConsInit(fname, args, _) ->
+      let ret = Some (Cil.var vi) in
+      let fname = Cil.evar ~loc fname in
+      Function_call.instr ret fname args loc fenv
+
+  let instr vi li loc fenv =
+    if must_model_vi vi !fenv then
+      instr vi li loc fenv
+end
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Track function arguments} {{{ *)
+(* Track function arguments {{{ *)
 (* ************************************************************************** *)
 
 (* Update local environment with a statement tracking temporal metadata
    associated with adding a function argument to a stack frame *)
-let rec track_argument ?(typ) param index env =
+let track_argument ?(typ) param index env =
   let typ = Extlib.opt_conv param.vtype typ in
-  match typ with
+  match Cil.unrollType typ with
   | TPtr _
   | TComp _ ->
-    let stmt = mk_pull_param ~loc:Location.unknown param index in
+    let stmt = Mk.pull_param ~loc:Location.unknown param index in
     Env.add_stmt ~post:false env stmt
   | TInt _ | TFloat _ | TEnum _ | TBuiltin_va_list _ -> env
-  | TNamed(info, _) ->
-    track_argument ~typ:info.ttype param index env
-  | _ -> failwith "Failed to handle function parameter"
+  | TNamed _ -> assert false
+  | TVoid _ |TArray _ | TFun _ ->
+    Options.fatal "Failed to handle function parameter"
 (* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle return statements} {{{ *)
+(* Handle return statements {{{ *)
 (* ************************************************************************** *)
 
 (* Update local environment [fenv] with statements tracking return value
    of a function. *)
 let handle_return_stmt loc ret fenv =
   match ret.enode with
-  | Lval(lv) ->
+  | Lval lv ->
     if Cil.isPointerType (Cil.typeOfLval lv) then begin
       let exp = Cil.mkAddrOf ~loc lv in
-      let stmt = mk_handle_return_referent ~loc ~save:true exp in
+      let stmt = Mk.handle_return_referent ~loc ~save:true exp in
       fenv := Env.add_stmt ~post:false !fenv stmt
     end
-  | _ -> failwith "Something other than Lval in return"
+  | _ -> Options.fatal "Something other than Lval in return"
 
 let handle_return_stmt loc ret fenv =
   if must_model_exp ret !fenv then
     handle_return_stmt loc ret fenv
+(* }}} *)
 
 (* ************************************************************************** *)
-(** {Handle instructions} {{{ *)
+(* Handle instructions {{{ *)
 (* ************************************************************************** *)
 
 (* Update local environment [fenv] with statements tracking
@@ -436,68 +456,70 @@ let handle_instruction instr fenv =
   | Set(lv, exp, loc) ->
     set_instr loc lv exp fenv
   | Call(ret, fname, args, loc) ->
-    call_instr ret fname args loc fenv
+    Function_call.instr ret fname args loc fenv
   | Local_init(vi, li, loc) ->
-    local_init_instr vi li loc fenv
-  | Asm _ | Skip _ -> ()
-  | Code_annot _ -> failwith "Code_annot is not supported"
-
+    Local_init.instr vi li loc fenv
+  | Asm _ -> Options.warning ~once:true ~current:true "@[Analysis is\
+potentially incorrect in presence of assembly code.@]";
+  | Skip _ -> ()
+  | Code_annot _ -> ()
+(* }}} *)
 
 (* ************************************************************************** *)
-(** {Initialization of globals} {{{ *)
+(* Initialization of globals {{{ *)
 (* ************************************************************************** *)
+
 (* Provided that [vi] is a global variable initialized by the initializer [init]
    at offset [off] return [Some stmt], where [stmt] is a statement
    tracking that initialization. If [init] does not need to be tracked than
    the return value is [None] *)
-let mk_global_init vi off init env =
+let mk_global_init ~loc vi off init env =
   let exp = match init with
-    | SingleInit(e) -> e
+    | SingleInit e -> e
     (* Compound initializers should have been thrown away at this point *)
-    | _ -> failwith "Unexpected ComppoundInit in global initializer"
+    | _ -> Options.fatal "Unexpected ComppoundInit in global initializer"
   in
   (* Initializer expression can be a literal string, so look up the
      corresponding variable which that literal string has been converted to *)
-  let exp = (try
-    let rec get_string e = match e.enode with
+  let exp =
+    try let rec get_string e = match e.enode with
       | Const(CStr str) -> str
       | CastE(_, exp) -> get_string exp
       | _ -> raise Not_found
     in
     let str = get_string exp in
-    Cil.evar ~loc:Location.unknown (Literal_strings.find str)
+    Cil.evar ~loc (Literal_strings.find str)
   with
     (* Not a literal string: just use the expression at hand *)
-    Not_found -> exp)
+    Not_found -> exp
   in
   (* The input [vi] is from the old project, so get the corresponding variable
      from the new one, otherwise AST integrity is violated *)
   let vi = Cil.get_varinfo (Env.get_behavior env) vi in
-  let lv = (Var(vi), off) in
-  mk_stmt_from_assign Location.unknown lv exp
+  let lv = Var vi, off in
+  mk_stmt_from_assign loc lv exp
+(* }}} *)
 
 (* ************************************************************************** *)
-(** {Public API} {{{ *)
+(* Public API {{{ *)
 (* ************************************************************************** *)
 
-let enable param =
-  generate := param
+let enable param = generate := param
 
-let is_enabled () =
-  !generate
+let is_enabled () = !generate
 
 let handle_arguments kf env =
   if is_enabled () then
-    let getpar = Cil.get_varinfo (Env.get_behavior env) in
-    let formals = List.map getpar (Kernel_function.get_formals kf) in
     let env, _ = List.fold_left
       (fun (env, index) param ->
-        if Mmodel_analysis.must_model_vi ~kf param then
-          track_argument param index env, index + 1
-        else
-          env, index + 1)
+        let param = Cil.get_varinfo (Env.get_behavior env) param in
+        let env =
+          if Mmodel_analysis.must_model_vi ~kf param then
+            track_argument param index env
+          else env
+        in env, index + 1)
       (env, 0)
-      formals
+      (Kernel_function.get_formals kf)
     in env
   else
     env
@@ -507,11 +529,13 @@ let handle_stmt stmt env =
     current_stmt := stmt;
     let fenv = ref env in
     (match stmt.skind with
-    | Instr(instr) ->
+    | Instr instr ->
       handle_instruction instr fenv
     | Return(ret, loc) ->
       Extlib.may (fun ret -> handle_return_stmt loc ret fenv) ret
-    | _ -> ());
+    | Goto _ | Break _ | Continue _ | If _ | Switch _ | Loop _ | Block _
+    | UnspecifiedSequence _ | Throw _ | TryCatch _ | TryFinally _
+    | TryExcept _ -> ());
     current_stmt := Cil.dummyStmt;
     !fenv
   end else
@@ -519,8 +543,7 @@ let handle_stmt stmt env =
 
 let handle_global_init vi off init env =
   if is_enabled () then
-    mk_global_init vi off init env
+    mk_global_init ~loc:vi.vdecl vi off init env
   else
     None
-
 (* }}} *)
diff --git a/src/plugins/e-acsl/temporal.mli b/src/plugins/e-acsl/temporal.mli
index 9225abf9c3753fa10c33f876fe3d282d32b5d213..de424624f3cf51619e4f42057a825ba65f6a3824 100644
--- a/src/plugins/e-acsl/temporal.mli
+++ b/src/plugins/e-acsl/temporal.mli
@@ -20,6 +20,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Transformations to detect temporal memory errors (e.g., derererence of
+    stale pointers). Detailed description of the transformations is presented
+    in Sections 2 and 3 of the RV'17 paper "Runtime Detection of Temporal Memory
+    Errors" by K. Vorobyov, N. Kosmatov, J Signoles and A. Jakobsson.
+*)
+
 val enable: bool -> unit
 (** Enable/disable temporal transformations *)
 
@@ -28,7 +34,10 @@ val is_enabled: unit -> bool
 
 val handle_arguments: Cil_types.kernel_function -> Env.t -> Env.t
 (** Update local environment ([Env.t]) with statements allowing to track
-    referent numbers across function calls *)
+    referent numbers across calls function whose definitions are available.
+    This is such that whenever a function [f] is called (and a new stack
+    frame is created) [handle_arguments] generates statements that transfer
+    referent numbers stored in RTL to the new stack frame. *)
 
 val handle_stmt: Cil_types.stmt -> Env.t -> Env.t
 (** Update local environment ([Env.t]) with statements tracking temporal
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
new file mode 100644
index 0000000000000000000000000000000000000000..079bed7a28295221323d50ca01b10c69ad4fdb27
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
@@ -0,0 +1,36 @@
+/* Generated by Frama-C */
+#include "stdint.h"
+#include "stdlib.h"
+int main(int argc, char **argv)
+{
+  int __retres;
+  char *p;
+  int *q;
+  __e_acsl_memory_init(& argc,& argv,(size_t)8);
+  __e_acsl_store_block((void *)(& q),(size_t)8);
+  __e_acsl_store_block((void *)(& p),(size_t)8);
+  uintptr_t addr = (unsigned long)(& argc);
+  __e_acsl_store_block((void *)(& addr),(size_t)8);
+  __e_acsl_full_init((void *)(& addr));
+  __e_acsl_temporal_store_nblock((void *)(& q),(void *)(& argc));
+  __e_acsl_full_init((void *)(& q));
+  q = & argc;
+  __e_acsl_temporal_store_nblock((void *)(& p),(void *)((char *)addr));
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)addr;
+  __e_acsl_temporal_store_nblock((void *)(& p),(void *)0x123456);
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)0x123456;
+  __e_acsl_temporal_store_nreferent((void *)(& p),(void *)(& q));
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)q;
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& argc));
+  __e_acsl_delete_block((void *)(& q));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_delete_block((void *)(& addr));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
new file mode 100644
index 0000000000000000000000000000000000000000..562cc4e026c35f45fdeb94e9e2c0b3aa32a65bf2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
@@ -0,0 +1,18 @@
+/* run.config
+  COMMENT: Case when a pointer is taking address by value.
+*/
+
+#include <stdint.h>
+
+int main (int argc, char **argv) {
+  uintptr_t addr = (uintptr_t)&argc;
+  char *p;
+  int *q;
+  q = &argc;
+  /* Here the referent of p should be assigned from the value of addr */
+  p = (char*)addr;
+  p = (char*)0x123456;
+  p = (char*)q;
+}
+
+
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 91a22644d4de57561c6c2a3b2300ce3bfd3998f3..de3806a0d62284a1bc1aae55c6eddf024b1ac412 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -206,6 +206,8 @@ class e_acsl_visitor prj generate = object (self)
                     :: stmts)
                   stmts
               in
+              let return =
+                Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
               (* Generate init statements for temporal analysis *)
               let tinit_stmts = Varinfo.Hashtbl.fold
                 (fun vi (off, init) acc ->
@@ -215,11 +217,9 @@ class e_acsl_visitor prj generate = object (self)
                       (match stmt with | Some stmt -> stmt :: acc | None -> acc)
                   | None -> acc)
                 global_vars
-                []
+                [return]
               in
-              let return =
-                Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
-              let stmts = stmts @ tinit_stmts @ [return] in
+              let stmts = stmts @ tinit_stmts in
               (* Create a new code block with generated statements *)
               let (b, env), stmts = match stmts with
                 | [] -> assert false
@@ -601,7 +601,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
           let env = Temporal.handle_stmt stmt env in
           (* Add initialization statements and store_block statements stemming
              from Local_init *)
-            self#add_initializers stmt env kf
+            self#handle_instructions stmt env kf
         else
           env
       in
@@ -727,47 +727,40 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     in
     Cil.ChangeDoChildrenPost(stmt, mk_block)
 
-  method private add_initializer loc ?vi lv ?(post=false) stmt env kf =
-    assert generate;
-    let may_safely_ignore = function
-      | Var vi, NoOffset -> vi.vglob || vi.vformal
-      | _ -> false
-    in
-    if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~kf lv then
-      let before = Cil.memo_stmt self#behavior stmt in
-      let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
-      let new_stmt = Cil.memo_stmt self#behavior new_stmt in
-      let env = Env.add_stmt ~post ~before env new_stmt in
-      let env = match vi with
-        | None -> env
-        | Some vi ->
-          let new_stmt = Project.on prj Misc.mk_store_stmt vi in
-          let new_stmt = Cil.memo_stmt self#behavior new_stmt in
-          Env.add_stmt ~post ~before env new_stmt
+  method private handle_instructions stmt env kf =
+    let add_initializer loc ?vi lv ?(post=false) stmt env kf =
+      assert generate;
+      let may_safely_ignore = function
+        | Var vi, NoOffset -> vi.vglob || vi.vformal
+        | _ -> false
       in
-      env
-    else
-      env
-
-  method private add_initializers stmt env kf =
-    let do_instr instr =
-      match instr with
-      | Set(lv, _, loc) ->
-        self#add_initializer loc lv stmt env kf
-      | Local_init(vi, _, loc) ->
-        let lv = (Var(vi), NoOffset) in
-        self#add_initializer loc ~vi lv ~post:true stmt env kf
-      | Call (Some lv, _, _, loc) ->
-        if not (Misc.is_generated_kf kf) then
-          self#add_initializer loc lv ~post:false stmt env kf
-        else env
-      | _ -> env
+      if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~stmt ~kf lv then
+        let before = Cil.memo_stmt self#behavior stmt in
+        let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
+        let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+        let env = Env.add_stmt ~post ~before env new_stmt in
+        let env = match vi with
+          | None -> env
+          | Some vi ->
+            let new_stmt = Project.on prj Misc.mk_store_stmt vi in
+            let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+            Env.add_stmt ~post ~before env new_stmt
+        in
+        env
+      else
+        env
     in
     match stmt.skind with
-    | Instr(i) -> do_instr i
+    | Instr(Set(lv, _, loc)) -> add_initializer loc lv stmt env kf
+    | Instr(Local_init(vi, _, loc)) ->
+      let lv = (Var(vi), NoOffset) in
+      add_initializer loc ~vi lv ~post:true stmt env kf
+    | Instr(Call (Some lv, _, _, loc)) ->
+      if not (Misc.is_generated_kf kf) then
+        add_initializer loc lv ~post:false stmt env kf
+      else env
     | _ -> env
 
-
   method !vblock blk =
     let handle_memory new_blk =
       match new_blk.blocals with