diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 232f8e12eecad61b6c0c6517b10fd1bd8dc882b5..a71352d34ce063b9face88d17cb1f7825b85d0dd 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -464,12 +464,6 @@ module type S = sig
   (** Category for the messages about the domain.
       Must be created through {!Value_parameters.register_category}. *)
   val log_category : Value_parameters.category
-end
-
-(** Full implementation of domains. Automatically built by
-    {!Domain_builder.Complete} from an {!S_with_Structure} domain. *)
-module type Internal = sig
-  include S
 
   (** This function is called after the analysis. The argument is the state
       computed at the return statement of the main function. The function can
@@ -485,7 +479,7 @@ type 't key = 't Structure.Key_Domain.key
 
 (** Signature for a leaf module of a domain. *)
 module type Leaf = sig
-  include Internal
+  include S
 
   (** The key identifies the domain and the type [t] of its states. *)
   val key: t key
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 1f3b2fdede76129a0c0827f6c3019fc7c4fc035f..3b8321d98f7a8553cd99c07700df949c83d8ddc2 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -370,7 +370,7 @@ module Make (Man : Input) = struct
   let top = Abstract1.top man empty_env
   let make_top env = Abstract1.top man env
 
-  include Datatype.Make_with_collections (
+  module D = Datatype.Make_with_collections (
     struct
       include Datatype.Undefined
       type t = state
@@ -402,6 +402,7 @@ module Make (Man : Input) = struct
 
       let mem_project = Datatype.never_any_project
     end )
+  include D
 
   let name = Man.name
 
@@ -428,6 +429,14 @@ module Make (Man : Input) = struct
     let s = Abstract1.meet man s1 s2 in
     if Abstract1.is_bottom man s then `Bottom else `Value s
 
+  include Domain_builder.Complete
+      (struct
+        include D
+        let name = name
+        let top = top
+        let join = join
+      end)
+
   let make_eval state =
     let env = Abstract1.env state in
     fun e ->
@@ -728,7 +737,7 @@ end
 let () = Floating_point.set_round_nearest_even ()
 
 let make name (module Man: Input) =
-  let module Domain = Domain_builder.Complete (Make (Man)) in
+  let module Domain = Make (Man) in
   let descr =
     "Binding to the " ^ name ^ " domain of the Apron library. " ^
     "See http://apron.cri.ensmp.fr/library for more details."
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index ac0278cd3d441c738f4684e4f36730dc0ce41635..0d48207dbda6cecb132797dd407e09c4aff43123 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -21,14 +21,20 @@
 (**************************************************************************)
 
 module type InputDomain = sig
-  include Abstract_domain.S
+  include Datatype.S
+  val top: t
+  val join: t -> t -> t
 end
 
-module Complete
-    (Domain: InputDomain)
-= struct
+module type LeafDomain = sig
+  type t
+  val post_analysis: t Bottom.or_bottom -> unit
+  module Store: Domain_store.S with type t := t
+  val key: t Abstract_domain.key
+end
+
+module Complete (Domain: InputDomain) = struct
 
-  include Domain
   module Store = Domain_store.Make (Domain)
 
   let key: Domain.t Structure.Key_Domain.key =
@@ -140,6 +146,7 @@ module Complete_Minimal
        : Datatype.S_with_collections with type t := t)
   end
 
+  include D
   include Complete (D)
 
 end
@@ -161,6 +168,7 @@ module Complete_Minimal_with_datatype
        : Datatype.S_with_collections with type t := t)
   end
 
+  include D
   include Complete (D)
 
 end
@@ -253,6 +261,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
     let reuse _kf _bases ~current_input:_ ~previous_output = previous_output
   end
 
+  include D
   include Complete (D)
 end
 
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index e27fcc16829920acee3094841a6b31114800aa52..5d76e37049443157acd6f91a77cc3ee578fda293 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -24,14 +24,19 @@
     simplified interfaces. *)
 
 module type InputDomain = sig
-  include Abstract_domain.S
+  include Datatype.S
+  val top: t
+  val join: t -> t -> t
 end
 
