diff --git a/Makefile b/Makefile
index 977133d5e9174b99399ca09663454ca41ffe7830..9e3ac8f0cafacd58b0c57683ce897f7783cb62fa 100644
--- a/Makefile
+++ b/Makefile
@@ -861,7 +861,7 @@ endif
 
 # General rules for ordering files within PLUGIN_CMO:
 # - try to keep the legacy Value before Eva
-PLUGIN_CMO:= partitioning/split_strategy value_parameters \
+PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
 	utils/value_perf utils/eva_annotations \
 	utils/value_util utils/red_statuses \
 	utils/mark_noresults \
diff --git a/doc/value/main.tex b/doc/value/main.tex
index dd2d364f61eeca2ee6cb90b14e125fd39e523282..96d66840582568d5262abe620678ac86a58c9c23 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3904,7 +3904,7 @@ with large arrays and matrices, it is worth considering its usage.
 \label{sec:eva}
 
 
-Starting from \FramaC Silicon, new analysis \emph{domains} are
+This section presents the analysis \emph{domains}
 available to improve the precision on specific code constructs.
 They can (and probably should) be enabled at the beginning of the analysis.
 Their only downside is that they increase the analysis time.
@@ -3913,7 +3913,21 @@ These analysis domains are enabled by the option \texttt{-eva-domains}, followed
 by a list of domain names. A list of the available domains, and a short
 description of each one, can be displayed with \texttt{-eva-domains help}.
 
-\emph{Restrictions:}
+Domains can also be enabled for specific functions through option
+\texttt{-eva-domains-function}:
+\begin{itemize}
+\item \texttt{-eva-domains-function d1:f,d1:g,d2:h} enables the domain
+  \texttt{d1} on functions \lstinline+f+ and \lstinline+g+, and the domain
+  \texttt{d2} on function \lstinline+h+.
+\item \texttt{-eva-domains-function d:f+} enables the domain
+  \texttt{d} on function \lstinline+f+ and on any function called
+  from \lstinline+f+.
+\item \texttt{-eva-domains-function d:f-} disables the domain
+  \texttt{d} on function \lstinline+f+ and on any function called
+  from \lstinline+f+.
+\end{itemize}
+
+These analysis domains currently have some restrictions:
 \begin{itemize}
 \item adding a new domain may interact with the \lstinline+slevel+ partitioning
   in unpredictable ways, and new alarms may sometimes appear;
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2ada5971dd26cf43899de59b063ce5ae0a7d88f5..9c669cda9390d35e43e048e6019ba9aa82c09c84 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1224,6 +1224,8 @@ src/plugins/value/domains/cvalue/locals_scoping.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/cvalue/locals_scoping.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/cvalue/warn.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/cvalue/warn.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/domain_mode.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/domain_mode.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/domain_builder.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/domain_builder.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/domain_lift.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index df7e17c543eec3539b3d37cca378284a673cbfe8..c6093135e2a977f3e25c1e8ccea6dc94977a6b66 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -134,7 +134,8 @@ module type Queries = sig
       - a value for the expression, which can be:
         – `Bottom if its evaluation is infeasible;
         – `Value (v, o) where [v] is an over-approximation of the abstract
-           value of the expression [exp], and [o] is the origin of the value. *)
+           value of the expression [exp], and [o] is the origin of the value,
+           which can be None. *)
 
   (** Query function for compound expressions:
       [eval oracle t exp] returns the known value of [exp] by the state [t].
@@ -143,14 +144,14 @@ module type Queries = sig
       No recursive evaluation should be done by this function. *)
   val extract_expr :
     (exp -> value evaluated) ->
-    state -> exp -> (value * origin) evaluated
+    state -> exp -> (value * origin option) evaluated
 
   (** Query function for lvalues:
       [find oracle t lval typ loc] returns the known value stored at
       the location [loc] of the left value [lval] of type [typ]. *)
   val extract_lval :
     (exp -> value evaluated) ->
