diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 88937d027a..34d5b1a89b 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -13,7 +13,8 @@ struct
   module D = BoolDomain.MustBool
   module C = Printable.Unit
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
+  let startcontext () = ()
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 24cb7399bc..bf1892fdf0 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -14,7 +14,7 @@ struct
   let name () = "access"
 
   module D = Lattice.Unit
-  module C = Printable.Unit
+  include Analyses.ValueContexts(D)
 
   module V =
   struct
@@ -52,11 +52,12 @@ struct
     );
     if M.tracing then M.traceu "access" "access_one_top"
 
+
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
   let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
-  let context fd d = ()
+  let context ctx fd d = ()
 
 
   (** Transfer functions: *)
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index be13489993..69db900d4c 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/src/analyses/activeSetjmp.ml
@@ -10,7 +10,7 @@ struct
   let name () = "activeSetjmp"
 
   module D = JmpBufDomain.JmpBufSet
-  module C = JmpBufDomain.JmpBufSet
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index fa220552f1..e9c21ae1a3 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -20,7 +20,7 @@ struct
   module Priv = Priv (RD)
   module D = RelationDomain.RelComponents (RD) (Priv.D)
   module G = Priv.G
-  module C = D
+  include Analyses.ValueContexts(D)
   module V =
   struct
     include Priv.V
@@ -40,7 +40,7 @@ struct
   (* Result map used for comparison of results for relational traces paper. *)
   let results = PCU.RH.create 103
 
-  let context fd x =
+  let context ctx fd x =
     if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.relation.context" ~removeAttr:"relation.no-context" ~keepAttr:"relation.context" fd then
       x
     else
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4385f1fca8..67e6276239 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -38,7 +38,7 @@ struct
   module Dom    = BaseDomain.DomFunctor (Priv.D) (RVEval)
   type t = Dom.t
   module D      = Dom