-module Complete
-    (Domain: InputDomain)
-  : Abstract_domain.Leaf with type state = Domain.state
-                          and type value = Domain.value
-                          and type location = Domain.location
+module type LeafDomain = sig
+  type t
+  val post_analysis: t Bottom.or_bottom -> unit
+  module Store: Domain_store.S with type t := t
+  val key: t Abstract_domain.key
+end
+
+module Complete (Domain: InputDomain) : LeafDomain with type t := Domain.t
 
 module Complete_Minimal
     (Value: Abstract_value.S)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index f14c28a4ec5f42e594a4481b95755a464da25bed..ced00ea1babace3fb59433affd4ff067891344af 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -538,6 +538,8 @@ module G = struct
       (Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)))
       (struct let module_name = "Values.Gauges_domain.G" end)
 
+  let name = "gauges"
+
   let empty = MV.empty, []
   let top (state: t) : t =
     let top_iteration_info = function
@@ -1117,7 +1119,7 @@ end
 
 let dkey = Value_parameters.register_category "d-gauges"
 
-module D_Impl : Abstract_domain.S
+module D : Abstract_domain.Leaf
   with type state = G.t
    and type value = Cvalue.V.t
    and type location = Precise_locs.precise_location
@@ -1128,8 +1130,8 @@ module D_Impl : Abstract_domain.S
   type origin
 
   include G
+  include Domain_builder.Complete (struct include G let top = empty end)
 
-  let name = "gauges"
   let log_category = dkey
 
   let empty _ = G.empty
@@ -1304,5 +1306,3 @@ module D_Impl : Abstract_domain.S
   let top = G.empty (* must not be used, not neutral w.r.t. join (because
                        join crashes...)!! *)
 end
-
-module D = Domain_builder.Complete (D_Impl)
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index bbcad31558f79453cbf1bd8b1357e5af06dc3c81..3d99d563f6c21429d3bc2188756607f0e57a97e9 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -95,6 +95,8 @@ module LatticeInout = struct
 
     end)
 
+  let name = "inout"
+
   (* Initial abstract at the beginning of the computation: nothing written
      or read so far. *)
   let empty = {
@@ -204,7 +206,7 @@ module Transfer = struct
 
 end
 
-module Internal
+module D
   (*: Domain_builder.InputDomain
     with type state = inout
     and type value = Cvalue.V.t
@@ -220,7 +222,8 @@ module Internal
              include Abstract_domain.Lattice with type state := state
            end)
 
-  let name = "inout"
+  include Domain_builder.Complete (LatticeInout)
+
   let log_category = Value_parameters.register_category "d-inout"
 
   let enter_scope _kind _vars state = state
@@ -284,9 +287,6 @@ module Internal
 
 end
 
-module D = Domain_builder.Complete (Internal)
-
-
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index fb5764a51511f4491b11a7514d17624161f6a9d6..e9928248897b008aa9ef13ce49270d2baa05d93f 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -231,7 +231,7 @@ struct
 end
 
 
-module DomainPrototype =
+module DomainLattice =
 struct
   (* The domain is essentially a map from bases to individual memory abstractions *)
   module Initial_Values = struct let v = [[]] end
@@ -241,16 +241,6 @@ struct
       (Base.Base) (Memory)
       (Hptmap.Comp_unused) (Initial_Values) (Deps)
 
-  type state = t
-  type value = Value.t
-  type base = Base.t
-  type offset = Location.offset
-  type memory = Memory.t
-  type location = Precise_locs.precise_location
-  type mdlocation = Location.t (* should be = to location *)
-  type origin
-
-
   let name = "multidim"
   let log_category = dkey
 
@@ -295,6 +285,23 @@ struct
     in
     inter ~cache:Hptmap_sig.NoCache ~symmetric:false ~idempotent:true ~decide
 
+end
+
+module Domain =
+struct
+
+  include DomainLattice
+  include Domain_builder.Complete (DomainLattice)
+
+  type state = t
+  type value = Value.t
+  type base = Base.t
+  type offset = Location.offset
+  type memory = Memory.t
+  type location = Precise_locs.precise_location
+  type mdlocation = Location.t (* should be = to location *)
+  type origin
+
 
   (* Bases handling *)
 
@@ -556,7 +563,7 @@ struct
   let relate _kf _bases _state = Base.SetLattice.empty
 
   let filter _kf _kind bases state =
-    filter (fun elt -> Base.Hptset.mem elt bases) state
+    DomainLattice.filter (fun elt -> Base.Hptset.mem elt bases) state
 
   let reuse _kf bases ~current_input ~previous_output =
     let cache = Hptmap_sig.NoCache in
@@ -569,5 +576,4 @@ struct
       current_input previous_output
 end
 
-
-include Domain_builder.Complete (DomainPrototype)
+include Domain
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index cdccda505e95c46436496c395cc4233bc124e906..5b0fa4115085ad8829e2a6614be0e47335ef2380 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -753,6 +753,9 @@ module State = struct
           Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
       end)
 