-    state -> lval -> typ -> location -> (value * origin) evaluated
+    state -> lval -> typ -> location -> (value * origin option) evaluated
 
   (** [backward_location state lval typ loc v] reduces the location [loc] of the
       lvalue [lval] of type [typ], so that only the locations that may have value
@@ -357,12 +358,13 @@ module type S = sig
   (** Logical evaluation. This API is subject to changes. *)
   (* TODO: cooperative evaluation of predicates in the engine. *)
 
-  (** [logic_assign from loc_asgn pre state] applies the effect of the
-      [assigns ... \from ...] clause [from] to [state]. [pre] is the state
-      before the assign clauses, in which the terms of the clause are evaluated.
-      [loc_asgn] is the result of the evaluation of the [assigns] part of [from]
-      in [pre]. *)
-  val logic_assign: logic_assign -> location -> pre:state -> state -> state
+  (** [logic_assign None loc state] removes from [state] all inferred properties
+      that depend on the memory location [loc].
+      If the first argument is not None, it contains the logical clause being
+      interpreted and the pre-state in which the terms of the clause are
+      evaluated. The clause can be an assigns, allocates or frees clause.
+      [loc] is then the memory location concerned by the clause. *)
+  val logic_assign: (logic_assign * state) option -> location -> state -> state
 
   (** Evaluates a [predicate] to a logical status in the current [state].
       The [logic_environment] contains the states at some labels and the
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 8915d40c396f57aaf97140bb23e241066397d70f..c21820f2b2dfa19d7132a2b9f646c38321d72881 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -360,7 +360,7 @@ module Make (Man : Input) = struct
   type state = Man.t Abstract1.t
   type value = Main_values.Interval.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   let man = Man.manager
   let log_category = dkey
@@ -463,7 +463,7 @@ module Make (Man : Input) = struct
   let dummy_oracle _ exn = raise exn
 
   let compute state expr typ =
-    let top = `Value (None, ()), Alarmset.all in
+    let top = `Value (None, None), Alarmset.all in
     if not (is_relevant expr)
     then top
     else
@@ -476,7 +476,7 @@ module Make (Man : Input) = struct
         let value =
           if Interval.is_bottom interval
           then `Bottom
-          else `Value (interval_to_ival interval, ())
+          else `Value (interval_to_ival interval, None)
         in
         (* TODO: remove alarms if computation does not overflow *)
         value, Alarmset.all
@@ -673,7 +673,7 @@ module Make (Man : Input) = struct
 
   let show_expr _valuation _state _fmt _expr = ()
 
-  let logic_assign _assigns location ~pre:_ state = kill_bases location state
+  let logic_assign _assigns location state = kill_bases location state
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 811a00dd6b09360cc96c1b58561035a402d0e79b..5257e966b8729ffd4b3223a17080b80706964655 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -38,7 +38,7 @@ module Model = struct
      lvalue can be incomparable. The origin is then used to store the value from
      the state, to later choose which value to keep. This is done by the update
      function in cvalue_transfer. *)
-  type origin = value option
+  type origin = value
 
   let extract_expr _ _ _ = `Value (Cvalue.V.top, None), Alarmset.all
 
@@ -308,15 +308,19 @@ module State = struct
           Printer.pp_from assign pp_eval_error e;
         Cvalue.V.top
 
-  let logic_assign logic_assign location ~pre:(pre_state, _) (state, sclob) =
+  let logic_assign logic_assign location (state, sclob) =
     match logic_assign with
-    | Assigns assign ->
+    | None ->
+      let location = Precise_locs.imprecise_location location
+      and value = Cvalue.V.top in
+      Cvalue.Model.add_binding ~exact:false state location value, sclob
+    | Some (Assigns assign, (pre_state, _)) ->
       let location = Precise_locs.imprecise_location location in
       let env = Eval_terms.env_assigns pre_state in
       let value = evaluate_from_clause env assign in
       Locals_scoping.remember_if_locals_in_value sclob location value;
       Cvalue.Model.add_binding ~exact:false state location value, sclob
-    | Frees _ | Allocates _ -> state, sclob
+    | Some ((Frees _ | Allocates _), _) -> state, sclob
 
   (* ------------------------------------------------------------------------ *)
   (*                             Initialization                               *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 540f2ec4bd4927c1b91585eb4ec1a46d1f3b3355..94bb435e1011082f6a365b22399e8612f0b2355b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -25,7 +25,7 @@ open Eval
 open Cvalue.Model
 
 type value = Main_values.CVal.t
-type origin = value option
+type origin = value
 type location = Main_locations.PLoc.location
 
 let unbottomize = function
@@ -71,7 +71,7 @@ let update valuation t =
              included in the other). We use some notion of cardinality of
              abstract values to choose the best value to keep. *)
           match record.origin with
-          | Some (Some previous_v) ->
+          | Some previous_v ->
             let typ = Cil.typeOfLval lv in
             if is_smaller_value typ v previous_v then v else previous_v
           | _ -> v
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.mli b/src/plugins/value/domains/cvalue/cvalue_transfer.mli
index d9f23bf0ff20793c38529bdb71d38c9895d01c77..b74f2266bebc6c722c9ae1c946c947b47a20e752 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.mli
@@ -23,7 +23,7 @@
 (** Transfer functions for the main domain of the Value analysis. *)
 
 type value = Main_values.CVal.t
-type origin = value option
+type origin = value
 type location = Main_locations.PLoc.location
 
 include Abstract_domain.Transfer
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 83e734a69f51032108eaefc831f4cd2385762b03..af877385426edb598dce3e2d4bcdd901c516bf19 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -20,7 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
 module type InputDomain = sig
   include Abstract_domain.S
   val storage: unit -> bool
@@ -65,11 +64,11 @@ module Make_Minimal
   type value = Value.t
   type location = Location.location
   type state = Domain.t
-  type origin = unit
+  type origin
 
   let narrow x _y = `Value x
 
-  let top_answer = `Value (Value.top, ()), Alarmset.all
+  let top_answer = `Value (Value.top, None), Alarmset.all
   let extract_expr _oracle _state _expr = top_answer
   let extract_lval _oracle _state _lval _typ _location = top_answer
   let backward_location _state _lval _typ location value = `Value (location, value)
@@ -102,7 +101,7 @@ module Make_Minimal
     let lval = Cil.var varinfo in
     Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
 
-  let logic_assign _assigns _location ~pre:_ _state = top
+  let logic_assign _assigns _location _state = top
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ t _ _ = `Value t
 
@@ -184,16 +183,19 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
     type value = Cvalue.V.t
     type location = Precise_locs.precise_location
     type state = Domain.t
-    type origin = unit
+    type origin
 
     let narrow x _y = `Value x
 
     let extract_expr _oracle state expr =
-      let v = Domain.extract_expr state expr >>-: fun v -> v, () in
+      let v = Domain.extract_expr state expr >>-: fun v -> v, None in
       v, Alarmset.all
 
     let extract_lval _oracle state lval typ location =
-      let v = Domain.extract_lval state lval typ location >>-: fun v -> v, () in
+      let v =
+        Domain.extract_lval state lval typ location >>-: fun v ->
+        v, None
+      in
       v, Alarmset.all
 
     let backward_location _state _lval _typ location value =
@@ -236,7 +238,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
       let lval = Cil.var varinfo in
       Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
 
-    let logic_assign _assigns _location ~pre:_ _state = top
+    let logic_assign _assigns _location _state = top
     let evaluate_predicate _ _ _ = Alarmset.Unknown
     let reduce_by_predicate _ t _ _ = `Value t
 
@@ -249,3 +251,350 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
 
   include Complete (D)
 end
+
+(* -------------------------------------------------------------------------- *)
+
+module Restrict
+    (Value: Abstract_value.S)
+    (Domain: Abstract.Domain.Internal with type value = Value.t)
+    (Scope: sig val functions: Domain_mode.function_mode list end)
+= struct
+
+  open Domain_mode
+
+  (* Defines the join and the narrow of different modes. *)
+  module Mode = struct
+    include Mode
+
+    let merge f m1 m2 =
+      let merge_perm p1 p2 =
+        { read = f p1.read p2.read;
+          write = f p1.write p2.write; }
+      in
+      { current = merge_perm m1.current m2.current;
+        calls = merge_perm m1.calls m2.calls; }
+
+    let join = merge (&&)
+    let narrow = merge (||)
+  end
+
+  (* Map that binds functions to their analysis mode. *)
+  let functions_map =
+    List.fold_left
+      (fun map (kf, mode) -> Kernel_function.Map.add kf mode map)
+      Kernel_function.Map.empty Scope.functions
+
+  (* This module propagates states of type [(state * mode) option]:
+     - None is propagated as long as no functions from [Scope.functions]
+       are analyzed.
+     - then the current [mode] is propagated alongside the state. Queries and
+       transfer functions are applied accordingly. The current mode is replaced
+       at function calls by [mode.calls]. *)
+
+  module Info = struct let module_name = Domain.name ^ " restricted" end
+  module D = Datatype.Pair_with_collections (Domain) (Mode) (Info)
+
+  module I = struct let module_name = Domain.name ^ " option" end
+  include Datatype.Option_with_collections (D) (I)
+
+  let default = Domain.top, Mode.all
+  let structure: t Abstract.Domain.structure =
+    Abstract.Domain.(Option ((Node (Domain.structure, Void)), default))
+
+  type state = t
+  type value = Domain.value
+  type location = Domain.location
+  type origin = Domain.origin
+
+  let get_state = function
+    | None -> Domain.top
+    | Some (state, _mode) -> state
+
+  (* When the first function from [Scope.functions] is encountered, starts the
+     analysis with the state computed by this function. It is an empty state in
+     which the global variables exist and may have any values. *)
+  let compute_starting_state () =
+    let empty = Domain.empty () in
+    let var_kind = Abstract_domain.Global in
+    let init varinfo _init state =
+      let state = Domain.enter_scope var_kind [varinfo] state in
+      Domain.initialize_variable_using_type var_kind varinfo state
+    in
+    Globals.Vars.fold init empty
+
+  (* Do not recompute each time the starting state. Do not compute the starting
+     state too early either, in case it depends on analysis options. *)
+  let get_starting_state =
+    let starting_state = ref None in
+    fun () ->
+      match !starting_state with
+      | None ->
+        let s = compute_starting_state () in
+        starting_state := Some s;
+        s
+      | Some state -> state
+
+  (* ----- Lattice ---------------------------------------------------------- *)
+
+  let top = None
+
+  let is_included x y =
+    match x, y with
+    | _, None -> true
+    | None, _ -> false
+    | Some (d1, _), Some (d2, _) -> Domain.is_included d1 d2
+
+  let make_join join = fun x y ->
+    match x, y with
+    | None, _ | _, None -> None
+    | Some (d1, m1), Some (d2, m2) -> Some (join d1 d2, Mode.join m1 m2)
+
+  let join = make_join Domain.join
+  let widen kf stmt = make_join (Domain.widen kf stmt)
+
+  let narrow x y =
+    match x, y with
+    | None, s | s, None -> `Value s
+    | Some (d1, s1), Some (d2, s2) ->
+      Domain.narrow d1 d2 >>-: fun s ->
+      Some (s, Mode.narrow s1 s2)
+
+  (* ----- Queries ---------------------------------------------------------- *)
+
+  (* Applies the [query] only if the current mode allows the domain to read.
+     Otherwise, returns [default]. *)
+  let make_query default query = function
+    | None -> default
+    | Some (state, mode) ->
+      if mode.current.read
+      then query state
+      else default
+
+  let default_query = `Value (Value.top, None), Alarmset.all
+
+  let extract_expr oracle state expr =
+    make_query default_query (fun s -> Domain.extract_expr oracle s expr) state
+
+  let extract_lval oracle state lval typ location =
+    make_query
+      default_query
+      (fun s -> Domain.extract_lval oracle s lval typ location)
+      state
+
+  let backward_location state lval typ location value =
+    make_query
+      (`Value (location, value))
+      (fun s -> Domain.backward_location s lval typ location value)
+      state
+
+  let reduce_further state expr value =
+    make_query [] (fun s -> Domain.reduce_further s expr value) state
+
+  (* ----- Transfer functions ----------------------------------------------- *)
+
+  (* Applies the transfer function [f] only if the current mode allows the
+     domain to write. Otherwise, returns the state unchanged. *)
+  let make_transfer f = function
+    | None -> `Value None
+    | Some (state, mode) ->
+      if mode.current.write
+      then f state >>-: fun state -> Some (state, mode)
+      else `Value (Some (state, mode))
+
+  let update valuation = make_transfer (Domain.update valuation)
+  let assume stmt expr positive valuation =
+    make_transfer (Domain.assume stmt expr positive valuation)
+
+  (* Applies the [assign] transfer function according to the current mode.
+     In any case, removes from the state the properties depending on the memory
+     location modified by the assignment. *)
+  let assign kinstr lvalue expr assigned valuation = function
+    | None -> `Value None
+    | Some (state, mode) ->
+      if mode.current.write
+      then
+        Domain.assign kinstr lvalue expr assigned valuation state >>-: fun s ->
+        Some (s, mode)
+      else
+        let state = Domain.logic_assign None lvalue.lloc state in
+        `Value (Some (state, mode))
+
+  (* Starts an analysis at call [call] with state [state]. The domain was not
+     enabled before this call: the concrete arguments may contain variables that
+     have never been introduced into the state, so we should not use them. This
+     function only introduces the formal parameters in the state. *)
+  let start_analysis call state =
+    let formals = List.map (fun argument -> argument.formal) call.arguments in
+    let kind = Abstract_domain.Formal call.kf in
+    let state = Domain.enter_scope kind formals state in
+    let initialize acc v = Domain.initialize_variable_using_type kind v acc in
+    let state = List.fold_left initialize state formals in
+    state
+
+  (* When interpreting a function call:
+     - if the mode of the function called allows the domain to infer properties,
+       use [start_call] and [finalize_call] as normal. If the current mode did
+       not allow the domain to infer properties, use [start_analysis] instead.
+     - otherwise, only propagate the state from the call site to kill the
+       properties that depend on locations written in the called functions. *)
+
+  let start_call stmt call valuation state =
+    (* Starts the call with mode [new_mode]. [previous_mode] is the current mode
+       of the caller. *)
+    let start_call_with_mode ?previous_mode ~new_mode state =
+      if new_mode.current.write
+      then
+        match previous_mode with
+        | Some mode when mode.current.write ->
+          Domain.start_call stmt call valuation state >>-: fun state ->
+          Some (state, new_mode)
+        | _ ->
+          `Value (Some (start_analysis call state, new_mode))
+      else `Value (Some (state, new_mode))
+    in
+    (* If an analysis mode is defined for the called function in [Scope],
+       then this mode becomes the new current mode. Otherwise, use the [calls]
+       field of the previous mode. *)
+    let called_mode = Kernel_function.Map.find_opt call.kf functions_map in
+    match state, called_mode with
+    | Some (state, previous_mode), Some new_mode ->
+      start_call_with_mode ~previous_mode ~new_mode state
+    | Some (state, previous_mode), None ->
+      let new_mode = { previous_mode with current = previous_mode.calls } in
+      start_call_with_mode ~previous_mode ~new_mode state
+    | None, Some new_mode ->
+      start_call_with_mode ~new_mode (get_starting_state ())
+    | None, None ->
+      `Value None
+
+  let finalize_call stmt call ~pre ~post =
+    match pre, post with
+    | None, _ | _, None -> `Value None
+    | Some (pre, pre_mode), Some (post, post_mode) ->
+      if post_mode.current.write
+      then
+        Domain.finalize_call stmt call ~pre ~post >>-: fun state ->
+        Some (state, pre_mode)
+      else
+        `Value (Some (post, pre_mode))
+
+  let show_expr valuation state fmt expr =
+    match state with
+    | None -> ()
+    | Some (state, _mode) -> Domain.show_expr valuation state fmt expr
+
+  (* ----- Logic evalutation ------------------------------------------------ *)
+
+  let logic_assign assign location = function
+    | None -> None
+    | Some (state, mode) ->
+      let assign =
+        Extlib.opt_map (fun (assign, state) -> assign, get_state state) assign
+      in
+      Some (Domain.logic_assign assign location state, mode)
+
+  let lift_env env =
+    let states label = get_state (env.Abstract_domain.states label) in
+    Abstract_domain.{ env with states = states }
+
+  let evaluate_predicate env state predicate =
+    make_query
+      Alarmset.Unknown
+      (fun s -> Domain.evaluate_predicate (lift_env env) s predicate)
+      state
+
+  let reduce_by_predicate env state predicate positive =
+    make_transfer
+      (fun s -> Domain.reduce_by_predicate (lift_env env) s predicate positive)
+      state
+
+  (* ----- Scoping, initialization & loops ---------------------------------- *)
+
+  let lift f = function
+    | None -> None
+    | Some (state, mode) as x ->
+      if mode.current.write
+      then Some (f state, mode)
+      else x
+
+  let enter_scope kind varinfos = lift (Domain.enter_scope kind varinfos)
+  let leave_scope kf varinfos = lift (Domain.leave_scope kf varinfos)
+
+  (* Uses the mode of the 'main' function to start the analysis. *)
+  let empty () =
+    let main_kf = fst (Globals.entry_point ()) in
+    match Kernel_function.Map.find_opt main_kf functions_map with
+    | None -> None
+    | Some mode -> Some (Domain.empty (), mode)
+
+  let initialize_variable lval location ~initialized init_value =
+    lift (Domain.initialize_variable lval location ~initialized init_value)
+  let initialize_variable_using_type init_kind varinfo =
+    lift (Domain.initialize_variable_using_type init_kind varinfo)
+
+  let enter_loop stmt = lift (Domain.enter_loop stmt)
+  let incr_loop_counter stmt = lift (Domain.incr_loop_counter stmt)
+  let leave_loop stmt = lift (Domain.leave_loop stmt)
+
+  (* ----- MemExec ---------------------------------------------------------- *)
+
+  let relate kf bases = function
+    | None -> Base.SetLattice.empty
+    | Some (state, _mode) -> Domain.relate kf bases state
+
+  let filter kf kind bases = function
+    | None -> None
+    | Some (state, mode) -> Some (Domain.filter kf kind bases state, mode)
+
+  let reuse kf bases ~current_input ~previous_output =
+    match current_input, previous_output with
+    | None, _ | _, None -> None
+    | Some (current_input, mode), Some (previous_output, _) ->
+      Some (Domain.reuse kf bases ~current_input ~previous_output, mode)
+
+  let log_category = Domain.log_category
+
+  let post_analysis state =
+    let state = state >>-: get_state in
+    Domain.post_analysis state
+
+  (* ----- Storage ---------------------------------------------------------- *)
+
+  module Store = struct
+
+    let register_global_state state =
+      let state = state >>-: get_state in
+      Domain.Store.register_global_state state
+
+    let lift_register f state = f (get_state state)
+
+    let register_initial_state callstack =
+      lift_register (Domain.Store.register_initial_state callstack)
+    let register_state_before_stmt callstack stmt =
+      lift_register (Domain.Store.register_state_before_stmt callstack stmt)
+    let register_state_after_stmt callstack stmt =
+      lift_register (Domain.Store.register_state_after_stmt callstack stmt)
+
+    let inject state = Some (state, Mode.all)
+
+    let get_global_state () = Domain.Store.get_global_state () >>-: inject
+    let get_initial_state kf = Domain.Store.get_initial_state kf >>-: inject
+    let get_stmt_state ~after stmt =
+      Domain.Store.get_stmt_state ~after stmt >>-: inject
+
+    let inject_table = function
+      | `Top -> `Top
+      | `Bottom -> `Bottom
+      | `Value t ->
+        let module Hashtbl = Value_types.Callstack.Hashtbl in
+        let table = Hashtbl.create (Hashtbl.length t) in
+        Hashtbl.iter (fun key s -> Hashtbl.add table key (inject s)) t;
+        `Value table
+
+    let get_initial_state_by_callstack kf =
+      inject_table (Domain.Store.get_initial_state_by_callstack kf)
+    let get_stmt_state_by_callstack ~after stmt =
+      inject_table (Domain.Store.get_stmt_state_by_callstack ~after stmt)
+
+  end
+end
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index b604579e939f7d63075e53eaf5e1bc80e1748c30..66613b44d545a3e0ed7fbfe1d6b41e6f93ee8d73 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -55,3 +55,15 @@ module Complete_Simple_Cvalue
   : Abstract_domain.Leaf with type value = Cvalue.V.t
                           and type location = Precise_locs.precise_location
                           and type state = Domain.t
+
+(* Restricts an abstract domain on specific functions. The domain will only be
+   enabled on the given functions. Moreover, a mode is associated to each of
+   these functions, allowing (or not) the domain to infer or use properties
+   in the current function and in all functions called from it.
+   See {!Domain_mode} for more details. *)
+module Restrict
+    (Value: Abstract_value.S)
+    (Domain: Abstract.Domain.Internal with type value = Value.t)
+    (Scope: sig val functions: Domain_mode.function_mode list end)
+  : Abstract.Domain.Internal with type value = Value.t
+                              and type location = Domain.location
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0e8d958ef1dd6fe0dbb2bbc9526d6252af663df3..46331911138dce10ab88edc059e32d695b44c0ac 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -123,8 +123,8 @@ module Make
 
   let show_expr valuation = Domain.show_expr (lift_valuation valuation)
 
-  let logic_assign assigns location ~pre state =
-    Domain.logic_assign assigns (Convert.restrict_loc location) ~pre state
+  let logic_assign assigns location state =
+    Domain.logic_assign assigns (Convert.restrict_loc location) state
 
   let evaluate_predicate = Domain.evaluate_predicate
   let reduce_by_predicate = Domain.reduce_by_predicate
diff --git a/src/plugins/value/domains/domain_mode.ml b/src/plugins/value/domains/domain_mode.ml
new file mode 100644
index 0000000000000000000000000000000000000000..298f27fc57d885a4b0c438fe24e4388ad983f435
--- /dev/null
+++ b/src/plugins/value/domains/domain_mode.ml
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type permission = { read: bool; write: bool; }
+type mode = { current: permission; calls: permission; }
+
+type function_mode = Kernel_function.t * mode
+
+module Mode = struct
+  let all_permission = { read = true; write = true; }
+  let no_permission = { read = false; write = false; }
+
+  let default = { current = all_permission; calls = no_permission; }
+  let all = { current = all_permission; calls = all_permission; }
+  let none = { current = no_permission; calls = no_permission; }
+
+  include Datatype.Make_with_collections
+      (struct
+        include Datatype.Serializable_undefined
+        type t = mode
+        let name = "Domain_mode.Mode"
+        let reprs = [ default ]
+        let compare = Transitioning.Stdlib.compare
+        let equal = Datatype.from_compare
+        let hash = Hashtbl.hash
+      end)
+
+  let check str =
+    String.iter
+      (fun c ->
+         if Char.lowercase_ascii c <> 'r' && Char.lowercase_ascii c <> 'w'
+         then raise (Invalid_argument ("invalid mode " ^ str)))
+      str
+
+  let of_string str =
+    check str;
+    let calls =
+      { read = String.contains str 'R';
+        write = String.contains str 'W'; }
+    and current =
+      { read = String.contains str 'r';
+        write = String.contains str 'w'; }
+    in
+    { current; calls; }
+
+  let to_string t =
+    let string_if c b = if b then c else "" in
+    string_if "r" t.current.read ^ string_if "w" t.current.write ^
+    string_if "R" t.calls.read ^ string_if "W" t.calls.write
+end
+
+module Function_Mode = struct
+  include Datatype.Pair (Kernel_function) (Mode)
+  type key = string
+
+  let of_string ~key ~prev:_ str =
+    match str with
+    | None -> raise (Invalid_argument ("no value bound to " ^ key))
+    | Some str ->
+      let get_function str =
+        try Globals.Functions.find_by_name str
+        with Not_found -> raise (Invalid_argument ("no function " ^ str))
+      in
+      match String.split_on_char '-' str with
+      | [ kf; "" ] -> Some (get_function kf, Mode.none)
+      | _ ->
+        match String.split_on_char '+' str with
+        | [ kf ]       -> Some (get_function kf, Mode.default)
+        | [ kf; "" ]   -> Some (get_function kf, Mode.all)
+        | [ kf; mode ] -> Some (get_function kf, Mode.of_string mode)
+        | _ -> raise (Invalid_argument ("invalid argument " ^ str))
+
+  let to_string ~key:_ = function
+    | None -> None
+    | Some (kf, mode) ->
+      Some (Kernel_function.get_name kf ^ "+" ^ Mode.to_string mode)
+end
+
+include Datatype.List (Function_Mode)
diff --git a/src/plugins/value/domains/domain_mode.mli b/src/plugins/value/domains/domain_mode.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cbb9a07e2c7ef60b0e39379690049951244070b2
--- /dev/null
+++ b/src/plugins/value/domains/domain_mode.mli
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** This module defines the mode to restrict an abstract domain on specific
+    functions. *)
+
+(** Permission for an abstract domain to read/write its state.
+    If [write] is true, the domain infers new properties when interpreting
+    assignments, assumptions, and logical assertions. Otherwise, it only
+    propagates already known properties as long as they hold.
+    If [read] is true, the domain uses its inferred properties to improve
+    the evaluation of expressions by extracting information from its state.
+    It can also evaluate logical assertions. *)
+type permission = { read: bool; write: bool; }
+
+(** Mode for the analysis of a function [f]:
+    - [current] is the read/write permission for [f].
+    - [calls] is the read/write permission for all functions called from [f]. *)
+type mode = { current: permission; calls: permission; }
+
+(** Datatype for modes. *)
+module Mode : sig
+  include Datatype.S_with_collections with type t = mode
+  val all: t (** Default mode: all permissions are granted. *)
+end
+
+(** A function associated with an analysis mode. *)
+type function_mode = Kernel_function.t * mode
+
+module Function_Mode:
+  Parameter_sig.Multiple_value_datatype with type key = string
+                                         and type t = function_mode
+
+(** Analysis mode for a domain. *)
+include Datatype.S with type t = function_mode list
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index d73cc44bf4a3293e531a0df0752500116498963a..06574e327e6fed7fb945168a33b07b20372d9f98 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -37,8 +37,8 @@ module Make
   type location = Left.location
 
   type origin = {
-    left:  reductness * Left.origin;
-    right: reductness * Right.origin;
+    left:  reductness * Left.origin option;
+    right: reductness * Right.origin option;
   }
 
   let () = incr counter
@@ -85,7 +85,7 @@ module Make
           else if Value.equal v2 Value.top then Created else Reduced
         in
         let origin = {left = left, o1; right = right, o2} in
-        value, origin
+        value, Some origin
       in
       value, alarms
 
@@ -120,7 +120,7 @@ module Make
       | Reduced, Some (Created, _) -> Created
       | _ as x, _ -> x
     in
-    let origin = Extlib.opt_map snd origin in
+    let origin = Extlib.may_map snd ~dft:None origin in
     { record with origin; reductness }
 
   let lift_valuation side valuation =
@@ -227,9 +227,14 @@ module Make
          print_one_side fmt right_log Right.name Right.pretty right)
 
 
-  let logic_assign assign location ~pre:(left_pre, right_pre) (left, right) =
-    Left.logic_assign assign location ~pre:left_pre left,
-    Right.logic_assign assign location ~pre:right_pre right
+  let logic_assign assign location (left, right) =
+    let left_assign, right_assign =
+      match assign with
+      | None -> None, None
+      | Some (assign, (left, right)) -> Some (assign, left), Some (assign, right)
+    in
+    Left.logic_assign left_assign location left,
+    Right.logic_assign right_assign location right
 
   let lift_logic_env f logic_env =
     Abstract_domain.{ states = (fun label -> f (logic_env.states label));
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index b36c5560bf041b5b3faac65731f3daf489acccd5..b04cd0ffa19955c80a0e67c183af5193509399ff 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -189,7 +189,7 @@ module Make
 
   type value = Value.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   let reduce_further (equalities, _, _) expr value =
     let atom = HCE.of_exp expr in
@@ -232,12 +232,12 @@ module Make
       in
       let v = Equality.Equality.fold aux_eq equality (`Value Value.top) in
       (* Remove the 'origin' information of garbled mixes. *)