-  module C      = Dom
+  include Analyses.ValueContexts(D)
 
   (* Two global invariants:
      1. Priv.V -> Priv.G  --  used for Priv
@@ -79,6 +79,7 @@ struct
   type glob_diff = (V.t * G.t) list
 
   let name () = "base"
+
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
 
@@ -622,7 +623,7 @@ struct
 
   let drop_intervalSet = CPA.map (function Int x -> Int (ID.no_intervalSet x) | x -> x )
 
-  let context (fd: fundec) (st: store): store =
+  let context ctx (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
     (* Here earlyglobs only drops syntactic globals from the context and does not consider e.g. escaped globals. *)
diff --git a/src/analyses/callstring.ml b/src/analyses/callstring.ml
index a8734cdf1c..391f5f6657 100644
--- a/src/analyses/callstring.ml
+++ b/src/analyses/callstring.ml
@@ -1,7 +1,7 @@
 (**
-   Call String analysis [call_string] and/or Call Site analysis [call_site]. 
-   The call string limitation for both approaches can be adjusted with the "callString_length" option. 
-   By adding new implementations of the CallstringType, additional analyses can be added. 
+   Call String analysis [call_string] and/or Call Site analysis [call_site].
+   The call string limitation for both approaches can be adjusted with the "callString_length" option.
+   By adding new implementations of the CallstringType, additional analyses can be added.
 *)
 
 open Analyses
@@ -18,20 +18,22 @@ end
 
 (** Analysis with infinite call string or with limited call string (k-CFA, tracks the last k call stack elements).
     With the CT argument it is possible to specify the type of the call string elements *)
-module Spec (CT:CallstringType) : MCPSpec = 
+module Spec (CT:CallstringType) : MCPSpec =
 struct
-  include Analyses.IdentitySpec
+  include UnitAnalysis.Spec
 
   (* simulates a call string (with or without limitation)*)
   module CallString = struct
     include Printable.PQueue (CT)
 
+    let (empty:t) = BatDeque.empty
+
     (* pushes "elem" to the call string, guarantees a depth of k if limitation is specified with "ana.context.callString_length" *)
-    let push callstr elem = 
+    let push callstr elem =
       match elem with
       | None -> callstr
-      | Some e -> 
-        let new_callstr = BatDeque.cons e callstr in (* pushes new element to callstr *)     
+      | Some e ->
+        let new_callstr = BatDeque.cons e callstr in (* pushes new element to callstr *)
         if get_int "ana.context.callString_length" < 0
         then new_callstr (* infinite call string *)
         else (* maximum of k elements *)
@@ -41,38 +43,24 @@ struct
           | _ -> failwith "CallString Error: It shouldn't happen that more than one element must be deleted to maintain the correct height!"
   end
 
-  module D = Lattice.Flat (CallString) (* should be the CallString (C=D). Since a Lattice is required, Lattice.Flat is used to fulfill the type *) 
   module C = CallString
-  module V = EmptyV
-  module G = Lattice.Unit
 
   let name () = "call_"^ CT.ana_name
-  let startstate v = `Lifted (BatDeque.empty)
-  let exitstate v =  `Lifted (BatDeque.empty)
-
-  let context fd x = match x with 
-    | `Lifted x -> x
-    | _ -> failwith "CallString: Context error! The context cannot be derived from Top or Bottom!"
-
-  let callee_state ctx f = 
-    let elem = CT.new_ele f ctx in (* receive element that should be added to call string *)
-    let new_callstr = CallString.push (context f ctx.local) elem in
-    `Lifted new_callstr
-
-  let enter ctx r f args = [ctx.local, callee_state ctx f]
 
-  let combine_env ctx lval fexp f args fc au f_ask = ctx.local
+  let startcontext () = CallString.empty
 
-  let threadenter ctx ~multiple lval v args = [callee_state ctx (Cilfacade.find_varinfo_fundec v)]
+  let context ctx fd _ =
+    let elem = CT.new_ele fd ctx in (* receive element that should be added to call string *)
+    CallString.push (ctx.context ()) elem
 end
 
 (* implementations of CallstringTypes*)
 module Callstring: CallstringType = struct
   include CilType.Fundec
   let ana_name = "string"
-  let new_ele f ctx = 
-    let f' = Node.find_fundec ctx.node in 
-    if CilType.Fundec.equal f' dummyFunDec 
+  let new_ele f ctx =
+    let f' = Node.find_fundec ctx.node in
+    if CilType.Fundec.equal f' dummyFunDec
     then None
     else Some f'
 end
@@ -80,7 +68,7 @@ end
 module Callsite: CallstringType = struct
   include CilType.Stmt
   let ana_name = "site"
-  let new_ele f ctx = 
+  let new_ele f ctx =
     match ctx.prev_node with
     | Statement stmt -> Some stmt
     | _ -> None (* first statement is filtered *)
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 393be0a857..22b9db1cd4 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -58,7 +58,7 @@ struct
 
   let name () = "condvars"
   module D = Domain
-  module C = Domain
+  include Analyses.ValueContexts(D)
 
   (* >? is >>=, |? is >> *)
   let (>?) = Option.bind
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index fef3d9ff9f..46ec4774e5 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -13,7 +13,7 @@ struct
   let name () = "expsplit"
 
   module D = MapDomain.MapBot (Basetype.CilExp) (ID)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let startstate v = D.bot ()
   let exitstate = startstate
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 6cc347d511..a61c54ab96 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -866,7 +866,7 @@ module Spec : Analyses.MCPSpec = struct
   (** Domains *)
   module D = PthreadDomain.D
 
-  module C = D
+  include Analyses.ValueContexts(D)
 
   (** Set of created tasks to spawn when going multithreaded *)
   module G = Tasks
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 6a816b9e6c..aad8e0119a 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -15,7 +15,7 @@ struct
   let name () = "lockset"
 
   module D = D
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let startstate v = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]
diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
index ab768e235d..66a50c17b7 100644
--- a/src/analyses/loopTermination.ml
+++ b/src/analyses/loopTermination.ml
@@ -30,7 +30,8 @@ struct
   let name () = "termination"
 
   module D = Lattice.Unit
-  module C = D
+  include Analyses.ValueContexts(D)
+
   module V = struct
     include UnitV
     let is_write_only _ = true
diff --git a/src/analyses/loopfreeCallstring.ml b/src/analyses/loopfreeCallstring.ml
index 172114d37c..d9760e58a0 100644
--- a/src/analyses/loopfreeCallstring.ml
+++ b/src/analyses/loopfreeCallstring.ml
@@ -1,60 +1,49 @@
-(** 
+(**
    Loopfree Callstring analysis [loopfree_callstring] that reduces the call string length of the classical Call String approach for recursions
-   The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set 
+   The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set
    In case no call cycles appears, the call string is identical to the call string of the Call String approach
-   For example: 
+   For example:
    - call string [main, a, b, c, a] is represented as [main, {a, b, c}]
    - call string [main, a, a, b, b, b] is represented as [main, {a}, {b}]
 
    This approach is inspired by
-   @see <https://arxiv.org/abs/2301.06439> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F. 
+   @see <https://arxiv.org/abs/2301.06439> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F.
 *)
 open Analyses
 
 module Spec : MCPSpec =
 struct
-  include Analyses.IdentitySpec
+  include UnitAnalysis.Spec
 
   let name () = "loopfree_callstring"
 
   module FundecSet = SetDomain.Make (CilType.Fundec)
-  module Either =  Printable.Either (CilType.Fundec) (FundecSet) 
-
-  module D = Lattice.Flat (Printable.Liszt (Either)) (* A domain element is a list containing fundecs and sets of fundecs.*) 
-  module C = D
-  module V = EmptyV
-  module G = Lattice.Unit
-  let startstate v = `Lifted([])
-  let exitstate  v = `Lifted([])
-
-  let get_list list = match list with
-    | `Lifted e -> e
-    | _ -> failwith "Error loopfreeCallstring (get_list): The list cannot be derived from Top or Bottom!"
-
-  let loop_detected f = function
-    (* note: a call string contains each Fundec at most once *)
-    | `Left ele -> CilType.Fundec.equal f ele
-    | `Right set -> FundecSet.mem f set 
-
-  let add_to_set old = function
-    | `Left ele -> FundecSet.add ele old
-    | `Right set -> FundecSet.join old set
-
-  let rec callee_state f prev_set prev_list = function
-    | [] -> (`Left f)::(List.rev prev_list) (* f is not yet contained in the call string *)
-    | e::rem_list -> 
-      let new_set = add_to_set prev_set e in
-      if loop_detected f e (* f is already present in the call string *)
-      then (`Right new_set)::rem_list (* combine all elements of the call cycle in a set *)
-      else callee_state f new_set (e::prev_list) rem_list
-
-  let callee_state f ctx = `Lifted(callee_state f (FundecSet.empty ()) [] (get_list ctx.local))
-
-  let enter ctx r f args = [ctx.local, callee_state f ctx]
-
-  let threadenter ctx ~multiple lval v args = [callee_state (Cilfacade.find_varinfo_fundec v) ctx]
-
-  let combine_env ctx lval fexp f args fc au f_ask = ctx.local
+  module Either =  Printable.Either (CilType.Fundec) (FundecSet)
+
+  module C = Printable.Liszt (Either)
+
+  let append fd current =
+    let loop_detected f = function
+      (* note: a call string contains each Fundec at most once *)
+      | `Left ele -> CilType.Fundec.equal f ele
+      | `Right set -> FundecSet.mem f set
+    in
+    let add_to_set old = function
+      | `Left ele -> FundecSet.add ele old
+      | `Right set -> FundecSet.join old set
+    in
+    let rec append f prev_set prev_list = function
+      | [] -> (`Left f)::(List.rev prev_list) (* f is not yet contained in the call string *)
+      | e::rem_list ->
+        let new_set = add_to_set prev_set e in
+        if loop_detected f e (* f is already present in the call string *)
+        then (`Right new_set)::rem_list (* combine all elements of the call cycle in a set *)
+        else append f new_set (e::prev_list) rem_list
+    in
+    append fd (FundecSet.empty ()) [] current
+
+  let startcontext () = []
+  let context ctx fd x = append fd (ctx.context ())
 end
 
 let _ = MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 50e2f62931..71c887dda5 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -83,10 +83,10 @@ struct
     check_deps !activated;
     activated := topo_sort_an !activated;
     begin
-      match get_string_list "ana.ctx_sens" with 
+      match get_string_list "ana.ctx_sens" with
       | [] -> (* use values of "ana.ctx_insens" (blacklist) *)
         let cont_inse = map' find_id @@ get_string_list "ana.ctx_insens" in
-        activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n cont_inse)) !activated;      
+        activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n cont_inse)) !activated;
       | sens -> (* use values of "ana.ctx_sens" (whitelist) *)
         let cont_sens = map' find_id @@ sens in
         activated_ctx_sens := List.filter (fun (n, _) -> List.mem n cont_sens) !activated;