+  let name = "octagon"
+  let log_category = Value_parameters.register_category "d-octagon"
+
   let pretty_debug fmt { octagons; intervals; relations } =
     Format.fprintf fmt "@[<v> Octagons: %a@; Intervals: %a@; Relations: %a@]"
       Octagons.pretty octagons Intervals.pretty intervals
@@ -1034,6 +1037,7 @@ end
 module Domain = struct
 
   include State
+  include Domain_builder.Complete (State)
 
   type value = Cvalue.V.t
   type location = Precise_locs.precise_location
@@ -1320,8 +1324,6 @@ module Domain = struct
             relations = join_rel prev_output.relations current_input.relations;
             modified = current_input.modified }
 
-  let name = "octagon"
-  let log_category = Value_parameters.register_category "d-octagon"
 end
 
-include Domain_builder.Complete (Domain)
+include Domain
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 2818f14c91fd7098d7031a51ff917c800db11178..7f4e4b4846bb38975dd5dcf0a62924e855fbb2f3 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -86,10 +86,12 @@ module Memory = struct
     widen wh s1 s2
 
   let narrow x _y = `Value x
+
+  let name = "bitwise"
 end
 
 
-module Internal  : Domain_builder.InputDomain
+module D : Abstract_domain.Leaf
   with type state = Memory.t
    and type value = offsm_or_top
    and type location = Precise_locs.precise_location
@@ -104,7 +106,8 @@ module Internal  : Domain_builder.InputDomain
              include Abstract_domain.Lattice with type state := state
            end)
 
-  let name = "bitwise"
+  include Domain_builder.Complete (Memory)
+
   let log_category = dkey
 
   let empty _ = Memory.empty_map
@@ -233,6 +236,3 @@ module Internal  : Domain_builder.InputDomain
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 end
-
-
-module D = Domain_builder.Complete (Internal)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index b8260e5834de57a281343c8a1ca36d506417860a..80c5dbce55e2f322c2e47d4c8633fcd4df4ec0be 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -176,7 +176,7 @@ module Make_Memory (Value: Value) = struct
 
 end
 
-module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
+module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
 
   let table = Hashtbl.create 17
   let () =
@@ -186,7 +186,10 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
     try Some (Hashtbl.find table name)
     with Not_found -> None
 
-  include Make_Memory (Value)
+  module M = Make_Memory (Value)
+  include M
+
+  include Domain_builder.Complete (M)
 
   let name = Info.name
 
@@ -344,13 +347,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
     merge ~cache ~symmetric:false ~idempotent:true
       ~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
       current_input previous_output
-end
 
-
-module Make_Domain (Info: sig val name: string end) (Value: Value) =
-struct
-  module M = Make_Internal (Info) (Value)
-  include Domain_builder.Complete (M)
   let add = M.add
   let find = M.find
   let remove = M.remove
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 840e4fdbb09e6d5af87809663168a7cf5fb30f44..8e49fd93cf70384a2f941322f85a20c67e7b8f7d 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -215,6 +215,8 @@ module Memory = struct
 
     end)
 
+  let name = "symbolic-locations"
+
   let top = {
     values = K2V.M.empty;
     zones = K2Z.empty;
@@ -454,7 +456,7 @@ module Memory = struct
       syntactic_deps = B2K.union into.syntactic_deps t.syntactic_deps }
 end
 
-module Internal : Domain_builder.InputDomain
+module D : Abstract_domain.Leaf
   with type state = Memory.t
    and type value = V.t
    and type location = Precise_locs.precise_location
@@ -469,7 +471,8 @@ module Internal : Domain_builder.InputDomain
              include Abstract_domain.Lattice with type state := state
            end)
 
-  let name = "symbolic-locations"
+  include Domain_builder.Complete (Memory)
+
   let log_category = dkey
 
   let empty _ = Memory.empty_map
@@ -640,5 +643,3 @@ module Internal : Domain_builder.InputDomain
   let evaluate_predicate _ _ _ = Alarmset.Unknown
   let reduce_by_predicate _ state _ _ = `Value state
 end