-      let v = v >>-: fun v -> imprecise_origin v, () in
+      let v = v >>-: fun v -> imprecise_origin v, None in
       (* All expressions used by the equality domain have already been evaluated
          before during the analysis; alarms about those expressions have already
          been emitted. *)
       v, Alarmset.none
-    | None -> `Value (Value.top, ()), Alarmset.all
+    | None -> `Value (Value.top, None), Alarmset.all
 
   let extract_expr (oracle: exp -> Value.t evaluated) (equalities, _, _) expr =
     let expr = Cil.constFold true expr in
@@ -503,7 +503,7 @@ module Make
     | Some equality -> Equality.Equality.pretty fmt equality
     | None -> ()
 
-  let logic_assign _assigns location ~pre:_ state =
+  let logic_assign _assigns location state =
     let loc = Precise_locs.imprecise_location location in
     let zone = Locations.(enumerate_valid_bits Write loc) in
     kill Hcexprs.Modified zone state
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 75acbedd0d9b10b60c6c028ccbf45435ada87e4a..4c8dec87e1ecf236a920ef4eb38a1134f3a6ceb7 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1130,7 +1130,7 @@ module D_Impl : Abstract_domain.S
   type value = Cvalue.V.t
   type state = G.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   include G
 
@@ -1260,7 +1260,7 @@ module D_Impl : Abstract_domain.S
   (* TODO: it would be interesting to return something here, but we
      currently need a valuation to perform the translation. *)
   let extract_expr _oracle _state _exp =