@@ -113,19 +113,18 @@ struct
     let ys = fold_left one_el [] xs in
     List.rev ys, !dead
 
-  let context fd x =
-    let x = spec_list x in
-    filter_map (fun (n,(module S:MCPSpec),d) ->
-        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
-          None
-        else
-          Some (n, Obj.repr @@ S.context fd (Obj.obj d))
-      ) x
-
   let exitstate  v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, Obj.repr @@ S.exitstate  v) !activated
   let startstate v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, Obj.repr @@ S.startstate v) !activated
   let morphstate v x = map (fun (n,(module S:MCPSpec),d) -> n, Obj.repr @@ S.morphstate v (Obj.obj d)) (spec_list x)
 
+  let startcontext () =
+    filter_map (fun (n,{spec=(module S:MCPSpec); _}) ->
+        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
+          None
+        else
+          Some (n, Obj.repr @@ S.startcontext ())
+      ) !activated
+
   let rec assoc_replace (n,c) = function
     | [] -> failwith "assoc_replace"
     | (n',c')::xs -> if n=n' then (n,c)::xs else (n',c') :: assoc_replace (n,c) xs
@@ -235,6 +234,17 @@ struct
     if M.tracing then M.traceu "event" "";
     ctx'.local
 
+  and context ctx fd x =
+    let ctx'' = outer_ctx "context_computation" ctx in
+    let x = spec_list x in
+    filter_map (fun (n,(module S:MCPSpec),d) ->
+        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
+          None
+        else
+          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "context_computation" ctx'' n d in
+          Some (n, Obj.repr @@ S.context ctx' fd (Obj.obj d))
+      ) x
+
   and branch (ctx:(D.t, G.t, C.t, V.t) ctx) (e:exp) (tv:bool) =
     let spawns = ref [] in
     let splits = ref [] in
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index ca14de0a3c..020046c678 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -10,7 +10,7 @@ struct
 
   (* must fresh variables *)
   module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let name () = "mallocFresh"
 
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index f993db0c6e..5e6225caac 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -13,7 +13,7 @@ struct
 
   module Addr = ValueDomain.Addr
   module D = ValueDomain.AddrSetDomain
-  module C = ValueDomain.AddrSetDomain
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   (*
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index f2d707067d..362800b7b4 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -14,13 +14,13 @@ struct
   let name () = "memLeak"
 
   module D = ToppedVarInfoSet
-  module C = D
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   module V = UnitV
   module G = WasMallocCalled
 
-  let context _ d = d
+  let context ctx _ d = d
 
   let must_be_single_threaded ~since_start ctx =
     ctx.ask (Queries.MustBeSingleThreaded { since_start })
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 51304f5bf5..914644a86e 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -20,9 +20,9 @@ struct
   include Analyses.IdentitySpec
 
   module D = Lattice.Unit
-  module C = D
+  include Analyses.ValueContexts(D)
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
 
   let name () = "memOutOfBounds"
 
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 70f1624922..68c2bf4f34 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -14,7 +14,7 @@ struct
 
   let name () = "pthreadSignals"
   module D = MustSignals
-  module C = MustSignals
+  include Analyses.ValueContexts(D)
   module G = SetDomain.ToppedSet (MHP) (struct let topname = "All Threads" end)
 
   let possible_vinfos (a: Queries.ask) cv_arg =
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index c2b40ff12f..e53dded304 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -16,7 +16,8 @@ struct
 
   module D = RegionDomain.RegionDom
   module G = RegPart
-  module C = D
+  include Analyses.ValueContexts(D)
+
   module V =
   struct
     include Printable.UnitConf (struct let name = "partitions" end)
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index dd2cedf871..56656c0639 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -2,7 +2,6 @@
 
 open GoblintCil
 open Analyses
-module LF = LibraryFunctions
 
 module Spec (D: StackDomain.S) (N: sig val name : string end)=
 struct
@@ -10,7 +9,7 @@ struct
 
   let name () = N.name
   module D = D
-  module C = D
+  include Analyses.ValueContexts(D)
 
   (* transfer functions *)
 
@@ -31,7 +30,7 @@ struct
 
   let name () = "stack_loc"
   module D = StackDomain.Dom3
-  module C = StackDomain.Dom3
+  include Analyses.ValueContexts(D)
 
   (* transfer functions *)
 
@@ -41,7 +40,6 @@ struct
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
 
-
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 6fd18de6ff..cafb8f5376 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -24,7 +24,7 @@ struct
   exception Top
 
   module D = LockDomain.Symbolic
-  module C = LockDomain.Symbolic
+  include Analyses.ValueContexts(D)
 
   let name () = "symb_locks"
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index ed30e3633e..07f46e915d 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -12,7 +12,7 @@ struct
 
   let name () = "thread"
   module D = ConcDomain.CreatedThreadSet
-  module C = D
+  include Analyses.ValueContexts(D)
   module G = ConcDomain.ThreadCreation
   module V =
   struct
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index fd7c564f2f..4311e72558 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -21,7 +21,7 @@ struct
 
   let name () = "escape"
   module D = EscapeDomain.EscapedVars
-  module C = EscapeDomain.EscapedVars
+  include Analyses.ValueContexts(D)
   module V = VarinfoV
   module G = ThreadIdSet
 
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index a751ae074a..e1efcaaba5 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -19,13 +19,14 @@ struct
 
   module Flag = ThreadFlagDomain.Simple
   module D = Flag
-  module C = Flag
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
   module V = UnitV
   module G = BoolDomain.MayBool
 
   let name () = "threadflag"
 
+
   let startstate v = Flag.bot ()
   let exitstate  v = Flag.get_multi ()
 
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 70ae13661e..80bab1ebf9 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -53,14 +53,14 @@ struct
 
   (** Uniqueness Counter * TID * (All thread creates of current thread * All thread creates of the current function and its callees) *)
   module D = Lattice.Prod3 (N) (ThreadLifted) (Created)
-  module C = D
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   let tids = ref (Hashtbl.create 20)
 
   let name () = "threadid"
 
-  let context fd ((n,current,td) as d) =
+  let context ctx fd ((n,current,td) as d) =
     if GobConfig.get_bool "ana.thread.context.create-edges" then
       d
     else
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 160b123e78..eddbe184da 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -19,7 +19,7 @@ struct
   (* The first component is the set of must-joined TIDs, the second component tracks whether all TIDs recorded in MustTIDs have been exited cleanly, *)
   (* i.e., all created subthreads have also been joined. This is helpful as there is no set of all transitively created threads available. *)
   module D = Lattice.Prod(MustTIDs)(CleanExit)
-  module C = D
+  include Analyses.ValueContexts(D)
   module G = D
   module V =
   struct
@@ -105,6 +105,7 @@ struct
     let (callee_joined, callee_clean) = au in
     (MustTIDs.union caller_joined callee_joined, local_clean && callee_clean)
 
+
   let startstate v = (MustTIDs.empty (), true)
   let exitstate  v = (MustTIDs.empty (), true)
 end
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index 0aed06851a..f3b9622b00 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -13,7 +13,7 @@ struct
 
   let name () = "threadreturn"
   module D = IntDomain.Booleans
-  module C = D
+  include Analyses.ValueContexts(D)
 
   (* transfer functions *)
 
diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index 2c26ad33b6..28f7e0acdc 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -50,7 +50,7 @@ struct
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let startstate v = D.bot ()
   let exitstate = startstate
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 1015188d88..f62a5a4722 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -28,7 +28,9 @@ struct
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context _ _ = ()
+  let context ctx _ _ = ()
+  let startcontext () = ()
+
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
   let rec is_exp_tainted (state:D.t) (e:Cil.exp) = match e with
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 319d0039ba..225767f010 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -38,6 +38,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     ctx.local
 
+  let startcontext () = ()
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx ~multiple lval f args fctx = ctx.local
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 8693599a4d..a385d0a1cd 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -15,7 +15,7 @@ struct
   module Addr = ValueDomain.Addr
 
   module D = ValueDomain.AddrSetDomain
-  module C = ValueDomain.AddrSetDomain
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   type trans_in  = D.t
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index f56d3487bb..8ece99d6e8 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -38,7 +38,7 @@ struct
         ) ss (Invariant.top ())
   end
 
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let name () = "var_eq"
 
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index 9510304e56..eb9ec6ce02 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -57,7 +57,7 @@ struct
     else remove unique_call counter |> add unique_call (count + 1)
 
   module D = Lattice.Prod (NodeFlatLattice) (UniqueCallCounter)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let wrappers = Hashtbl.create 13
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index c8464f6e84..930793b60f 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -206,7 +206,8 @@ sig
   val morphstate : varinfo -> D.t -> D.t
   val exitstate  : varinfo -> D.t
 
-  val context : fundec -> D.t -> C.t
+  val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
+  val startcontext: unit -> C.t
 
   val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
@@ -375,7 +376,7 @@ struct
   let sync ctx _ = ctx.local
   (* Most domains do not have a global part. *)
 
-  let context fd x = x
+  let context ctx fd x = x
   (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
 
   let paths_as_set ctx = [ctx.local]
@@ -420,7 +421,13 @@ module IdentityUnitContextsSpec = struct
   include IdentitySpec
   module C = Printable.Unit
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
+  let startcontext () = ()
+end
+
+module ValueContexts (D:Lattice.S) = struct
+  module C = D
+  let startcontext () = D.top ()
 end
 
 module type SpecSys =
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 2d2fa80f8d..07180d54dd 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -43,13 +43,14 @@ struct
   let exitstate  v = D.lift (S.exitstate  v)
   let morphstate v d = D.lift (S.morphstate v (D.unlift d))
 
-  let context fd = S.context fd % D.unlift
-
   let conv ctx =
     { ctx with local = D.unlift ctx.local
              ; split = (fun d es -> ctx.split (D.lift d) es )
     }
 
+  let context ctx fd = S.context (conv ctx) fd % D.unlift
+  let startcontext () = S.startcontext ()
+
   let sync ctx reason =
     D.lift @@ S.sync (conv ctx) reason
 
@@ -125,11 +126,12 @@ struct
   let exitstate  = S.exitstate
   let morphstate = S.morphstate
 
-  let context fd = C.lift % S.context fd
-
   let conv ctx =
     { ctx with context = (fun () -> C.unlift (ctx.context ())) }
 
+  let context ctx fd = C.lift % S.context (conv ctx) fd
+  let startcontext () = C.lift @@ S.startcontext ()
+
   let sync ctx reason =
     S.sync (conv ctx) reason
 
@@ -224,13 +226,14 @@ struct
   let exitstate  v = (S.exitstate  v, !start_level)
   let morphstate v (d,l) = (S.morphstate v d, l)
 
-  let context fd (d,_) = S.context fd d
-
   let conv ctx =
     { ctx with local = fst ctx.local
              ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
     }
 
+  let context ctx fd (d,_) = S.context (conv ctx) fd d
+  let startcontext () = S.startcontext ()
+
   let lift_fun ctx f g h =
     f @@ h (g (conv ctx))
 
@@ -375,16 +378,19 @@ struct
 
   let inj f x = f x, M.bot ()
 
+  let startcontext () = S.startcontext ()
   let startstate = inj S.startstate
   let exitstate  = inj S.exitstate
   let morphstate v (d,m) = S.morphstate v d, m
 
-  let context fd (d,m) = S.context fd d (* just the child analysis' context *)
 
   let conv ctx =
     { ctx with local = fst ctx.local
              ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
     }
+
+  let context ctx fd (d,m) = S.context (conv ctx) fd d (* just the child analysis' context *)
+
   let lift_fun ctx f g = g (f (conv ctx)), snd ctx.local
 
   let sync ctx reason = lift_fun ctx S.sync   ((|>) reason)
@@ -453,17 +459,20 @@ struct
   let init = S.init
   let finalize = S.finalize
 
+
+  let startcontext () = S.startcontext ()
   let startstate v = `Lifted (S.startstate v)
   let exitstate  v = `Lifted (S.exitstate  v)
   let morphstate v d = try `Lifted (S.morphstate v (D.unlift d)) with Deadcode -> d
 
-  let context fd = S.context fd % D.unlift
 
   let conv ctx =
     { ctx with local = D.unlift ctx.local
              ; split = (fun d es -> ctx.split (D.lift d) es )
     }
 
+  let context ctx fd = S.context (conv ctx) fd % D.unlift
+
   let lift_fun ctx f g h b =
     try f @@ h (g (conv ctx))
     with Deadcode -> b
@@ -498,7 +507,7 @@ struct
 end
 
 module NoContext = struct let name = "no context" end
-module IntConf = 
+module IntConf =
 struct
   let n () = max_int
   let names x = Format.asprintf "%d" x
@@ -507,15 +516,15 @@ end
 (** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
     For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
 module ContextGasLifter (S:Spec)
-  : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf)) 
+  : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf))
           and module C = Printable.Option (S.C) (NoContext)
           and module G = S.G
 =
 struct
   include S
 
-  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) = 
-  struct 
+  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) =
+  struct
     include Lattice.Prod (Base1) (Base2)
     let printXml f (x,y) =
       BatPrintf.fprintf f "\n%a<analysis name=\"context gas value\">\n%a\n</analysis>" Base1.printXml x Base2.printXml y
@@ -537,17 +546,15 @@ struct
   let init = S.init
   let finalize = S.finalize
 
+
+  let startcontext () = Some (S.startcontext ())
   let name () = S.name ()^" with context gas"
   let startstate v = S.startstate v, get_int "ana.context.gas_value"
   let exitstate v = S.exitstate v, get_int "ana.context.gas_value"
   let morphstate v (d,i) = S.morphstate v d, i
 
-  let context fd (d,i) = 
-    (* only keep context if the context gas is greater zero *)
-    if i <= 0 then None else Some (S.context fd d)
-
   let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
-    if (cg_val ctx <= 0) 
+    if (cg_val ctx <= 0)
     then {ctx with local = fst ctx.local
                  ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
                  ; context = (fun () -> ctx_failwith "no context (contextGas = 0)")}
@@ -555,14 +562,18 @@ struct
                  ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
                  ; context = (fun () -> Option.get (ctx.context ()))}
 
+  let context ctx fd (d,i) =
+    (* only keep context if the context gas is greater zero *)
+    if i <= 0 then None else Some (S.context (conv ctx) fd d)
+
   let enter ctx r f args =
     (* callee gas = caller gas - 1 *)
     let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in
-    liftmap_tup (S.enter (conv ctx) r f args) 
+    liftmap_tup (S.enter (conv ctx) r f args)
 
-  let threadenter ctx ~multiple lval f args = 
+  let threadenter ctx ~multiple lval f args =
     let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in
-    liftmap (S.threadenter (conv ctx) ~multiple lval f args) 
+    liftmap (S.threadenter (conv ctx) ~multiple lval f args)
 
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
   let query ctx q                                 = S.query (conv ctx) q
@@ -576,7 +587,7 @@ struct
   let special ctx r f args                        = S.special (conv ctx) r f args, cg_val ctx
   let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
   let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
-  let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx) 
+  let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx)
   let threadspawn ctx ~multiple lval f args fctx  = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
   let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx
 end
@@ -648,7 +659,7 @@ struct
           spawns := (lval, f, args, d, multiple) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
           | fd ->
-            let c = S.context fd d in
+            let c = S.context ctx fd d in
             sidel (FunctionEntry fd, c) d;
             ignore (getl (Function fd, c))
           | exception Not_found ->
@@ -789,7 +800,7 @@ struct
       r
     in
     let paths = S.enter ctx lv f args in
-    let paths = List.map (fun (c,v) -> (c, S.context f v, v)) paths in
+    let paths = List.map (fun (c,v) -> (c, S.context ctx f v, v)) paths in
     List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) paths;
     let paths = List.map (fun (c,fc,v) -> (c, fc, if S.D.is_bot v then v else getl (Function f, fc))) paths in
     (* Don't filter bot paths, otherwise LongjmpLifter is not called. *)
@@ -1146,16 +1157,11 @@ struct
   let init = Spec.init
   let finalize = Spec.finalize
 
+  let startcontext () = Spec.startcontext ()
   let exitstate  v = D.singleton (Spec.exitstate  v)
   let startstate v = D.singleton (Spec.startstate v)
   let morphstate v d = D.map (Spec.morphstate v) d
 
-  let context fd l =
-    if D.cardinal l <> 1 then
-      failwith "PathSensitive2.context must be called with a singleton set."
-    else
-      Spec.context fd @@ D.choose l
-
   let conv ctx x =
     let rec ctx' = { ctx with ask   = (fun (type a) (q: a Queries.t) -> Spec.query ctx' q)
                             ; local = x
@@ -1163,6 +1169,14 @@ struct
     in
     ctx'
 
+  let context ctx fd l =
+    if D.cardinal l <> 1 then
+      failwith "PathSensitive2.context must be called with a singleton set."
+    else
+      let x = D.choose l in
+      Spec.context (conv ctx x) fd x
+
+
   let map ctx f g =
     let h x xs =
       try D.add (g (f (conv ctx x))) xs
@@ -1352,6 +1366,7 @@ struct
 
 
   let branch ctx = S.branch (conv ctx)
+  let context ctx = S.context (conv ctx)
 
   let branch ctx exp tv =
     if !AnalysisState.postsolving then (
@@ -1466,6 +1481,7 @@ struct
   let paths_as_set ctx = S.paths_as_set (conv ctx)
   let body ctx = S.body (conv ctx)
   let return ctx = S.return (conv ctx)
+  let context ctx = S.context (conv ctx)
 
   let combine_env ctx lv e f args fc fd f_ask =
     let conv_ctx = conv ctx in
@@ -1746,6 +1762,7 @@ struct
     sideg (V.call callee) (G.create_singleton_caller caller)
 
   let enter ctx  = S.enter (conv ctx)
+  let context ctx = S.context (conv ctx)
   let paths_as_set ctx = S.paths_as_set (conv ctx)
   let body ctx = S.body (conv ctx)
   let return ctx = S.return (conv ctx)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 714a83b236..de849749bc 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -23,7 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
-      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter) 
+      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
@@ -404,8 +404,8 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in enter_with context.")
         ; node    = MyCFG.dummy_node
         ; prev_node = MyCFG.dummy_node
-        ; control_context = (fun () -> ctx_failwith "enter_func has no context.")
-        ; context = (fun () -> ctx_failwith "enter_func has no context.")
+        ; control_context = (fun () -> ctx_failwith "enter_with has no control_context.")
+        ; context = Spec.startcontext
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
@@ -458,14 +458,29 @@ struct
 
     AnalysisState.global_initialization := false;
 
+    let ctx e =
+      { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+      ; emit   = (fun _ -> failwith "Cannot \"emit\" in enter_with context.")
+      ; node    = MyCFG.dummy_node
+      ; prev_node = MyCFG.dummy_node
+      ; control_context = (fun () -> ctx_failwith "enter_with has no control_context.")
+      ; context = Spec.startcontext
+      ; edge    = MyCFG.Skip
+      ; local   = e
+      ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
+      ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+      ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
+      ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
+      }
+    in
     let startvars' =
       if get_bool "exp.forward" then
-        List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context n e)) startvars
+        List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (ctx e) n e)) startvars
       else
-        List.map (fun (n,e) -> (MyCFG.Function n, Spec.context n e)) startvars
+        List.map (fun (n,e) -> (MyCFG.Function n, Spec.context (ctx e) n e)) startvars
     in
 
-    let entrystates = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context n e), e) startvars in
+    let entrystates = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (ctx e) n e), e) startvars in
     let entrystates_global = GHT.to_list gh in
 
     let uncalled_dead = ref 0 in
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 1816de90c7..41bb5d8477 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -126,8 +126,6 @@ struct
   let exitstate  v = (S.exitstate  v, TS.bot ())
   let morphstate v (d, t) = (S.morphstate v d, t)
 
-  let context fd = S.context fd % D.unlift
-
   let conv (ctx: (D.t, G.t, C.t, V.t) ctx): (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
     { ctx with local = D.unlift ctx.local
              ; split = (fun d es -> ctx.split (d, snd ctx.local) es) (* Split keeps local widening tokens. *)
@@ -135,6 +133,9 @@ struct
              ; sideg = (fun v g -> ctx.sideg v (g, !side_tokens)) (* Using side_tokens for side effect. *)
     }
 
+  let context ctx fd = S.context (conv ctx) fd % D.unlift
+  let startcontext () = S.startcontext ()
+
   let lift_fun ctx f g h =
     let new_tokens = ref (snd ctx.local) in (* New tokens not yet used during this transfer function, such that it is deterministic. *)
     let old_add = !add_ref in
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 58b5b31fe4..490a51021a 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -30,7 +30,7 @@ struct
     let names x = "state " ^ string_of_int x
   end
   module D = Lattice.Flat (Printable.Chain (ChainParams))
-  module C = D
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D) (* fully path-sensitive *)
 
   let step d prev_node node =
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 4af9dd898d..667562ef15 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -107,12 +107,6 @@ struct
   let startstate v = (Dom.singleton (Spec.startstate v) (R.bot ()), Sync.bot ())
   let morphstate v (d, _) = (Dom.map_keys (Spec.morphstate v) d, Sync.bot ())
 
-  let context fd (l, _) =
-    if Dom.cardinal l <> 1 then
-      failwith "PathSensitive3.context must be called with a singleton set."
-    else
-      Spec.context fd @@ Dom.choose_key l
-
   let step n c i e = R.singleton ((n, c, i), e)
   let step n c i e sync =
     match Sync.find i sync with
@@ -146,6 +140,15 @@ struct
     in
     ctx'
 
+  let context ctx fd (l, _) =
+    if Dom.cardinal l <> 1 then
+      failwith "PathSensitive3.context must be called with a singleton set."
+    else
+      let x = Dom.choose_key l in
+      Spec.context (conv ctx x) fd @@ x
+
+  let startcontext = Spec.startcontext
+
   let map ctx f g =
     (* we now use Sync for every tf such that threadspawn after tf could look up state before tf *)
     let h x (xs, sync) =