-
-module D = Domain_builder.Complete (Internal)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 6bf2ad5f6e7b23446ef752e3f7e7cafe59d20a6d..6ac9fe86559e41ce975f80e7cb00b0cd90c38fe9 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -106,6 +106,8 @@ module LatticeTaint = struct
 
     end)
 
+  let name = "taint"
+
   (* Initial state at the start of the computation: nothing is tainted yet. *)
   let empty = {
     locs_data = Zone.bottom;
@@ -329,7 +331,7 @@ module ReuseTaint = struct
 end
 
 
-module InternalTaint = struct
+module TaintDomain = struct
   type state = taint
   type value = Cvalue.V.t
   type location = Precise_locs.precise_location
@@ -340,6 +342,8 @@ module InternalTaint = struct
              include Abstract_domain.Lattice with type state := state
            end)
 
+  include Domain_builder.Complete (LatticeTaint)
+
   include (QueriesTaint: Abstract_domain.Queries
            with type state := state
             and type value := value
@@ -354,7 +358,6 @@ module InternalTaint = struct
 
   include (ReuseTaint: Abstract_domain.Reuse with type t := state)
 
-  let name = "taint"
   let log_category = dkey
 
 
@@ -415,5 +418,4 @@ module InternalTaint = struct
   let leave_loop _ state = state
 end
 
-
-include Domain_builder.Complete (InternalTaint)
+include TaintDomain
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index e29351acf715363ec2ea0db7f59811acee8000e6..25e01df3368bea33093937920ab65e6b738be34d 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -571,6 +571,8 @@ module Traces = struct
 
     end)
 
+  let name = "traces"
+
   let view m =
     if m == top then `Top
     else `Other m
@@ -844,174 +846,6 @@ let rec complete_graph (graph:Graph.t) =
     ) graph Graph.empty
 
 