-    `Value (Cvalue.V.top, ()), Alarmset.all
+    `Value (Cvalue.V.top, None), Alarmset.all
 
   let extract_lval _oracle state _lv typ loc =
     let v =
@@ -1274,7 +1274,7 @@ module D_Impl : Abstract_domain.S
     (* We can probably return an empty set of alarms when the value is known,
        but the only possible alarms on lvalues are about indeterminateness,
        and it is not clear that we know more than the Cvalue domain. *)
-    `Value (v, ()), Alarmset.all
+    `Value (v, None), Alarmset.all
 
   let backward_location _state _lval _typ loc value = `Value (loc, value)
 
@@ -1296,7 +1296,7 @@ module D_Impl : Abstract_domain.S
   let initialize_variable _ _ ~initialized:_ _ state = state
 
   (* Logic *)
-  let logic_assign _assigns location ~pre:_ state = kill location state
+  let logic_assign _assigns location state = kill location state
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 6bdc20363831dce8f2b6671deedfc4a08517db66..5bbf25ba1ff5dc18b3f392d07d6d25b5d35c4fcf 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -213,7 +213,7 @@ module Internal
   type state = inout
   type value = Cvalue.V.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   include (LatticeInout: sig
              include Datatype.S_with_collections with type t = state
@@ -261,7 +261,7 @@ module Internal
   let initialize_variable_using_type _ _ state  = state
 
   (* TODO *)
-  let logic_assign _assign _location ~pre:_ _state = top
+  let logic_assign _assign _location _state = top
 
   (* Logic *)
   let evaluate_predicate _ _ _ = Alarmset.Unknown
@@ -269,7 +269,7 @@ module Internal
 
   let storage () = true
 
-  let top_query = `Value (Cvalue.V.top, ()), Alarmset.all
+  let top_query = `Value (Cvalue.V.top, None), Alarmset.all
 
   let extract_expr _oracle _state _expr = top_query
   let extract_lval _oracle _state _lv _typ _locs = top_query
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 8ed828c84e0d967960095b7121f6ab5df7e6647a..b1faca4b4d688ab17f84382b814b3b23c4206a6b 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1037,9 +1037,9 @@ module Domain = struct
 
   type value = Cvalue.V.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
-  let top_value = `Value (Cvalue.V.top, ()), Alarmset.all
+  let top_value = `Value (Cvalue.V.top, None), Alarmset.all
 
   let extract_expr oracle state expr =
     let evaluate_expr expr =
@@ -1057,7 +1057,7 @@ module Domain = struct
     then top_value
     else if Ival.is_bottom ival
     then `Bottom, Alarmset.all
-    else `Value (Cvalue.V.inject_ival ival, ()), alarms
+    else `Value (Cvalue.V.inject_ival ival, None), alarms
 
   let extract_lval _oracle _t _lval _typ _loc = top_value
 
@@ -1235,7 +1235,7 @@ module Domain = struct
 
   let show_expr _valuation _state _fmt _expr = ()
 
-  let logic_assign _logic_assign location ~pre:_ state =
+  let logic_assign _logic_assign location state =
     let loc = Precise_locs.imprecise_location location in
     let zone = Locations.(enumerate_valid_bits Write loc) in
     let state = kill zone state in
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 87c59b2711520b55c106ef6aaedd552b7f7d99d2..cb7c583d9e8aa74a6008cbd9a746de1f3223d8ad 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -97,7 +97,7 @@ module Internal  : Domain_builder.InputDomain
   type value = offsm_or_top
   type state = Memory.t
   type location = Precise_locs.precise_location
