diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index a8eaf9900a164049d70e4a928ecf5b94f39b0efc..2557e2ab29c89ee90e398b8da1a04ced1731241c 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -184,46 +184,64 @@ module TransferTaint = struct
   (* No update about taint wrt information provided by the other domains. *)
   let update _valuation state = `Value state
 
+  (* Given a lvalue, returns:
+     - its memory location (as a zone);
+     - its indirect dependencies, i.e. the memory zone its location depends on;
+     - whether its location is a singleton. *)
+  let compute_zones lval to_loc =
+    match lval with
+    | Var vi, NoOffset ->
+      (* Special case for direct access to variable: do not use [to_loc] here,
+         as it will fail for the formal parameters of calls. *)
+      let zone = Locations.zone_of_varinfo vi in
+      zone, Zone.bottom, true
+    | _ ->
+      let ploc = to_loc lval in
+      let singleton = Precise_locs.cardinal_zero_or_one ploc in
+      let lv_zone =
+        let loc = Precise_locs.imprecise_location ploc in
+        Locations.enumerate_valid_bits Write loc
+      in
+      let lv_indirect_zone = Value_util.indirect_zone_of_lval to_loc lval in
+      lv_zone, lv_indirect_zone, singleton
+
+  (* Propagates data- and control-taints for an assignement [lval = exp]. *)
+  let assign_aux lval exp to_loc state =
+    let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in
+    let exp_zone = Value_util.zone_of_expr to_loc exp in
+    (* [lv] becomes data-tainted if a memory location on which the value of
+       [exp] depends on is data-tainted. *)
+    let data_tainted = Zone.intersects state.locs_data exp_zone in
+    (* [lv] becomes control-tainted if:
+       - the current call depends on a tainted assume statements of a caller;
+       - the execution of the assignment depends on a tainted assume statement;
+       - the value of [exp] is control-tainted;
+       - the assigned location depends on tainted values. *)
+    let ctrl_tainted =
+      state.dependent_call
+      || not (Stmt.Set.is_empty state.assume_stmts)
+      || Zone.intersects state.locs_control exp_zone
+      || LatticeTaint.intersects state lv_indirect_zone
+    in
+    let update tainted locs =
+      if tainted
+      then Zone.join locs lv_zone
+      else if singleton
+      then Zone.diff locs lv_zone
+      else locs
+    in
+    { state with locs_data = update data_tainted state.locs_data;
+                 locs_control = update ctrl_tainted state.locs_control; }
+
   let assign ki lv exp _v valuation state =
     let state =
       match ki with
       | Kglobal ->
         state
       | Kstmt stmt ->
-        let to_loc = loc_of_lval valuation in
-        let ploc = to_loc lv.Eval.lval in
-        let lv_zone =
-          let loc = Precise_locs.imprecise_location ploc in
-          Locations.enumerate_valid_bits Write loc
-        in
         let state = filter_active_tainted_assumes stmt state in
-        (* Control-dependency: taint the left-value of an assign statement whose
-           execution depends on the value of a tainted assume statement. *)
-        let state =
-          if not state.dependent_call && Stmt.Set.is_empty state.assume_stmts
-          then
-            (* No active tainted assume statement means that there is no
-               control-dependecy that applies on [lv]. *)
-            state
-          else
-            { state with locs_control = Zone.join state.locs_control lv_zone }
-        in
-        (* Compute data-dependency with [state]: whenever [exp] (or its
-           sub-expressions) is tainted, or [lv] is indexed by a tainted memory
-           location. *)
-        let exp_zone = Value_util.zone_of_expr to_loc exp in
-        let lv_indirect_zone =
-          Value_util.indirect_zone_of_lval to_loc lv.Eval.lval
-        in
-        let intersect_state =
-          LatticeTaint.intersects state exp_zone ||
-          LatticeTaint.intersects state lv_indirect_zone
-        in
-        if intersect_state
-        then { state with locs_data = Zone.join state.locs_data lv_zone }
-        else if Precise_locs.cardinal_zero_or_one ploc
-        then { state with locs_data = Zone.diff state.locs_data lv_zone }
-        else state
+        let to_loc = loc_of_lval valuation in
+        assign_aux lv.Eval.lval exp to_loc state
     in
     `Value state
 
@@ -250,11 +268,7 @@ module TransferTaint = struct
       let to_loc = loc_of_lval valuation in
       List.fold_left
         (fun s { Eval.concrete; formal; _ } ->
-           let concrete_zone = Value_util.zone_of_expr to_loc concrete in
-           let formal_zone = Locations.zone_of_varinfo formal in
-           if LatticeTaint.intersects state concrete_zone
-           then { s with locs_data = Zone.join s.locs_data formal_zone }
-           else s)
+           assign_aux (Cil.var formal) concrete to_loc s)
         state
         call.Eval.arguments
     in