-module Internal = struct
-  type nonrec state = state
-  type value = Cvalue.V.t
-  type location = Precise_locs.precise_location
-  type origin
-
-  include (Traces: sig
-             include Datatype.S_with_collections with type t = state
-             include Abstract_domain.Lattice with type state := state
-           end)
-
-  let name = "traces"
-  let log_category = Value_parameters.register_category "d-traces"
-
-  let assign ki lv e _v _valuation state =
-    let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
-    `Value (Traces.add_trans state trans)
-
-  let assume stmt e pos _valuation state =
-    let trans = Assume (stmt, e, pos) in
-    `Value (Traces.add_trans state trans)
-
-  let start_call stmt call _recursion _valuation state =
-    let kf = call.Eval.kf in
-    if Kernel_function.is_definition kf then
-      let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
-          (Kernel_function.is_definition call.Eval.kf) in
-      let state = Traces.add_trans state (Msg msg) in
-      let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
-      let state = Traces.add_trans state (EnterScope (kf, formals)) in
-      let state = List.fold_left (fun state arg ->
-          Traces.add_trans state
-            (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
-                     arg.Eval.formal.Cil_types.vtype,
-                     arg.Eval.concrete))) state call.Eval.arguments in
-      `Value state
-    else
-      (** enter the scope of the dumb result variable *)
-      let var = call.Eval.return in
-      let state = match var with
-        | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
-        | None -> state in
-      let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
-      let state = Traces.add_trans state
-          (CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
-      in `Value {state with call_declared_function = true}
-
-  let finalize_call _stmt call _recursion ~pre:_ ~post =
-    if post.call_declared_function
-    then `Value {post with call_declared_function = false}
-    else
-      let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
-      let state = Traces.add_trans post (Msg msg) in
-      `Value state
-
-  let update _valuation state = `Value state
-
-  let show_expr _valuation state fmt _expr = Traces.pretty fmt state
-
-  (* Memexec *)
-  (* This domains infers no relation between variables. *)
-  let relate _kf _bases _state = Base.SetLattice.bottom
-  (* Do not filter the state: the memexec cache will be applied only on function
-     calls for which the entry states are equal. This almost completely
-     disable memexec, but is always sound. *)
-  let filter _kf _kind _bases state = state
-  (* As memexec cache is only applied on equal entry states, the previous
-     output state is a correct output for the current input state. *)
-  let reuse _kf _bases ~current_input:_ ~previous_output:state = state
-
-  let empty () = Traces.empty
-  let initialize_variable lv _ ~initialized:_ _ state =
-    Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
-  let initialize_variable_using_type var_kind varinfo state =
-    let kind_str =
-      match var_kind with
-      | Abstract_domain.Global   -> "global"
-      | Abstract_domain.Local _  -> "local"
-      | Abstract_domain.Formal _ -> "formal"
-      | Abstract_domain.Result _ -> "result"
-    in
-    let msg =
-      Format.asprintf "initialize@ %s variable@ using@ type@ %a"
-        kind_str Varinfo.pretty varinfo
-    in
-    Traces.add_trans state (Msg msg)
-
-  (* TODO *)
-  let logic_assign _assign _location state =
-    Traces.add_trans state (Msg "logic assign")
-
-  (* Logic *)
-  let evaluate_predicate _ _ _ = Alarmset.Unknown
-  let reduce_by_predicate _ state _ _ = `Value state
-
-  let top_query = `Value (Cvalue.V.top, None), Alarmset.all
-
-  let extract_expr ~oracle:_ _context _state _expr = top_query
-  let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
-
-  let backward_location _state _lval _typ loc value =
-    `Value (loc, value)
-
-  let enter_loop stmt state =
-    let state = Traces.add_trans state (Msg "enter_loop") in
-    let state = if not (Value_parameters.TracesUnrollLoop.get ())
-      then Traces.add_loop stmt state
-      else { state with current = UnrollLoop(stmt,state.current) } in
-    state
-
-  let incr_loop_counter _ state =
-    match state.current with
-    | Base _ -> assert false
-    | UnrollLoop(_,_) -> state
-    | OpenLoop(stmt,s,last,_,g,l) ->
-      let last = Graph.join last g in
-      let last = if Value_parameters.TracesUnifyLoop.get () then
-          let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
-          let last = Graph.join last old_last in
-          assert (Node.equal s s');
-          Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
-          last
-        else last
-      in
-      let current = OpenLoop(stmt,s,last,s,Graph.empty,l) in
-      let state = { state with current } in
-      (* Traces.add_trans state (Msg("incr_loop_counter")) *)
-      state
-
-  let leave_loop stmt' state =
-    match state.current with
-    | Base _ -> assert false (* absurd: we are in at least a loop *)
-    | UnrollLoop(_,l) -> { state with current = l }
-    | OpenLoop(stmt,s,last,old_current_node,g,current) ->
-      assert (Stmt.equal stmt stmt');
-      let state = { state with current } in
-      let last = if Value_parameters.TracesUnifyLoop.get () then
-          let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
-          let last = Graph.join last old_last in
-          assert (Node.equal s s');
-          Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
-          last
-        else last
-      in
-      let state = if Graph.is_empty last then state
-        else Traces.add_trans state (Loop(stmt,s,last)) in
-      let state = Traces.copy_edges s old_current_node g state in
-      Traces.add_trans state (Msg "leave_loop")
-
-
-  let enter_scope kind vars state =
-    match kind with
-    | Abstract_domain.Global ->
-      { state with globals = vars @ state.globals }
-    | Abstract_domain.Formal kf ->
-      if Kernel_function.equal kf (fst (Globals.entry_point ()))
-      then { state with main_formals = vars @ state.main_formals }
-      else state
-    | Abstract_domain.(Local kf | Result kf) ->
-      Traces.add_trans state (EnterScope (kf, vars))
-
-  let leave_scope kf vars state =
-    Traces.add_trans state (LeaveScope (kf, vars))
-
-  let reduce_further _state _expr _value = [] (*Nothing intelligent to suggest*)
-
-end
-
 let dummy_loc = Location.unknown
 
 let subst_in_full var_mapping =
@@ -1250,15 +1084,179 @@ let project_of_cfg vreturn s =
 (*   ) () *)
 
 
-let output_dot filename state =
-  let out = open_out filename in
-  Value_parameters.feedback ~dkey:Internal.log_category "@[Output dot produced to %s.@]" filename;
-  (** *)
-  GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
-  close_out out
-
 module D = struct
-  include Domain_builder.Complete (Internal)
+  type nonrec state = state
+  type value = Cvalue.V.t
+  type location = Precise_locs.precise_location
+  type origin
+
+  include (Traces: sig
+             include Datatype.S_with_collections with type t = state
+             include Abstract_domain.Lattice with type state := state
+           end)
+
+  include Domain_builder.Complete (Traces)
+
+  let log_category = Value_parameters.register_category "d-traces"
+
+  let assign ki lv e _v _valuation state =
+    let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
+    `Value (Traces.add_trans state trans)
+
+  let assume stmt e pos _valuation state =
+    let trans = Assume (stmt, e, pos) in
+    `Value (Traces.add_trans state trans)
+
+  let start_call stmt call _recursion _valuation state =
+    let kf = call.Eval.kf in
+    if Kernel_function.is_definition kf then
+      let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
+          (Kernel_function.is_definition call.Eval.kf) in
+      let state = Traces.add_trans state (Msg msg) in
+      let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
+      let state = Traces.add_trans state (EnterScope (kf, formals)) in
+      let state = List.fold_left (fun state arg ->
+          Traces.add_trans state
+            (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
+                     arg.Eval.formal.Cil_types.vtype,
+                     arg.Eval.concrete))) state call.Eval.arguments in
+      `Value state
+    else
+      (** enter the scope of the dumb result variable *)
+      let var = call.Eval.return in
+      let state = match var with
+        | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
+        | None -> state in
+      let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
+      let state = Traces.add_trans state
+          (CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
+      in `Value {state with call_declared_function = true}
+
+  let finalize_call _stmt call _recursion ~pre:_ ~post =
+    if post.call_declared_function
+    then `Value {post with call_declared_function = false}
+    else
+      let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
+      let state = Traces.add_trans post (Msg msg) in
+      `Value state
+
+  let update _valuation state = `Value state
+
+  let show_expr _valuation state fmt _expr = Traces.pretty fmt state
+
+  (* Memexec *)
+  (* This domains infers no relation between variables. *)
+  let relate _kf _bases _state = Base.SetLattice.bottom
+  (* Do not filter the state: the memexec cache will be applied only on function
+     calls for which the entry states are equal. This almost completely
+     disable memexec, but is always sound. *)
+  let filter _kf _kind _bases state = state
+  (* As memexec cache is only applied on equal entry states, the previous
+     output state is a correct output for the current input state. *)
+  let reuse _kf _bases ~current_input:_ ~previous_output:state = state
+
+  let empty () = Traces.empty
+  let initialize_variable lv _ ~initialized:_ _ state =
+    Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
+  let initialize_variable_using_type var_kind varinfo state =
+    let kind_str =
+      match var_kind with
+      | Abstract_domain.Global   -> "global"
+      | Abstract_domain.Local _  -> "local"
+      | Abstract_domain.Formal _ -> "formal"
+      | Abstract_domain.Result _ -> "result"
+    in
+    let msg =
+      Format.asprintf "initialize@ %s variable@ using@ type@ %a"
+        kind_str Varinfo.pretty varinfo
+    in
+    Traces.add_trans state (Msg msg)
+
+  (* TODO *)
+  let logic_assign _assign _location state =
+    Traces.add_trans state (Msg "logic assign")
+
+  (* Logic *)
+  let evaluate_predicate _ _ _ = Alarmset.Unknown
+  let reduce_by_predicate _ state _ _ = `Value state
+
+  let top_query = `Value (Cvalue.V.top, None), Alarmset.all
+
+  let extract_expr ~oracle:_ _context _state _expr = top_query
+  let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
+
+  let backward_location _state _lval _typ loc value =
+    `Value (loc, value)
+
+  let enter_loop stmt state =
+    let state = Traces.add_trans state (Msg "enter_loop") in
+    let state = if not (Value_parameters.TracesUnrollLoop.get ())
+      then Traces.add_loop stmt state
+      else { state with current = UnrollLoop(stmt,state.current) } in
+    state
+
+  let incr_loop_counter _ state =
+    match state.current with
+    | Base _ -> assert false
+    | UnrollLoop(_,_) -> state
+    | OpenLoop(stmt,s,last,_,g,l) ->
+      let last = Graph.join last g in
+      let last = if Value_parameters.TracesUnifyLoop.get () then
+          let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
+          let last = Graph.join last old_last in
+          assert (Node.equal s s');
+          Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
+          last
+        else last
+      in
+      let current = OpenLoop(stmt,s,last,s,Graph.empty,l) in
+      let state = { state with current } in
+      (* Traces.add_trans state (Msg("incr_loop_counter")) *)
+      state
+
+  let leave_loop stmt' state =
+    match state.current with
+    | Base _ -> assert false (* absurd: we are in at least a loop *)
+    | UnrollLoop(_,l) -> { state with current = l }
+    | OpenLoop(stmt,s,last,old_current_node,g,current) ->
+      assert (Stmt.equal stmt stmt');
+      let state = { state with current } in
+      let last = if Value_parameters.TracesUnifyLoop.get () then
+          let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
+          let last = Graph.join last old_last in
+          assert (Node.equal s s');
+          Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
+          last
+        else last
+      in
+      let state = if Graph.is_empty last then state
+        else Traces.add_trans state (Loop(stmt,s,last)) in
+      let state = Traces.copy_edges s old_current_node g state in
+      Traces.add_trans state (Msg "leave_loop")
+
+
+  let enter_scope kind vars state =
+    match kind with
+    | Abstract_domain.Global ->
+      { state with globals = vars @ state.globals }
+    | Abstract_domain.Formal kf ->
+      if Kernel_function.equal kf (fst (Globals.entry_point ()))
+      then { state with main_formals = vars @ state.main_formals }
+      else state
+    | Abstract_domain.(Local kf | Result kf) ->
+      Traces.add_trans state (EnterScope (kf, vars))
+
+  let leave_scope kf vars state =
+    Traces.add_trans state (LeaveScope (kf, vars))
+
+  let reduce_further _state _expr _value = [] (*Nothing intelligent to suggest*)
+
+  let output_dot filename state =
+    let out = open_out filename in
+    Value_parameters.feedback ~dkey:log_category "@[Output dot produced to %s.@]" filename;
+    (** *)
+    GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
+    close_out out
 
   let post_analysis state =
     let return_stmt = Kernel_function.find_return (fst (Globals.entry_point ())) in
@@ -1267,7 +1265,7 @@ module D = struct
       | _ -> assert false in
     let header fmt = Format.fprintf fmt "Trace domains:" in
     let body = Bottom.pretty Traces.pretty in
-    Value_parameters.printf ~dkey:Internal.log_category ~header " @[%a@]" body state;
+    Value_parameters.printf ~dkey:log_category ~header " @[%a@]" body state;
     if Value_parameters.TracesProject.get () ||
        not (Value_parameters.TracesDot.is_default ()) then
       match state with
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index b7158ae6e3f5c13f22e31e947a78e864a08b6471..84c9df4689093ad239daf553731854a390db5df3 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -72,13 +72,13 @@ end
 module Domain = struct
 
   module D = struct
-    type 'a t = (module Abstract_domain.Internal with type state = 'a)
+    type 'a t = (module Abstract_domain.S with type state = 'a)
   end
 
   include Structure.Shape (Structure.Key_Domain) (D)
 
   module type Internal = sig
-    include Abstract_domain.Internal
+    include Abstract_domain.S
     val structure: t structure
   end
 
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 643159a7b0008376843b36481d5f04a784d2aaae..5ea4d7e853139c34ab46a47c8e438f35adfcd45e 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -98,10 +98,10 @@ end
 module Domain : sig
   include Structure.Shape
     with type 'a key = 'a Structure.Key_Domain.key
-     and type 'a data = (module Abstract_domain.Internal with type state = 'a)
+     and type 'a data = (module Abstract_domain.S with type state = 'a)
 
   module type Internal = sig
-    include Abstract_domain.Internal
+    include Abstract_domain.S
     val structure: t structure
   end