-  type origin = unit (* ???? *)
+  type origin
 
   include (Memory: sig
              include Datatype.S_with_collections with type t = state
@@ -164,7 +164,7 @@ module Internal  : Domain_builder.InputDomain
   let show_expr _valuation _state _fmt _expr = ()
 
   let extract_expr _oracle _state _exp =
-    `Value (Offsm_value.Offsm.top, ()), Alarmset.all
+    `Value (Offsm_value.Offsm.top, None), Alarmset.all
 
   (* Basic 'find' on a location *)
   let find_loc state loc =
@@ -181,7 +181,7 @@ module Internal  : Domain_builder.InputDomain
       if Cil.typeHasQualifier "volatile" typ ||
          not (Cil.isArithmeticOrPointerType typ)
       then
-        `Value (Top, ())
+        `Value (Top, None)
       else
         try
           let aux_loc loc o =
@@ -189,8 +189,8 @@ module Internal  : Domain_builder.InputDomain
             Bottom.join Offsm_value.Offsm.join o o'
           in
           Precise_locs.fold aux_loc locs `Bottom >>-: fun v ->
-          v, ()
-        with Abstract_interp.Error_Top -> `Value (Top, ())
+          v, None
+        with Abstract_interp.Error_Top -> `Value (Top, None)
     in
     o, Alarmset.all
 
@@ -216,7 +216,7 @@ module Internal  : Domain_builder.InputDomain
   let initialize_variable _ _ ~initialized:_ _ state = state
 
   (* Logic *)
-  let logic_assign _assign location ~pre:_ state =
+  let logic_assign _assign location state =
     let loc = Precise_locs.imprecise_location location in
     kill loc state
 
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 56e9aecdb1276f7318e81e53543763a67ad8d586..f2e84f2c345451919a483d69b896082546acb526 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -187,7 +187,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
   type state = t
   type value = Value.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   let log_category = Value_parameters.register_category ("d-" ^ Info.name)
 
@@ -198,9 +198,9 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
      evaluation. *)
   let extract_lval _oracle state _lv typ loc =
     let v = find loc typ state in
-    `Value (v, ()), Alarmset.all
+    `Value (v, None), Alarmset.all
 
-  let extract_expr _oracle _state _expr = `Value (Value.top, ()), Alarmset.all
+  let extract_expr _oracle _state _expr = `Value (Value.top, None), Alarmset.all
 
   let backward_location state _lval typ loc _value =
     let new_value = find loc typ state in
@@ -300,7 +300,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
   let incr_loop_counter _ state = state
   let leave_loop _ state = state
 
-  let logic_assign _assign location ~pre:_ state = remove location state
+  let logic_assign _assign location state = remove location state
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index f7e994cc2546eda24b8da368e0831934869e3a62..9464308a6e2d57bed2ad1a649186983298815d56 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -466,7 +466,7 @@ module Internal : Domain_builder.InputDomain
   type state = Memory.t
   type value = V.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   include (Memory: sig
              include Datatype.S_with_collections with type t = state
@@ -569,7 +569,7 @@ module Internal : Domain_builder.InputDomain
 
   let show_expr _valuation _state _fmt _expr = ()
 
-  let top_query = `Value (V.top, ()), Alarmset.all
+  let top_query = `Value (V.top, None), Alarmset.all
 
   (* For extraction functions, if we have an information about the value,
      this means that the key has been evaluated in all the paths that reach
@@ -579,12 +579,12 @@ module Internal : Domain_builder.InputDomain
   let extract_expr _oracle state expr =
     match Memory.find_expr expr state with
     | None -> top_query
-    | Some v -> `Value (v, ()), Alarmset.none
+    | Some v -> `Value (v, None), Alarmset.none
 
   let extract_lval _oracle state lv _typ _locs =
     match Memory.find_lval lv state with
     | None -> top_query
-    | Some v -> `Value (v, ()), Alarmset.none
+    | Some v -> `Value (v, None), Alarmset.none
 
   let backward_location _state _lval _typ loc value =
     (* Nothing to do. We could check if [[lval]] intersects [value] and
@@ -631,7 +631,7 @@ module Internal : Domain_builder.InputDomain
   let initialize_variable _ _ ~initialized:_ _ state = state
 
   (* Logic *)
-  let logic_assign _assigns location ~pre:_ state =
+  let logic_assign _assigns location state =
     let loc = Precise_locs.imprecise_location location in
     Memory.kill loc state
 
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 1761500f38fa86be76428eeb46db791f4099c4ec..de5887617b6b296e62609fe8fbe67d6ae974e4fb 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -848,7 +848,7 @@ module Internal = struct
   type nonrec state = state
   type value = Cvalue.V.t
   type location = Precise_locs.precise_location
-  type origin = unit
+  type origin
 
   include (Traces: sig
              include Datatype.S_with_collections with type t = state
@@ -931,7 +931,7 @@ module Internal = struct
     Traces.add_trans state (Msg msg)
 
   (* TODO *)
-  let logic_assign _assign _location ~pre:_ state =
+  let logic_assign _assign _location state =
     Traces.add_trans state (Msg "logic assign")
 
   (* Logic *)
@@ -940,7 +940,7 @@ module Internal = struct
 
   let storage () = true
 
-  let top_query = `Value (Cvalue.V.top, ()), Alarmset.all
+  let top_query = `Value (Cvalue.V.top, None), Alarmset.all
 
   let extract_expr _oracle _state _expr = top_query
   let extract_lval _oracle _state _lv _typ _locs = top_query
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 00c59d6445cdcc7fc3434a0162222f2d1d0158e1..c12cdfc9f3cfa03bc6b7b3ac6ef2001b96513110 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -52,9 +52,9 @@ module Make
   include Static
   type value = Value.t
   type location = Loc.location
-  type origin = unit
+  type origin
 
-  let eval_top = `Value (Value.top, ()), Alarmset.all
+  let eval_top = `Value (Value.top, None), Alarmset.all
   let extract_expr _ _ _ = eval_top
   let extract_lval _ _ _ _ _ = eval_top
   let backward_location _ _ _ loc value = `Value (loc, value)
@@ -67,7 +67,7 @@ module Make
   let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
   let show_expr _ _ _ _ = ()
 
-  let logic_assign _ _ ~pre:_ _ = ()
+  let logic_assign _ _ _ = ()
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ _ _ _ = `Value ()
 
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index d393a2061409a669a59d45d703814d192735d35f..5f568596c566adfd2d406a06c248255bc10d4088 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -53,16 +53,23 @@ type flag = Flag: 'v abstraction with_info -> flag
 (* --- Config and registration ---------------------------------------------- *)
 
 module Config = struct
-  module Flag = struct
-    type t = flag
+  module OptMode = Datatype.Option (Domain_mode)
+  module Element = struct
+    type t = flag * Domain_mode.t option
 
     (* Flags are sorted by increasing priority order, and then by name. *)
-    let compare (Flag f1) (Flag f2) =
+    let compare (Flag f1, mode1) (Flag f2, mode2) =
       let c = Datatype.Int.compare f1.priority f2.priority in
-      if c <> 0 then c else Datatype.String.compare f1.name f2.name
+      if c <> 0 then c else
+        let c = Datatype.String.compare f1.name f2.name in
+        if c <> 0 then c else
+          OptMode.compare mode1 mode2
   end
 
-  include Set.Make (Flag)
+  include Set.Make (Element)
+
+  let mem (Flag domain) =
+    exists (fun (Flag flag, _mode) -> flag.name = domain.name)
 
   type dynamic = Dynamic: (unit -> 'v abstraction) with_info -> dynamic
 
@@ -83,19 +90,29 @@ module Config = struct
     dynamic_abstractions := dynamic :: !dynamic_abstractions
 
   let configure () =
+    let add_main_mode mode =
+      let main, _ = Globals.entry_point () in
+      (main, Domain_mode.Mode.all) :: mode
+    in
+    let add config name make =
+      let enabled = Value_parameters.Domains.mem name in
+      try
+        let mode = Value_parameters.DomainsFunction.find name in
+        let mode = if enabled then add_main_mode mode else mode in
+        add (make (), Some mode) config
+      with Not_found ->
+        if enabled then add (make (), None) config else config
+    in
     let aux config (Flag domain as flag) =
-      if Value_parameters.Domains.mem domain.name
-      then add flag config
-      else config
+      add config domain.name (fun () -> flag)
     in
     let config = List.fold_left aux empty !abstractions in
     let aux config (Dynamic { name; experimental; priority; abstraction; }) =
-      if Value_parameters.Domains.mem name
-      then
+      let make () =
         let abstraction = abstraction () in
-        let flag = Flag { name; experimental; priority; abstraction; } in
-        add flag config
-      else config
+        Flag { name; experimental; priority; abstraction; }
+      in
+      add config name make
     in
     List.fold_left aux config !dynamic_abstractions
 
@@ -171,7 +188,7 @@ module Config = struct
   (* --- Default and legacy configurations ---------------------------------- *)
 
   let default = configure ()
-  let legacy = singleton cvalue
+  let legacy = singleton (cvalue, None)
 end
 
 let register = Config.register
@@ -221,17 +238,23 @@ module Internal_Value = struct
         let structure = Node (Value.structure, Leaf (key, v))
       end)
 
+  let void_value () =
+    Value_parameters.fatal
+      "Cannot register a value module from a Void structure."
+
   let add_value_structure value internal =
     let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
       fun value -> function
+        | Option (s, _) -> aux value s
         | Leaf (key, v) -> add_value_leaf value (V (key, v))
         | Node (s1, s2) -> aux (aux value s1) s2
         | Unit -> value
+        | Void -> void_value ()
     in
     aux value internal
 
   let build_values config initial_value =
-    let build (Flag flag) acc =
+    let build (Flag flag, _) acc =
       match flag.abstraction.values with
       | Struct structure -> add_value_structure acc structure
       | Single (module V) -> add_value_leaf acc (V (V.key, (module V)))
@@ -258,7 +281,9 @@ module Internal_Value = struct
         | Node (s1, s2) ->
           let set1 = set s1 and set2 = set s2 in
           fun (v1, v2) value -> set1 v1 (set2 v2 value)
+        | Option (s, default) -> fun v -> set s (Extlib.opt_conv default v)
         | Unit -> fun () value -> value
+        | Void -> void_value ()
       in
       set structure
 
@@ -270,7 +295,9 @@ module Internal_Value = struct
         | Node (s1, s2) ->
           let get1 = get s1 and get2 = get s2 in
           fun v -> get1 v, get2 v
+        | Option (s, _) -> fun v -> Some (get s v)
         | Unit -> fun _ -> ()
+        | Void -> void_value ()
       in
       get structure
 
@@ -297,7 +324,7 @@ let eq_value:
       | Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
       | _ -> None
 
-let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
+let add_domain (type v) mode (abstraction: v abstraction) (module Acc: Acc) =
   let domain : (module internal_domain with type value = Acc.Val.t) =
     match abstraction.domain with
     | Functor make ->
@@ -317,6 +344,19 @@ let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
         let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
         (module Domain_lift.Make (Domain) (Convert))
   in
+  let domain : (module internal_domain with type value = Acc.Val.t) =
+    match mode with
+    | None -> domain
+    | Some kf_modes ->
+      let module Scope = struct let functions = kf_modes end in
+      let module Domain =
+        Domain_builder.Restrict
+          (Acc.Val)
+          ((val domain))
+          (Scope)
+      in
+      (module Domain)
+  in
   let domain : (module internal_domain with type value = Acc.Val.t) =
     match Abstract.Domain.(eq_structure Acc.Dom.structure Unit) with
     | Some _ -> domain
@@ -337,9 +377,9 @@ let warn_experimental flag =
                         "The %s domain is experimental." flag.name)
 
 let build_domain config abstract =
-  let build (Flag flag) acc =
+  let build (Flag flag, mode) acc =
     warn_experimental flag;
-    add_domain flag.abstraction acc
+    add_domain mode flag.abstraction acc
   in
   (* Domains in the [config] are sorted by increasing priority: domains with
      higher priority are added last: they will be at the top of the domains
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 0156b516d8ad4b0e39cdad5baaa1986a5547e08b..3f3ff8d674ec678f41beec36025bc7b14fcac6f8 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -25,13 +25,14 @@
 (** {2 Registration of abstractions.} *)
 
 (** Dynamic registration of the abstractions to be used in an Eva analysis:
-    - value abstractions, detailled in the {Abstract_value} signature;
-    - location abstractions, detailled in the {Abstract_location} signature;
-    - state abstractions, or abstract domains, detailled in {Abstract_domain}.
+    - value abstractions, detailed in the {Abstract_value} signature;
+    - location abstractions, detailed in the {Abstract_location} signature;
+    - state abstractions, or abstract domains, detailed in {Abstract_domain}.
 *)
 
 (** Module types of value abstractions: either a single leaf module, or
-    a compound of several modules described by a structure. *)
+    a compound of several modules described by a structure. In this last case,
+    the structure must not contain the Void constructor. *)
 type 'v value =
   | Single of (module Abstract_value.Leaf with type t = 'v)
   | Struct of 'v Abstract.Value.structure
@@ -137,9 +138,14 @@ val register_hook: ((module S) -> (module S)) -> unit
 (** {2 Configuration of an analysis.} *)
 
 (** Configuration defining the abstractions to be used in an analysis.
-    A configuration is a set of flags, i.e. a set of enabled abstractions. *)
+    A configuration is a set of flags, i.e. a set of abstract domains. Each flag
+    comes with an optional mode. None is the default mode: the given domain is
+    enabled for the whole analysis. See {!Domain_mode} for more details. *)
 module Config : sig
-  include Set.S with type elt = flag
+  include Set.S with type elt = flag * Domain_mode.t option
+
+  (** Returns true if the given flag is in the configuration. *)
+  val mem: flag -> t -> bool
 
   (** Flags for the standard domains currently provided in Eva. *)
 
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 757510704f68b66455b05f3259038503aba41372..06c72bf50993d410b025682e5ee4f2ab914a45a9 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -165,17 +165,8 @@ let force_compute () =
   let module Analyzer = (val snd !ref_analyzer) in
   Analyzer.compute_from_entry_point ~lib_entry kf
 
-let set_hook_on_parameter parameter =
-  let open Typed_parameter in
-  match parameter.accessor with
-  | Bool (accessor, _)   -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
-  | Int (accessor, _)    -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
-  | String (accessor, _) -> accessor.add_set_hook (fun _ _ -> reset_analyzer ())
-
-(* Resets the Analyzer whenever an abstraction parameter or the current project
-   is changed. This maintains the analyzer consistent with the Eva parameters. *)
+(* Resets the Analyzer when the current project is changed. *)
 let () =
-  List.iter set_hook_on_parameter Value_parameters.parameters_abstractions;
   Project.register_after_set_current_hook
     ~user_only:true (fun _ -> reset_analyzer ());
   Project.register_after_global_load_hook reset_analyzer
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 5e0445cf0ca78cca3d9cdd2f8cff7654954e8a0e..d4d08981adf244d32f5bbd3fb4c3ddbd90740829 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -258,7 +258,7 @@ let indeterminate_copy lval result alarms =
   let reductness = Unreduced in
   let v, origin = match result with
     | `Bottom -> `Bottom, None
-    | `Value (v, origin) -> `Value v, Some origin
+    | `Value (v, origin) -> `Value v, origin
   in
   let value = { v; initialized; escaping } in
   let record = { value; origin; reductness; val_alarms = alarms} in
@@ -853,7 +853,6 @@ module Make
             in
             let reduction =
               update_reduction reduction (Value.equal intern_value result)
-            and origin = Some origin
             and value = define_value result in
             (* The proper alarms will be set in the record by forward_eval. *)
             {value; origin; reductness; val_alarms = Alarmset.all},
@@ -1084,7 +1083,6 @@ module Make
       let v, alarms = assume_valid_value typ_lv lval (v, alarms) in
       (v, alarms) >>=: fun (value, origin) ->
       let value = define_value value
-      and origin = Some origin
       and reductness, reduction =
         if Alarmset.is_empty alarms then Unreduced, Neither else Reduced, Forward
       in
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index d84a01a562d01814e83e121f2c0deb60109e5a05..4521648ffbbe9efce1e5e6a20a06226aba7309fb 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -267,7 +267,7 @@ module Make
     let env = make_env state in
     let assigns_with_locations = evaluate_locations env retres_loc assigns in
     let transfer state (logic_assign, location) =
-      Domain.logic_assign logic_assign location ~pre state
+      Domain.logic_assign (Some (logic_assign, pre)) location state
     in
     List.fold_left transfer state assigns_with_locations
 
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 1d221ef75907685c1077325fc0fccec131c40994..9722347d7d85b1bbd54e823b3f1a5ec5876c4c27 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -69,8 +69,10 @@ module type Shape = sig
 
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
 end
@@ -81,8 +83,10 @@ module Shape (Key: Key) (Data: sig type 'a t end) = struct
 
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   let rec eq_structure : type a b. a structure -> b structure -> (a, b) eq option
     = fun a b ->
@@ -94,6 +98,12 @@ module Shape (Key: Key) (Data: sig type 'a t end) = struct
           | Some Eq, Some Eq -> Some Eq
           | _, _ -> None
         end
+      | Option (s1, _), Option (s2, _) ->
+        begin
+          match eq_structure s1 s2 with
+          | Some Eq -> Some Eq
+          | None -> None
+        end
       | Unit, Unit -> Some Eq
       | _, _ -> None
 end
@@ -130,8 +140,10 @@ module Open
 
   let rec mem : type a. 'v Shape.key -> a structure -> bool = fun key -> function
     | Unit -> false
+    | Void -> false
     | Leaf (k, _) -> Shape.equal key k
     | Node (left, right) -> mem key left || mem key right
+    | Option (s, _) -> mem key s
 
   let mem key = mem key M.structure
 
@@ -144,11 +156,15 @@ module Open
 
   let rec compute_getters : type a. a structure -> (a getter) KMap.t = function
     | Unit -> KMap.empty
+    | Void -> KMap.empty
     | Leaf (key, _) ->  KMap.singleton key (Get (key, fun (t : a) -> t))
     | Node (left, right) ->
       let l = compute_getters left and r = compute_getters right in
       let l = KMap.map (lift_get fst) l and r = KMap.map (lift_get snd) r in
       KMap.union (fun _k a _b -> Some a) l r
+    | Option (s, default) ->
+      let l = compute_getters s in
+      KMap.map (lift_get (Extlib.opt_conv default)) l
 
   let getters = compute_getters M.structure
   let get (type a) (key: a Shape.key) : (M.t -> a) option =
@@ -167,12 +183,16 @@ module Open
 
   let rec compute_setters : type a. a structure -> (a setter) KMap.t = function
     | Unit -> KMap.empty
+    | Void -> KMap.empty
     | Leaf (key, _) -> KMap.singleton key (Set (key, fun v _t -> v))
     | Node (left, right) ->
       let l = compute_setters left and r = compute_setters right in
       let l = KMap.map (lift_set (fun set (l, r) -> set l, r)) l
       and r = KMap.map (lift_set (fun set (l, r) -> l, set r)) r in
       KMap.union (fun _k a _b -> Some a) l r
+    | Option (s, _) ->
+      let l = compute_setters s in
+      KMap.map (lift_set Extlib.opt_map) l
 
   let setters = compute_setters M.structure
   let set (type a) (key: a Shape.key) : (a -> M.t -> M.t) =
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index 51a5d26d183cad4c857788d2ff791c3246cc4cfd..96555303c0f1139131ae32877f80e65806b3583c 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -62,8 +62,10 @@ module type Shape = sig
       Used internally to automatically generate efficient accessors of its nodes. *)
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
 end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 70311f618f178f9f657a7a05ea338807f30a14d1..ef524a0d17969518161a318f8c8d8e60f866c614 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -193,12 +193,6 @@ let register_domain ~name ~descr =
   Cmdline.replace_option_help
     Domains.option_name "eva" domains (domains_help ())
 
-let enabled_domains () =
-  let domains = Domains.get () in
-  List.filter
-    (fun (name, _) -> Datatype.String.Set.mem name domains)
-    !domains_ref
-
 (* Checks that a domain has been registered. *)
 let check_domain domain =
   if domain = "help" || domain = "list"
@@ -213,10 +207,40 @@ let () =
   Domains.add_set_hook
     (fun _old domains -> Datatype.String.Set.iter check_domain domains)
 
-(* Set of parameters defining the abstractions used in an Eva analysis. *)
-let parameters_abstractions =
-  ref (Typed_parameter.Set.singleton Domains.parameter)
+let () = Parameter_customize.set_group domains
+module DomainsFunction =
+  Make_multiple_map
+    (struct
+      include Datatype.String
+      let of_string str = check_domain str; str
+      let of_singleton_string = no_element_of_string
+      let to_string str = str
+    end)
+    (struct
+      include Domain_mode.Function_Mode
+      let of_string ~key ~prev str =
+        try of_string ~key ~prev str
+        with Invalid_argument msg -> raise (Cannot_build msg)
+    end)
+    (struct
+      let option_name = "-eva-domains-function"
+      let help = "Enables a domain only for the given functions. \
+                  <d:f+> enables the domain [d] from function [f] \
+                  (the domain is enabled in all functions called from [f]). \
+                  <d:f-> disables the domain [d] from function [f]."
+      let arg_name = "d:f"
+      let default = Datatype.String.Map.empty
+      let dependencies = []
+    end)
+let () = add_precision_dep DomainsFunction.parameter
 
+let enabled_domains () =
+  let domains = Domains.get () in
+  let domains_by_fct = DomainsFunction.get () in
+  List.filter
+    (fun (name, _) -> Datatype.String.Set.mem name domains
+                      || Datatype.String.Map.mem name domains_by_fct)
+    !domains_ref
 
 let () = Parameter_customize.set_group domains
 module EqualityCall =
@@ -1525,8 +1549,6 @@ let parameters_correctness =
   Typed_parameter.Set.elements !parameters_correctness
 let parameters_tuning =
   Typed_parameter.Set.elements !parameters_tuning
-let parameters_abstractions =
-  Typed_parameter.Set.elements !parameters_abstractions
 
 
 
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8c338bbc48c349b742d7af40e1ae39b0e4a580b8..b31c526f8648c46fb06a6677000e518e45f4f94b 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -29,6 +29,9 @@ module OracleDepth: Parameter_sig.Int
 module ReductionDepth: Parameter_sig.Int
 
 module Domains: Parameter_sig.String_set
+module DomainsFunction: Parameter_sig.Multiple_map
+  with type key = string
+   and type value = Domain_mode.function_mode
 
 module EqualityCall: Parameter_sig.String
 module EqualityCallFunction:
@@ -160,7 +163,6 @@ val configure_precision: unit -> unit
 
 val parameters_correctness: Typed_parameter.t list
 val parameters_tuning: Typed_parameter.t list
-val parameters_abstractions: Typed_parameter.t list
 
 (** Debug categories responsible for printing initial and final states of Value.
     Enabled by default, but can be disabled via the command-line:
diff --git a/tests/value/domains_function.c b/tests/value/domains_function.c
new file mode 100644
index 0000000000000000000000000000000000000000..e81f3e8c8dca745264423d081f29bb7c163c5dbf
--- /dev/null
+++ b/tests/value/domains_function.c
@@ -0,0 +1,123 @@
+/* run.config*
+   STDOPT: #"-eva-domains-function symbolic-locations:infer+w,symbolic-locations:use+r,symbolic-locations:test_propagation-,symbolic-locations:enabled,symbolic-locations:disabled-,symbolic-locations:recursively_enabled+"
+*/
+
+#include <__fc_builtin.h>
+
+/* Tests the -eva-domains-function option that enables a domain for the given
+   functions. This test uses the symbolic locations domain to store the value
+   of the location t[i] where [i] is imprecise, from an assignment of t[i]
+   to a read of t[i].
+   If the domain is not enabled, the value of t[i] remains imprecise because
+   [i] is imprecise. If the domain is enabled, the value of the first assignemnt
+   is stored until the read. If the assignment and the read are in different
+   functions, the domain should also be enabled in all functions in between. */
+
+volatile int undet;
+int i, result, t[10];
+
+/* No interaction with the known properties about t[i]. */
+void nothing () {
+  int tmp = t[i] - t[0];
+}
+
+/* Modify the value of t[i]. */
+void kill () {
+  t[0] = undet;
+}
+
+/* The domain has write access on this function: it infers the value of t[i]. */
+void infer () {
+  t[i] = 42;
+}
+
+/* The domain has no write access on this function. */
+void no_infer () {
+  t[i] = 42;
+}
+
+/* The domain has read access on this function: it can use the value of t[i]. */
+void use () {
+  result = t[i];
+}
+
+/* The domain has no read access on this function. */
+void no_use () {
+  result = t[i];
+}
+
+/* Test the propagation of information about t[i] from function [infer]
+   to function [use]. All other combinations of functions should not be
+   precise. */
+void test_propagation () {
+  infer ();
+  no_use ();
+  Frama_C_show_each_top(result);
+  nothing ();
+  use ();
+  Frama_C_show_each_singleton(result);
+  kill ();
+  use ();
+  Frama_C_show_each_top(result);
+  no_infer ();
+  use ();
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is enabled on this function. */
+void enabled () {
+  t[i] = 0;
+  result = t[i];
+}
+
+/* The domain is not enabled on this function. */
+void not_enabled () {
+  t[i] = 1;
+  result = t[i];
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is disabled on this function. */
+void disabled () {
+  t[i] = 2;
+  result = t[i];
+  Frama_C_show_each_top(result);
+}
+
+/* Precise result only after [enabled], since it is the only function
+   where the domain is enabled. */
+void test () {
+  t[i] = 3;
+  result = t[i];
+  Frama_C_show_each_top(result);
+  enabled ();
+  Frama_C_show_each_singleton(result);
+  not_enabled ();
+  Frama_C_show_each_top(result);
+  disabled ();
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is recursively enabled in this function and all functions called
+   from it: the results should be precise, except after [disabled] where the
+   domain is specifically disabled.*/
+void recursively_enabled () {
+  t[i] = 4;
+  result = t[i];
+  Frama_C_show_each_singleton(result);
+  enabled ();
+  Frama_C_show_each_singleton(result);
+  not_enabled ();
+  Frama_C_show_each_singleton(result);
+  disabled ();
+  Frama_C_show_each_top(result);
+}
+
+void main () {
+  for (int j = 0; j < 10; j++)
+    t[j] = undet;
+  i = Frama_C_interval(0,9);
+  test ();
+  recursively_enabled ();
+  test_propagation ();
+}
diff --git a/tests/value/numerors/oracle/numerors.res.oracle b/tests/value/numerors/oracle/numerors.res.oracle
index 96be7457bfd14f6f6707c210dea5bd6fd6bdb68a..6dc3b08df0fc2ca71334cb216a60933a004fa328 100644
--- a/tests/value/numerors/oracle/numerors.res.oracle
+++ b/tests/value/numerors/oracle/numerors.res.oracle
@@ -1,10 +1,10 @@
-[eva:experimental] Warning: The numerors domain is experimental.
 [kernel] Parsing tests/value/numerors/numerors.c (with preprocessing)
 [kernel:parser:decimal-float] tests/value/numerors/numerors.c:24: Warning: 
   Floating-point constant 0.69314718056 is not represented exactly. Will use 0x1.62e42fefa3bdcp-1.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [kernel:typing:implicit-function-declaration] tests/value/numerors/numerors.c:246: Warning: 
   Calling undeclared function DPRINTFrama_C_domain_show_each_ex10. Old style K&R code?
+[eva:experimental] Warning: The numerors domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -298,7 +298,7 @@
   In these functions, 257 statements reached (out of 257): 100% coverage.
   ----------------------------------------------------------------------------
   Some errors and warnings have been raised during the analysis:
-    by the Eva analyzer:      0 errors    0 warnings
+    by the Eva analyzer:      0 errors    1 warning
     by the Frama-C kernel:    0 errors    3 warnings
   ----------------------------------------------------------------------------
   0 alarms generated by the analysis.
diff --git a/tests/value/oracle/domains_function.res.oracle b/tests/value/oracle/domains_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..51ded1eb5fd5e3357568dc1f23ce53933d9e762c
--- /dev/null
+++ b/tests/value/oracle/domains_function.res.oracle
@@ -0,0 +1,272 @@
+[kernel] Parsing tests/value/domains_function.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  i ∈ {0}
+  result ∈ {0}
+  t[0..9] ∈ {0}
+[eva] tests/value/domains_function.c:117: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/value/domains_function.c:119.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/domains_function.c:119: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function test <- main.
+  Called from tests/value/domains_function.c:120.
+[eva] tests/value/domains_function.c:92: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function enabled <- test <- main.
+  Called from tests/value/domains_function.c:93.
+[eva] Recording results for enabled
+[eva] Done for function enabled
+[eva] tests/value/domains_function.c:94: Frama_C_show_each_singleton: {0}
+[eva] computing for function not_enabled <- test <- main.
+  Called from tests/value/domains_function.c:95.
+[eva] tests/value/domains_function.c:77: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for not_enabled
+[eva] Done for function not_enabled
+[eva] tests/value/domains_function.c:96: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function disabled <- test <- main.
+  Called from tests/value/domains_function.c:97.
+[eva] tests/value/domains_function.c:84: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for disabled
+[eva] Done for function disabled
+[eva] tests/value/domains_function.c:98: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for test
+[eva] Done for function test
+[eva] computing for function recursively_enabled <- main.
+  Called from tests/value/domains_function.c:121.
+[eva] tests/value/domains_function.c:107: Frama_C_show_each_singleton: {4}
+[eva] computing for function enabled <- recursively_enabled <- main.
+  Called from tests/value/domains_function.c:108.
+[eva] Recording results for enabled
+[eva] Done for function enabled
+[eva] tests/value/domains_function.c:109: Frama_C_show_each_singleton: {0}
+[eva] computing for function not_enabled <- recursively_enabled <- main.
+  Called from tests/value/domains_function.c:110.
+[eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+[eva] Recording results for not_enabled
+[eva] Done for function not_enabled
+[eva] tests/value/domains_function.c:111: Frama_C_show_each_singleton: {1}
+[eva] computing for function disabled <- recursively_enabled <- main.
+  Called from tests/value/domains_function.c:112.
+[eva] tests/value/domains_function.c:84: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for disabled
+[eva] Done for function disabled
+[eva] tests/value/domains_function.c:113: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for recursively_enabled
+[eva] Done for function recursively_enabled
+[eva] computing for function test_propagation <- main.
+  Called from tests/value/domains_function.c:122.
+[eva] computing for function infer <- test_propagation <- main.
+  Called from tests/value/domains_function.c:53.
+[eva] Recording results for infer
+[eva] Done for function infer
+[eva] computing for function no_use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:54.
+[eva] Recording results for no_use
+[eva] Done for function no_use
+[eva] tests/value/domains_function.c:55: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function nothing <- test_propagation <- main.
+  Called from tests/value/domains_function.c:56.
+[eva:alarm] tests/value/domains_function.c:21: Warning: 
+  signed overflow. assert -2147483648 ≤ t[i] - t[0];
+[eva:alarm] tests/value/domains_function.c:21: Warning: 
+  signed overflow. assert t[i] - t[0] ≤ 2147483647;
+[eva] Recording results for nothing
+[eva] Done for function nothing
+[eva] computing for function use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:57.
+[eva] Recording results for use
+[eva] Done for function use
+[eva] tests/value/domains_function.c:58: Frama_C_show_each_singleton: {42}
+[eva] computing for function kill <- test_propagation <- main.
+  Called from tests/value/domains_function.c:59.
+[eva] Recording results for kill
+[eva] Done for function kill
+[eva] computing for function use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:60.
+[eva] Recording results for use
+[eva] Done for function use
+[eva] tests/value/domains_function.c:61: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function no_infer <- test_propagation <- main.
+  Called from tests/value/domains_function.c:62.
+[eva] Recording results for no_infer
+[eva] Done for function no_infer
+[eva] tests/value/domains_function.c:63: Reusing old results for call to use
+[eva] tests/value/domains_function.c:64: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for test_propagation
+[eva] Done for function test_propagation
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function disabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function enabled:
+  result ∈ {0}
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function infer:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function kill:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function no_infer:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function no_use:
+  result ∈ [--..--]
+[eva:final-states] Values at end of function not_enabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function nothing:
+  tmp ∈ [--..--]
+[eva:final-states] Values at end of function recursively_enabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function test:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function use:
+  result ∈ [--..--]
+[eva:final-states] Values at end of function test_propagation:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ [0..9]
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[from] Computing for function disabled
+[from] Done for function disabled
+[from] Computing for function enabled
+[from] Done for function enabled
+[from] Computing for function infer
+[from] Done for function infer
+[from] Computing for function kill
+[from] Done for function kill
+[from] Computing for function no_infer
+[from] Done for function no_infer
+[from] Computing for function no_use
+[from] Done for function no_use
+[from] Computing for function not_enabled
+[from] Done for function not_enabled
+[from] Computing for function nothing
+[from] Done for function nothing
+[from] Computing for function recursively_enabled
+[from] Done for function recursively_enabled
+[from] Computing for function test
+[from] Done for function test
+[from] Computing for function use
+[from] Done for function use
+[from] Computing for function test_propagation
+[from] Done for function test_propagation
+[from] Computing for function main
+[from] Computing for function Frama_C_interval <-main
+[from] Done for function Frama_C_interval
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function disabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function infer:
+  t[0..9] FROM i (and SELF)
+[from] Function kill:
+  t[0] FROM undet
+[from] Function no_infer:
+  t[0..9] FROM i (and SELF)
+[from] Function no_use:
+  result FROM i; t[0..9]
+[from] Function not_enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function nothing:
+  NO EFFECTS
+[from] Function recursively_enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function test:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function use:
+  result FROM i; t[0..9]
+[from] Function test_propagation:
+  result FROM undet; i; t[1..9]
+  t[0] FROM undet; i
+   [1..9] FROM i (and SELF)
+[from] Function main:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  i FROM Frama_C_entropy_source
+  result FROM Frama_C_entropy_source; undet; t[1..9]
+  t[0] FROM Frama_C_entropy_source; undet
+   [1..9] FROM Frama_C_entropy_source; undet (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function disabled:
+    result; t[0..9]
+[inout] Inputs for function disabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function enabled:
+    result; t[0..9]
+[inout] Inputs for function enabled:
+    i; t[0..9]
+[inout] Out (internal) for function infer:
+    t[0..9]
+[inout] Inputs for function infer:
+    i
+[inout] Out (internal) for function kill:
+    t[0]
+[inout] Inputs for function kill:
+    undet
+[inout] Out (internal) for function no_infer:
+    t[0..9]
+[inout] Inputs for function no_infer:
+    i
+[inout] Out (internal) for function no_use:
+    result
+[inout] Inputs for function no_use:
+    i; t[0..9]
+[inout] Out (internal) for function not_enabled:
+    result; t[0..9]
+[inout] Inputs for function not_enabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function nothing:
+    tmp
+[inout] Inputs for function nothing:
+    i; t[0..9]
+[inout] Out (internal) for function recursively_enabled:
+    result; t[0..9]
+[inout] Inputs for function recursively_enabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function test:
+    result; t[0..9]
+[inout] Inputs for function test:
+    i; result; t[0..9]
+[inout] Out (internal) for function use:
+    result
+[inout] Inputs for function use:
+    i; t[0..9]
+[inout] Out (internal) for function test_propagation:
+    result; t[0..9]
+[inout] Inputs for function test_propagation:
+    undet; i; result; t[0..9]
+[inout] Out (internal) for function main:
+    Frama_C_entropy_source; i; result; t[0..9]; j
+[inout] Inputs for function main:
+    Frama_C_entropy_source; undet; i; result; t[0..9]
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 3d86f18943019f3f0a467294eb91a6e35ce14333..c89a9da2b49c07a5a9ee5a2c912b00d4e13952a3 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
 [kernel] Parsing tests/value/traces/test1.c (with preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 200e815eb5c348b65cc3bb4411ebf9401052ac21..3e1b821db9efd4784476373cafee29cc104913ef 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
 [kernel] Parsing tests/value/traces/test2.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index 1557613f54517aa6adcf22b46a8b6f617191eff7..bff1a57599b827a894c7723e22904c20bee9cebe 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
 [kernel] Parsing tests/value/traces/test3.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index ffd3f1dd1ce713fc3f9efc6ac926cd892952e725..45691fa981c5087f70854e4529ec6764fc659d45 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -1,5 +1,5 @@
-[eva:experimental] Warning: The traces domain is experimental.
 [kernel] Parsing tests/value/traces/test4.i (no preprocessing)
+[eva:experimental] Warning: The traces domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 0715058c74b454795f3d2ddd083afeb84b532d2f..739104c81f0f670a1edc22ac9d26de27c823251e 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -1,7 +1,7 @@
-[eva:experimental] Warning: The traces domain is experimental.
 [kernel] Parsing tests/value/traces/test5.i (no preprocessing)
 [kernel:typing:implicit-function-declaration] tests/value/traces/test5.i:21: Warning: 
   Calling undeclared function my_switch. Old style K&R code?
+[eva:experimental] Warning: The traces domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed