diff --git a/src/analyses/wp_analyses/liveness.ml b/src/analyses/wp_analyses/liveness.ml
new file mode 100644
index 0000000000..fc442d9c29
--- /dev/null
+++ b/src/analyses/wp_analyses/liveness.ml
@@ -0,0 +1,274 @@
+open GoblintCil
+open Analyses
+
+module BackwSpec : BackwAnalyses.BackwSpecSpec = functor (ForwSpec : Analyses.Spec) ->
+struct
+
+  include BackwAnalyses.DefaultBackwSpec (ForwSpec)
+  module C = ForwSpec.C
+
+  (* Adding these module definitions because the "include" of the DefaultBackwSpec is not enough*)
+  module D_forw = ForwSpec.D
+  module G_forw = ForwSpec.G
+  module V_forw = ForwSpec.V
+  module P_forw = ForwSpec.P
+  let name () = "liveness"
+
+  module G = Lattice.Unit
+  module V = EmptyV
+  module P = EmptyP
+
+  module LiveVariableSet =  SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end)
+  module D =  LiveVariableSet (*Set of program variables as domain*)
+
+  let startstate v = D.empty()
+  let exitstate v = D.empty()
+
+  let rec vars_from_lval (l: lval) man_forw : varinfo list  = 
+    let vars_written_to =  
+      match l with
+      | Var v, _ ->  (
+          if (Cil.isFunctionType v.vtype) then [] else [v]  (*I do not want functions in the set of live variables*)
+        )
+      | Mem exp, _ -> (*If a pointer may point to a variable, these variables are live as well...*)
+        let may_point_to = Queries.AD.to_var_may (man_forw.ask (MayPointTo exp)) in
+        if may_point_to = [] then (
+          M.warn ~category:MessageCategory.Unsound "The expression %a may point to an unknown variable. This makes the analysis unsound." d_exp exp; (*UNSOUND: I do not think that this check is enough. Maybe I should just exclude analyzing programs with variables whose address is taken.*)
+          vars_from_expr exp man_forw )
+        else (
+          Logs.debug "(!) The expression %a may point to the variables %s" d_exp exp (String.concat ", " (List.map (fun v -> v.vname) may_point_to));
+          may_point_to @ vars_from_expr exp man_forw)
+    in
+
+    let vars_in_offset = 
+      match l with
+      | Var _, off -> vars_from_offset off man_forw
+      | Mem _, off -> vars_from_offset off man_forw
+    in
+
+    (vars_written_to @ vars_in_offset)
+
+  and vars_from_offset (off: offset) man_forw : varinfo list =
+    match off with
+    | NoOffset -> []
+    | Field (_, off) -> vars_from_offset off man_forw (* what to do with fieldinfo?*)
+    | Index (e, off) -> 
+      let vars_in_e = vars_from_expr e man_forw  in
+      let vars_in_off = vars_from_offset off man_forw in
+      (match vars_in_off with
+       | [] -> []
+       | vars_in_off ->  (vars_in_e @ vars_in_off))
+
+  and vars_from_expr (e: exp) man_forw : varinfo list =
+    let rec aux acc e =
+      match e with
+      | Lval v -> vars_from_lval v man_forw @ acc 
+      | BinOp (_, e1, e2, _)  ->
+        let acc1 = aux acc e1 in
+        aux acc1 e2
+      | UnOp (_, e1, _)       -> aux acc e1
+      | SizeOfE e1            -> aux acc e1
+      | AlignOfE e1           -> aux acc e1
+      | Question (e1, e2, e3, _) -> 
+        let acc1 = aux acc e1 in
+        let acc2 = aux acc1 e2 in
+        aux acc2 e3
+      | CastE (_, e1)         ->   aux acc e1  (*This appears to make problems when building for jobs*)
+      | AddrOf (l1)          ->   (match vars_from_lval l1 man_forw with
+          | [] -> acc
+          |  v -> (v @ acc)
+        )
+      | _ ->  acc 
+
+    in
+    aux [] e
+
+  let rec assign man man_forw (lval:lval) (rval:exp) =
+    match lval with
+    | Var v, offset -> 
+      if (D.mem v man.local) then ( (* Global variables are considered live when writing to them -> No, not anymore. This of course does not wark with concurrent programs, but I am already excluding those. *)
+        let rval_vars = D.of_list (vars_from_expr rval man_forw)in
+        let rval_vars = D.filter (fun v -> not (Cil.isFunctionType v.vtype)) rval_vars in (*remove variables that are just function names*)
+
+        let offset_vars = D.of_list (vars_from_offset offset man_forw) in
+        let base_live =
+          match offset with
+          | NoOffset -> D.diff man.local (D.singleton v)
+          | _ -> man.local
+        in
+
+        D.union rval_vars (D.union offset_vars base_live)
+      ) else (
+        (* let loc = M.Location.Node man.node in *)
+        (* M.warn ~loc:loc ~category:MessageCategory.Program "Unnecessary assignment to variable '%s', as it is not live at this program point." v.vname; *)
+        man.local
+      )
+    | Mem exp, off -> 
+      let ad = man_forw.ask (MayPointTo exp) in
+      let lval_vars = D.of_list (vars_from_expr exp man_forw) in
+      let rval_vars = D.of_list (vars_from_expr rval man_forw) in
+      let rval_vars = D.filter (fun v -> not (Cil.isFunctionType v.vtype)) rval_vars in (*remove variables that are just function names*)
+
+      let strong_target =
+        match off, Queries.AD.to_mval ad with
+        | NoOffset, [(v, `NoOffset)] when Queries.AD.is_element (Queries.AD.Addr.of_mval (v, `NoOffset)) ad -> Some v
+        | _ -> None
+      in
+
+
+      let log_this ()= 
+        Logs.debug "(!) Assignment to memory location %a with may-point-to set [?]" d_exp exp;
+        Logs.debug "Variables in the lval: %s" (String.concat ", " (List.map (fun v -> v.vname) (D.elements lval_vars)));
+        Logs.debug "Variables in the rval: %s" (String.concat ", " (List.map (fun v -> v.vname) (D.elements rval_vars)));
+        match strong_target with
+        | Some v -> Logs.debug "Strong target variable: %s" v.vname
+        | None -> Logs.debug "No strong target variable identified"
+      in
+      log_this (); 
+
+      match strong_target with
+      | Some v ->
+        D.union (assign man man_forw (Var v, NoOffset) rval) lval_vars
+      | None -> D.union rval_vars (D.union lval_vars man.local)
+
+  let branch man man_forw (exp:exp) (tv:bool) =  
+    (* This just randomly asks whether all loops terimante to use getg_forw utilized in man.global *)
+    (* let () =
+       match man_forw.ask(Queries.MustTermAllLoops) with
+       | true -> Logs.debug "MustTermAllLoops is TRUE"
+       | _ -> Logs.debug "MustTermAllLoops is NOT TRUE"
+       in *)
+
+    let branch_irrelevant : bool = (
+      match Queries.eval_bool (Analyses.ask_of_man man_forw) exp with
+      | `Lifted b -> tv <> b
+      | `Bot -> false
+      | `Top -> false
+    )
+    in
+    if branch_irrelevant then (D.of_list (vars_from_expr exp man_forw))
+    else D.join man.local (D.of_list (vars_from_expr exp man_forw))
+
+  let body man man_forw (f:fundec) =
+    man.local
+
+  let enter man man_forw (lval: lval option) (f:fundec) (args:exp list) =
+
+    let global_vars_in_d = D.filter (fun v -> v.vglob) man.local in
+
+    let callee_d = 
+      match lval with
+      | Some (Var v, _) -> 
+        if (D.mem v man.local) then ( 
+          (D.singleton v) 
+        ) else (
+          D.empty()
+        )
+      | Some (Mem exp, _) -> D.of_list (vars_from_expr exp man_forw)
+      | None -> D.empty()
+    in
+
+    [man.local, (D.union callee_d global_vars_in_d)]
+
+
+  let combine_env man man_forw (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+
+    (* map relevant sformals in man.local to the corresponding variables contained in the argument*)
+    let arg_formal_pairs = List.combine args f.sformals in
+    let relevant_arg_vars = 
+      List.fold_left (fun acc (arg_exp, formal_var) ->
+          if D.mem formal_var au then
+            D.join acc (D.of_list(vars_from_expr arg_exp man_forw))
+          else
+            acc
+        ) (D.empty()) arg_formal_pairs
+    in
+
+    (*join relevant*)
+    D.join man.local relevant_arg_vars 
+
+  let combine_assign man man_forw (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =  
+    match lval with 
+    | None -> man.local 
+    | Some l -> assign man man_forw l fexp
+
+  (** A transfer function which handles the return statement, i.e.,
+      "return exp" or "return" in the passed function (fundec) *)
+  let return man man_forw (exp: exp option) (f:fundec) : D.t =
+
+    let return_val_is_important = (not (D.is_bot man.local)) || (String.equal f.svar.vname "main") in
+
+    match exp with
+    | None -> man.local
+    | Some e -> if return_val_is_important
+      then D.of_list (vars_from_expr e man_forw) |> D.union man.local
+      else man.local
+
+
+  let special man man_forw (lval: lval option) (f:varinfo) (arglist:exp list) =
+    (* log when called  *)
+    Logs.debug "(!) Called special for function %s with arguments %s" f.vname (String.concat ", " (List.map (fun e -> Pretty.sprint ~width:80 (d_exp () e)) arglist));
+
+    let desc = LibraryFunctions.find f in 
+    match desc.special arglist with
+    (* Could have some special handeling of library functions here *)
+    | _ ->
+      let argvars = List.fold_left (fun acc arg -> D.union acc (D.of_list (vars_from_expr arg man_forw))) (D.empty()) arglist in 
+      match lval with
+      | None -> D.union man.local argvars
+      | Some (Var v, _) -> D.union (D.diff man.local (D.singleton(v))) argvars
+      | Some (Mem exp, _) -> D.union (D.union argvars (D.of_list (vars_from_expr exp man_forw))) man.local
+
+  let threadenter man man_forw ~multiple lval f args = [man.local]
+  let threadspawn man man_forw ~multiple lval f args fman = man.local
+
+  let query man (type a) man_forw (q: a Queries.t): a Queries.result =
+
+    (* Die recursion ist nicht sauber durchdacht *)
+    let rec is_dead_assign man man_forw (lval:lval) (rval:exp) (is_dead:bool) : (D.t * bool) =
+
+      match lval with
+      | Var v, _ ->
+        Logs.debug "D.mem v man.local is %b" (D.mem v man.local);
+        Logs.debug "v.glob is %b" v.vglob;
+        if (D.mem v man.local) then ( (*I used to care whether a variable is global, I no longer do.*)
+          let rval_vars = D.of_list (vars_from_expr rval man_forw)
+          in
+          (D.union rval_vars (D.diff man.local (D.singleton v)), false)
+        )else (
+          Logs.debug "Variable '%s' is not live at this program point." v.vname;
+          (man.local, true)
+        )
+      | Mem exp, off -> (
+          Logs.debug "lval is expression";
+          let ad = man_forw.ask (MayPointTo exp) in
+          let lval_vars = D.of_list (vars_from_expr exp man_forw) in
+          let rval_vars = D.of_list (vars_from_expr rval man_forw) in
+
+          let strong_target =
+            match off, Queries.AD.to_mval ad with
+            | NoOffset, [(v, `NoOffset)] when Queries.AD.is_element (Queries.AD.Addr.of_mval (v, `NoOffset)) ad -> Some v
+            | _ -> None
+          in
+
+          match strong_target with
+          | Some v ->
+            let rec_assign_result, is_dead = 
+              match (is_dead_assign man man_forw (Var v, NoOffset) rval is_dead) with 
+              | (res, new_is_dead) -> res, new_is_dead
+            in 
+            (D.union rec_assign_result lval_vars, is_dead)
+          | None ->  ((D.union rval_vars (D.union lval_vars man.local)), is_dead)
+        )
+    in 
+
+    let open Queries in
+
+    match q with
+    | IsDeadVar v -> not (D.mem v man.local)
+    | MayBeDeadAssignment lval -> (
+        Logs.debug "Checking if assignment to lval %a may be dead at node %a with local state %a" d_lval lval Node.pretty_trace man.node D.pretty man.local;
+        match is_dead_assign man man_forw lval (Const (CInt (Z.zero, IInt, None))) false with
+        | (_, is_dead) -> Logs.debug "isdead is %b" is_dead ; is_dead )
+    | _ -> Result.top q
+end
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 02e634d9e7..1697ecc9c9 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1298,6 +1298,13 @@
             }
           },
           "additionalProperties": false
+        },
+         "wp_run": {
+          "title": "ana.wp_run",
+          "description":
+            "Do a wp analysis, in this case the liveness analysis.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 31e93dd0b2..ad36fad1ff 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -146,6 +146,8 @@ type _ t =
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
+  | IsDeadVar: varinfo -> MayBool.t t (* Whether a variable is dead at a program point, i.e., not read afterwards. *)
+  | MayBeDeadAssignment: lval -> MayBool.t t (* Whether an assignment is dead, i.e., the assigned variable is not read afterwards. *) 
 
 type 'a result = 'a
 
@@ -221,6 +223,8 @@ struct
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
+    | IsDeadVar _ -> (module MayBool)
+    | MayBeDeadAssignment _ -> (module MayBool)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -295,6 +299,8 @@ struct
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
+    | IsDeadVar _ -> MayBool.top ()
+    | MayBeDeadAssignment _ -> MayBool.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -366,6 +372,8 @@ struct
     | Any (MustProtectingLocks _) -> 61
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
+    | Any (IsDeadVar _) -> 64
+    | Any (MayBeDeadAssignment _) -> 65
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -540,6 +548,8 @@ struct
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
+    | Any (IsDeadVar v) -> Pretty.dprintf "IsDeadVar %a" CilType.Varinfo.pretty v
+    | Any (MayBeDeadAssignment s) -> Pretty.dprintf "MayBeDeadAssignment %a" CilType.Lval.pretty s
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index f655d89316..22db9d4031 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -429,9 +429,9 @@ module type SpecSys =
 sig
   module Spec: Spec
   module EQSys: Goblint_constraint.ConstrSys.DemandGlobConstrSys with module LVar = VarF (Spec.C)
-                               and module GVar = GVarF (Spec.V)
-                               and module D = Spec.D
-                               and module G = GVarG (Spec.G) (Spec.C)
+                                                                  and module GVar = GVarF (Spec.V)
+                                                                  and module D = Spec.D
+                                                                  and module G = GVarG (Spec.G) (Spec.C)
   module LHT: BatHashtbl.S with type key = EQSys.LVar.t
   module GHT: BatHashtbl.S with type key = EQSys.GVar.t
 end
@@ -443,4 +443,4 @@ sig
 
   val gh: EQSys.G.t GHT.t
   val lh: SpecSys.Spec.D.t LHT.t (* explicit SpecSys to avoid spurious module cycle *)
-end
+end
\ No newline at end of file
diff --git a/src/framework/backwAnalyses.ml b/src/framework/backwAnalyses.ml
new file mode 100644
index 0000000000..bfa83a4cbb
--- /dev/null
+++ b/src/framework/backwAnalyses.ml
@@ -0,0 +1,167 @@
+open GoblintCil
+open Analyses
+
+module M  = Messages
+
+module type BackwSpec = 
+sig
+  module D : Lattice.S
+  module G : Lattice.S
+  module C : Printable.S
+  module V: SpecSysVar (** Global constraint variables. *)
+  module P: DisjointDomain.Representative with type elt := D.t (** Path-representative. *)
+
+  module D_forw: Lattice.S
+  module G_forw: Lattice.S 
+  module V_forw: SpecSysVar (** Global constraint variables. *)
+  module P_forw: DisjointDomain.Representative with type elt := D_forw.t (* Path-representative. *)
+  val name : unit -> string
+
+  (** Auxiliary data (outside of solution domains) that needs to be marshaled and unmarshaled.
+      This includes:
+      * hashtables,
+      * varinfos (create_var),
+      * RichVarinfos. *)
+  type marshal
+
+  (** Initialize using unmarshaled auxiliary data (if present). *)
+  val init : marshal option -> unit
+
+  (** Finalize and return auxiliary data to be marshaled. *)
+  val finalize : unit -> marshal
+  (* val finalize : G.t -> unit *)
+
+  val startstate : varinfo -> D.t
+  val morphstate : varinfo -> D.t -> D.t
+  val exitstate  : varinfo -> D.t
+
+  val context: (D_forw.t, G_forw.t, C.t, V_forw.t) man -> fundec -> D_forw.t -> C.t 
+  val startcontext: unit -> C.t
+
+  val sync  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return] -> D.t
+  val query : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> 'a Queries.t -> 'a Queries.result
+
+  (** A transfer function which handles the assignment of a rval to a lval, i.e.,
+      it handles program points of the form "lval = rval;" *)
+  val assign: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval -> exp -> D.t
+
+  (** A transfer function used for declaring local variables.
+      By default only for variable-length arrays (VLAs). *)
+  val vdecl : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> varinfo -> D.t
+
+  (** A transfer function which handles conditional branching yielding the
+      truth value passed as a boolean argument *)
+  val branch: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> exp -> bool -> D.t
+
+  (** A transfer function which handles going from the start node of a function (fundec) into
+      its function body. Meant to handle, e.g., initialization of local variables *)
+  val body  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> fundec -> D.t
+
+  (** A transfer function which handles the return statement, i.e.,
+      "return exp" or "return" in the passed function (fundec) *)
+  val return: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> exp option  -> fundec -> D.t
+
+  (** A transfer function meant to handle inline assembler program points *)
+  val asm   : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t
+
+  (** A transfer function which works as the identity function, i.e., it skips and does nothing.
+      Used for empty loops. *)
+  val skip  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t
+
+  (** A transfer function which, for a call to a {e special} function f "lval = f(args)" or "f(args)",
+      computes the caller state after the function call *)
+  val special : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> varinfo -> exp list -> D.t
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      [enter] returns a caller state, and the initial state of the callee.
+      In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
+      will compute the caller state after the function call, given the return state of the callee *)
+  val enter   : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> fundec -> exp list -> (D.t * D.t) list
+
+  (* Combine is split into two steps: *)
+
+  (** Combine environment (global variables, mutexes, etc)
+      between local state (first component from enter) and function return.
+
+      This shouldn't yet assign to the lval. *)
+  val combine_env : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+
+  (** Combine return value assignment
+      to local state (result from combine_env) and function return.
+
+      This should only assign to the lval. *)
+  val combine_assign : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+
+  (* Paths as sets: I know this is ugly! *)
+  val paths_as_set : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t list
+
+  (** Returns initial state for created thread. *)
+  val threadenter : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
+
+  (** Updates the local state of the creator thread using initial state of created thread. *)
+  val threadspawn : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> multiple:bool -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) man -> D.t
+
+  val event : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> Events.t -> (D.t, G.t, C.t, V.t) man -> D.t
+end
+
+module type BackwSpecSpec = functor (ForwSpec : Analyses.Spec) -> sig
+  include BackwSpec 
+    with module C = ForwSpec.C
+    with module D_forw = ForwSpec.D
+    with module G_forw = ForwSpec.G
+    with module V_forw = ForwSpec.V
+    with module P_forw = ForwSpec.P  
+end
+
+module DefaultBackwSpec (ForwSpec : Analyses.Spec) =
+struct
+  module G = Lattice.Unit
+  module C = ForwSpec.C
+  module V = EmptyV
+  module P = EmptyP
+
+  module D_forw: Lattice.S = ForwSpec.D
+  module G_forw: Lattice.S = ForwSpec.G
+  module V_forw: SpecSysVar = ForwSpec.V (** Global constraint variables. *)
+  module P_forw: DisjointDomain.Representative with type elt := ForwSpec.D.t = ForwSpec.P (*Path-representative.*)
+
+  type marshal = unit
+  let init _ = ()
+
+  (* This means it does not matter which Spec's context function we use in control and BidirFromSpec. 
+   * For understandability in other parts of the code the context-function of the forward spec should be used explicitely*)
+
+  let context = ForwSpec.context 
+  let startcontext _ =  ForwSpec.startcontext ()
+  let finalize () = ()
+  (* no inits nor finalize -- only analyses like Mutex, Base, ... need
+     these to do postprocessing or other imperative hacks. *)
+
+  let vdecl man _ _ = man.local
+
+  let asm x _ =
+    M.msg_final Info ~category:Unsound "ASM ignored";
+    M.info ~category:Unsound "ASM statement ignored.";
+    x.local (* Just ignore. *)
+
+  let skip x _ = x.local (* Just ignore. *)
+
+  let query _ _ (type a) (q: a Queries.t) = Queries.Result.top q
+  (* Don't know anything --- most will want to redefine this. *)
+
+  let event man _ _ _ = man.local
+
+  let morphstate v d = d
+  (* Only for those who track thread IDs. *)
+
+  let sync man _ _ = man.local
+  (* Most domains do not have a global part. *)
+
+  (* let context man _ fd x = x *)
+  (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
+
+  let paths_as_set man _ = [man.local]
+
+  (* module A = UnitA *)
+  (* let access _ _ = () *)
+end
diff --git a/src/framework/bidirConstrains.ml b/src/framework/bidirConstrains.ml
new file mode 100644
index 0000000000..3c3cf17938
--- /dev/null
+++ b/src/framework/bidirConstrains.ml
@@ -0,0 +1,697 @@
+open Batteries
+open GoblintCil
+open MyCFG
+open Analyses
+open BackwAnalyses
+open Goblint_constraint.ConstrSys
+open GobConfig
+
+module type Increment =
+sig
+  val increment: increment_data option
+end
+
+module GVarF2 (V_forw: SpecSysVar) (V_backw : SpecSysVar) : 
+sig
+  module GV_forw : module type of GVarF (V_forw)
+  module GV_backw : module type of GVarF (V_backw)  
+  include VarType with type t = [ `Forw of GV_forw.t | `Backw of GV_backw.t ]
+  include SpecSysVar with type t := t
+  val spec : [ `Forw of V_forw.t | `Backw of V_backw.t ] -> [ `Forw of [`Left of V_forw.t] | `Backw of [`Left of V_backw.t] ]
+  val contexts : [ `Forw of V_forw.t | `Backw of V_backw.t ] -> [`Forw of [`Right of V_forw.t] | `Backw of  [`Right of V_backw.t]]
+end
+=
+struct
+  module GV_forw = GVarF (V_forw)
+  module GV_backw = GVarF (V_backw)  
+  type t = [ `Forw of GV_forw.t | `Backw of GV_backw.t ] [@@deriving eq, ord, hash]
+  let name () = "BidirFromSpec"
+
+  let tag _ = failwith "Std: no tag"
+
+  let relift = function
+    | `Forw x -> `Forw (GV_forw.relift x)
+    | `Backw x -> `Backw (GV_backw.relift x)
+
+  let pretty_trace () = function
+    | `Forw a -> GoblintCil.Pretty.dprintf "G_forw:%a" GV_forw.pretty_trace a
+    | `Backw a -> GoblintCil.Pretty.dprintf "G_backw:%a" GV_backw.pretty_trace a
+
+  let printXml f = function
+    | `Forw a -> GV_forw.printXml f a
+    | `Backw a -> GV_backw.printXml f a
+
+  let node = function
+    | `Forw a -> GV_forw.node a
+    | `Backw a -> GV_backw.node a
+
+  let is_write_only = function
+    | `Forw a -> GV_forw.is_write_only a
+    | `Backw a -> GV_backw.is_write_only a
+
+  let show = function
+    | `Forw a -> GV_forw.show a
+    | `Backw a -> GV_backw.show a
+
+  let pretty () = function
+    | `Forw a -> GV_forw.pretty () a
+    | `Backw a -> GV_backw.pretty () a
+  let to_yojson = function
+    | `Forw a -> GV_forw.to_yojson a
+    | `Backw a -> GV_backw.to_yojson a
+
+  let spec : [ `Forw of V_forw.t | `Backw of V_backw.t ] -> [ `Forw of [`Left of V_forw.t] | `Backw of [`Left of V_backw.t] ] = function
+    | `Forw v -> `Forw (GV_forw.spec v )
+    | `Backw v ->  `Backw (GV_backw.spec v )
+
+  let contexts : [ `Forw of V_forw.t | `Backw of V_backw.t ] -> [`Forw of [`Right of V_forw.t] | `Backw of  [`Right of V_backw.t]] = function
+    | `Forw v -> `Forw (GV_forw.contexts v)
+    | `Backw v ->  `Backw (GV_backw.contexts v)
+
+  let var_id = show
+
+  let arbitrary () =
+    failwith "no arbitrary"
+end 
+
+module BidirFromSpec (S_forw:Spec) (S_backw:BackwSpec with type D_forw.t = S_forw.D.t and type G_forw.t = S_forw.G.t and type C.t = S_forw.C.t and type V_forw.t = S_forw.V.t) (Cfg:CfgBidir) (I:Increment)
+  : sig
+    module LVar : Goblint_constraint.ConstrSys.VarType with type t = [ `L_forw of VarF(S_forw.C).t | `L_backw of VarF(S_forw.C).t ]
+    module GVar : (module type of GVarF2(S_forw.V)(S_backw.V))
+    include DemandGlobConstrSys with module LVar := LVar
+                                 and module GVar := GVar
+                                 and module D = Lattice.Lift2(S_forw.D)(S_backw.D)
+                                 and module G = GVarG (Lattice.Lift2(S_forw.G)(S_backw.G)) (S_forw.C)
+  end 
+= 
+struct
+  module LV = VarF (S_forw.C)
+  module LVar =
+  struct
+    type t = [ `L_forw of LV.t | `L_backw of LV.t ] [@@deriving eq, ord, hash]
+
+    let relift = function
+      | `L_forw x -> `L_forw (LV.relift x)
+      | `L_backw x -> `L_backw (LV.relift x)
+
+    let pretty_trace () = function
+      | `L_forw a -> GoblintCil.Pretty.dprintf "L_forw:%a" LV.pretty_trace a
+      | `L_backw a -> GoblintCil.Pretty.dprintf "L_backw:%a" LV.pretty_trace a
+
+    let printXml f = function
+      | `L_forw a -> LV.printXml f a
+      | `L_backw a -> LV.printXml f a
+
+    let var_id = function
+      | `L_forw a -> LV.var_id a
+      | `L_backw a -> LV.var_id a
+
+    let node = function
+      | `L_forw a -> LV.node a
+      | `L_backw a -> LV.node a
+
+    let is_write_only = function
+      | `L_forw a -> LV.is_write_only a
+      | `L_backw a -> LV.is_write_only a
+  end
+
+  module D = Lattice.Lift2(S_forw.D)(S_backw.D)
+  module GVar = GVarF2(S_forw.V)(S_backw.V)
+
+  module G_forw = GVarG (S_forw.G) (S_forw.C)
+  module G_backw = GVarG (S_backw.G) (S_forw.C)
+  module G  = GVarG (Lattice.Lift2(S_forw.G)(S_backw.G)) (S_forw.C)
+
+  module Forward = Constraints.FromSpec(S_forw)(Cfg)(I)
+
+  (* Lowering functions for local values.*)
+  let to_forw_d (d: D.t) : S_forw.D.t =
+    match d with
+    | `Lifted1 d -> d
+    | `Bot -> S_forw.D.bot ()
+    | `Top -> S_forw.D.top ()
+    | `Lifted2 _ -> failwith "bidirConstrains: forward local has backward value"
+
+  let to_backw_d (d: D.t) : S_backw.D.t =
+    match d with
+    | `Lifted2 d -> d
+    | `Bot -> S_backw.D.bot ()
+    | `Top -> S_backw.D.top ()
+    | `Lifted1 _ -> failwith "bidirConstrains: backward local has forward value"
+
+  (* Lowering and lifting functions to deal with different global values. This is convoluted -- but tbh, it is not that much worse than the G module in the existing forwards analysis. 
+   * The conversion between the CSets is quite disgusting though. *) 
+
+  let to_forw_g (g: G.t) : Forward.G.t =
+    match g with
+    | `Lifted1 (`Lifted1 g) -> `Lifted1 g
+    | `Lifted1 `Bot -> `Bot
+    | `Lifted1 `Top -> `Top
+    | `Lifted1 (`Lifted2 _) -> failwith "bidirConstrains: forward global got backward value"
+    | `Lifted2 c -> `Lifted2 (G_forw.CSet.of_list (G.CSet.elements c))
+    | `Bot -> `Bot
+    | `Top -> `Top
+
+  let to_backw_g (g: G.t) : G_backw.t =
+    match g with
+    | `Lifted1 (`Lifted2 g) -> `Lifted1 g
+    | `Lifted1 `Bot -> `Bot
+    | `Lifted1 `Top -> `Top
+    | `Lifted1 (`Lifted1 _) -> failwith "bidirConstrains: backward global got forward value"
+    | `Lifted2 c -> `Lifted2 (G_backw.CSet.of_list (G.CSet.elements c))
+    | `Bot -> `Bot
+    | `Top -> `Top
+
+  let of_forw_g (g: Forward.G.t) : G.t =
+    match g with
+    | `Lifted1 g -> `Lifted1 (`Lifted1 g)
+    | `Lifted2 c -> `Lifted2 (G.CSet.of_list (G_forw.CSet.elements c))
+    | `Bot -> `Bot
+    | `Top -> `Top
+
+  let of_backw_g (g: G_backw.t) : G.t =
+    match g with
+    | `Lifted1 g -> `Lifted1 (`Lifted2 g)
+    | `Lifted2 c -> `Lifted2 (G.CSet.of_list (G_backw.CSet.elements c))
+    | `Bot -> `Bot
+    | `Top -> `Top
+
+
+  (* actually relevant (transfer) functions *)
+  let sync_backw man man_forw =
+    match man.prev_node, Cfg.next man.prev_node with
+    | _, _ :: _ :: _ -> (* Join in CFG. *)
+      S_backw.sync man man_forw `Join
+    (* | FunctionEntry f, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+       S_backw.sync man man_forw (`JoinCall f) *)
+    | Function f, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+      S_backw.sync man man_forw (`JoinCall f)
+    | _, _ -> S_backw.sync man man_forw `Normal
+
+  let side_context_backw sideg f c =
+    if !AnalysisState.postsolving then 
+      sideg (GVar.GV_backw.contexts f) (G_backw.create_contexts (G_backw.CSet.singleton c))
+
+
+  let create_basic_man_forw var edge prev_node pval getl getl_forw sidel demandl getg getg_forw sideg : (S_forw.D.t, S_forw.G.t, S_forw.C.t, S_forw.V.t) man =
+    (* let r = ref [] in *)
+    let node = fst var in
+    let context : (unit -> S_forw.C.t) = snd var |> Obj.obj in
+
+    let rec man_forw = 
+      { ask     = (fun (type a) (q: a Queries.t) -> S_forw.query man_forw q)
+      ; emit    = (fun _ -> failwith "emit outside MCP")
+      ; node    = fst var
+      ; prev_node = MyCFG.dummy_node (*I do not have *)
+      ; control_context = (fun () -> failwith "control context not implemented (yet) for forward manager.")
+      ; context = context
+      ; edge    = edge
+      ; local   =  getl_forw (node, context())
+      ; global  = (fun g -> G_forw.spec (getg_forw (GVar.GV_forw.spec g)))
+      ; spawn   = (fun ?multiple _ _ _ -> failwith "spawn should not be called from forward manager")
+      ; split   = (fun _ _ -> failwith "split? what does this do?")
+      ; sideg   = (fun _ _ -> failwith "sideg should not be called from forward manager")
+      }
+    in 
+    man_forw
+
+  let common_man_backw (var:node*Obj.t) edge prev_node pval getl getl_forw (sidel : node * S_forw.C.t -> S_backw.D.t -> unit) demandl getg getg_forw sideg : (S_backw.D.t, S_backw.G.t, S_backw.C.t, S_backw.V.t) man * S_backw.D.t list ref * (lval option * varinfo * exp list * S_backw.D.t * bool) list ref =
+    let r = ref [] in
+    let spawns = ref [] in
+
+    let man_forw = create_basic_man_forw var edge prev_node pval getl getl_forw sidel demandl getg getg_forw sideg in      
+
+    (* Logs.debug "Created forward manager for node %a, now creating backward manager" Node.pretty (fst var); *)
+    (* now watch this ... *)
+    let rec man =
+      { ask     = (fun (type a) (q: a Queries.t) -> S_backw.query man man_forw q)
+      ; emit    = (fun _ -> failwith "emit outside MCP")
+      ; node    = fst var
+      ; prev_node = prev_node
+      ; control_context = snd var |> Obj.obj
+      ; context = snd var |> Obj.obj
+      ; edge    = edge
+      ; local   = pval
+      ; global  = (fun g -> G_backw.spec (getg (GVar.GV_backw.spec g)))
+      ; spawn   = spawn
+      ; split   = (fun (d:S_backw.D.t) es -> assert (List.is_empty es); r := d::!r)
+      ; sideg   = (fun g d -> sideg (GVar.GV_backw.spec g) (G_backw.create_spec d))
+      }
+    and spawn ?(multiple=false) lval f args =
+      (* TODO: adjust man node/edge? *)
+      (* TODO: don't repeat for all paths that spawn same *)
+
+      (* TODO: This needs to be changed for backwards!! Context is created using S_backw.context*)
+      let ds = S_backw.threadenter ~multiple man man_forw lval f args in
+      List.iter (fun (d : S_backw.D.t) ->
+          spawns := (lval, f, args, d, multiple) :: !spawns;
+          match Cilfacade.find_varinfo_fundec f with
+          | fd ->
+            let c = S_forw.context man_forw fd (man_forw.local) in
+            (* sidel (FunctionEntry fd, c) d;
+               demandl (Function fd, c) *)
+            sidel (Function fd, c) d;
+            demandl (FunctionEntry fd, c)
+          | exception Not_found ->
+            (* unknown function *)
+            M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
+            (* actual implementation (e.g. invalidation) is done by threadenter *)
+            (* must still sync for side effects, e.g., old sync-based none privatization soundness in 02-base/51-spawn-special *)
+            let rec sync_man =
+              { man with
+                ask = (fun (type a) (q: a Queries.t) -> (S_backw.query sync_man man_forw q));
+                local = d;
+                (* prev_node = Function dummyFunDec; *)
+                prev_node = FunctionEntry dummyFunDec;
+              }
+            in
+            (* TODO: more accurate man? *)
+            ignore (sync_backw sync_man man_forw)
+        ) ds
+    in
+    (* ... nice, right! *)
+    let pval = sync_backw man man_forw in
+    { man with local = pval }, r, spawns
+
+  let rec bigsqcup_backw = function
+    | []    -> S_backw.D.bot ()
+    | [x]   -> x
+    | x::xs -> S_backw.D.join x (bigsqcup_backw xs)
+
+  let thread_spawns_backws man man_forw d spawns =
+    if List.is_empty spawns then
+      d
+    else
+      let rec man' =
+        { man with
+          ask = (fun (type a) (q: a Queries.t) -> S_backw.query man' man_forw q)
+        ; local = d
+        }
+      in
+      (* TODO: don't forget path dependencies *)
+      let one_spawn (lval, f, args, fd, multiple) =
+        let rec fman =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S_backw.query fman man_forw q)
+          ; local = fd
+          }
+        in
+        S_backw.threadspawn man' man_forw ~multiple lval f args fman
+      in
+      bigsqcup_backw (List.map one_spawn spawns)
+
+  let common_join_backw man man_forw d splits spawns =
+    thread_spawns_backws man man_forw (bigsqcup_backw (d :: splits)) spawns
+
+  let common_joins_backw man man_forw ds splits spawns = common_join_backw man man_forw (bigsqcup_backw ds) splits spawns
+
+  let tf_assign_backw var edge prev_node lv e getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.assign man man_forw lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  let tf_vdecl_backw var edge prev_node v getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.vdecl man man_forw v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  let normal_return_backw r fd man man_forw sideg =
+    let spawning_return = S_backw.return man man_forw r fd in
+    let nval = S_backw.sync { man with local = spawning_return } man_forw `Return in
+    nval
+
+  let toplevel_kernel_return_backw r fd man man_forw sideg =
+    let st = if fd.svar.vname = MyCFG.dummy_func.svar.vname then man.local else S_backw.return man man_forw r fd in
+    let spawning_return = S_backw.return {man with local = st} man_forw None MyCFG.dummy_func in
+    let nval = S_backw.sync { man with local = spawning_return } man_forw `Return in
+    nval
+
+  let tf_ret_backw var edge prev_node ret fd getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+      if (CilType.Fundec.equal fd MyCFG.dummy_func ||
+          List.mem fd.svar.vname (get_string_list "mainfun")) &&
+         get_bool "kernel"
+      then toplevel_kernel_return_backw ret fd man man_forw sideg
+      else normal_return_backw ret fd man man_forw sideg
+    in
+    common_join_backw man man_forw d !r !spawns
+
+  let tf_entry_backw var edge prev_node fd getl getl_forw sidel demandl getg getg_forw sideg d =
+    (* Side effect function context here instead of at sidel to FunctionEntry,
+       because otherwise context for main functions (entrystates) will be missing or pruned during postsolving. *)
+    let c: unit -> S_forw.C.t = snd var |> Obj.obj in
+    side_context_backw sideg fd (c ());
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.body man man_forw fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  let tf_test_backw var edge prev_node e tv getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.branch man man_forw e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  (*TODO: THIS HAS TO BE BACKWARDS*) (*forward context not implemented yet*)
+  let tf_normal_call_backw man man_forw lv e (f:fundec) args getl (getl_forw : node * S_forw.C.t -> S_forw.D.t) sidel demandl getg getg_forw sideg =
+    let combine (cd, fc, fd) =
+      if M.tracing then M.traceli "combine" "local: %a" S_backw.D.pretty cd;
+      if M.tracing then M.trace "combine" "function: %a" S_backw.D.pretty fd;
+
+      (* Logs.debug "combine: local: %a" S_backw.D.pretty cd;
+         Logs.debug "combine: function: %a" S_backw.D.pretty fd; *)
+
+      let rec cd_man =
+        { man with
+          ask = (fun (type a) (q: a Queries.t) -> S_backw.query cd_man man_forw q);
+          local = cd;
+        }
+      in
+      let fd_man =
+        (* Inner scope to prevent unsynced fd_man from being used. *)
+        (* Extra sync in case function has multiple returns.
+           Each `Return sync is done before joining, so joined value may be unsound.
+           Since sync is normally done before tf (in common_man), simulate it here for fd. *)
+        (* TODO: don't do this extra sync here *)
+        let rec sync_man =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S_backw.query sync_man man_forw q);
+            local = fd;
+            (*prev_node = Function f*)
+            prev_node = FunctionEntry f;
+          }
+        in
+        (* TODO: more accurate man? *)
+        let synced = sync_backw sync_man man_forw in
+        let rec fd_man =
+          { sync_man with
+            ask = (fun (type a) (q: a Queries.t) -> S_backw.query fd_man man_forw q);
+            local = synced;
+          }
+        in
+        fd_man
+      in
+      let r = List.fold_left (fun acc fd1 ->
+          let rec fd1_man =
+            { fd_man with
+              ask = (fun (type a) (q: a Queries.t) -> S_backw.query fd1_man man_forw q);
+              local = fd1;
+            }
+          in
+          let combine_enved = S_backw.combine_env cd_man man_forw lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man) in
+          let rec combine_assign_man =
+            { cd_man with
+              ask = (fun (type a) (q: a Queries.t) -> S_backw.query combine_assign_man man_forw q);
+              local = combine_enved;
+            }
+          in
+          S_backw.D.join acc (S_backw.combine_assign combine_assign_man man_forw lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man))
+        ) (S_backw.D.bot ()) (S_backw.paths_as_set fd_man man_forw)
+      in
+      if M.tracing then M.traceu "combine" "combined local: %a" S_backw.D.pretty r;
+      (* Logs.debug "combined local: %a" S_backw.D.pretty r; *)
+      r
+    in
+    let paths = S_backw.enter man man_forw lv f args in
+
+    (* getl_forw should query the corresopoding unknown from the forward analysis *)
+    (* context = S_forw.context (S_forw.enter (getl_forw [this_node_, this_context])) *)
+
+    let man_forw =
+      { ask     = (fun (type a) (q: a Queries.t) -> failwith "manager for calculating context does not support queries")
+      ; emit    = (fun _ -> failwith "emit outside MCP")
+      ; node    = man.node
+      ; prev_node = MyCFG.dummy_node
+      ; control_context = man.control_context
+      ; context = man.context
+      ; edge    = man.edge
+      ; local   = (getl_forw (man.node, man.context ()))
+      ; global  = (fun g -> G_forw.spec (getg_forw (GVar.GV_forw.spec g)))
+      ; spawn   = (fun ?multiple _ _ _ -> failwith "manager for calculating context does not support spawn")
+      ; split   = (fun _ _ -> failwith "manager for calculating context does not support split") 
+      ; sideg   = (fun _ _ -> failwith "manager for calculating context does not support sideg")
+      } in
+
+    let paths_forw = 
+      Logs.debug "forward manager info at call to %a" Node.pretty man_forw.node;
+      S_forw.enter man_forw lv f args in
+
+    let paths = List.combine paths paths_forw in
+
+    (* filter paths were the forward analysis found out they are unreachable*)
+    let paths = List.filter (fun ((c,v),(_,b)) -> not (S_forw.D.is_bot b)) paths in 
+
+    (* this list now uses forward contexts*)
+    let paths = List.map (fun ((c,v),(_,b)) -> (c, S_forw.context man_forw f b, v)) paths in
+
+    (* The two lines below is what I should use. *)
+    (* List.iter (fun (c,fc,v) -> if not (S_backw.D.is_bot v) then sidel (Function f, fc) v) paths;  *)
+    (* let paths = List.map (fun (c,fc,v) -> (c, fc, if S_backw.D.is_bot v then v else getl (FunctionEntry f, fc))) paths in *)
+
+    (* A problem with my liveness analysis is that D.empty = D.bot, but I still need to evaluate a function since variables might become live inside. This is not optimal and the liveness analysis should be changed.*)
+    List.iter (fun (c,fc,v) -> sidel (Function f, fc) v) paths;
+    let paths = List.map (fun (c,fc,v) -> (c, fc, getl (FunctionEntry f, fc))) paths in
+
+
+    (* Don't filter bot paths, otherwise LongjmpLifter is not called. *)
+    (* let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in *)
+    let paths = List.map (Tuple3.map2 Option.some) paths in
+    if M.tracing then M.traceli "combine" "combining";
+    (* Logs.debug  "combining"; *)
+    let paths = List.map combine paths in
+    let r = List.fold_left S_backw.D.join (S_backw.D.bot ()) paths in
+    if M.tracing then M.traceu "combine" "combined: %a" S_backw.D.pretty r;
+    (* Logs.debug "combined: %a" S_backw.D.pretty r; *)
+    r
+
+  let rec tf_proc_backw var edge prev_node lv e args getl (getl_forw: node * S_forw.C.t -> S_forw.D.t) sidel demandl getg getg_forw sideg d =
+    let tf_special_call man man_forw f =
+      let once once_control init_routine =
+        (* Executes leave event for new local state d if it is not bottom *)
+        let leave_once d =
+          if not (S_backw.D.is_bot d) then
+            let rec man' =
+              { man with
+                ask = (fun (type a) (q: a Queries.t) -> S_backw.query man' man_forw q);
+                local = d;
+              }
+            in
+            S_backw.event man' man_forw (Events.LeaveOnce { once_control }) man'
+          else
+            S_backw.D.bot ()
+        in
+        let first_call =
+          let d' = S_backw.event man man_forw (Events.EnterOnce { once_control;  ran = false }) man in
+          tf_proc_backw var edge prev_node None init_routine [] getl getl_forw sidel demandl getg getg_forw sideg d'
+        in
+        let later_call = S_backw.event man man_forw (Events.EnterOnce { once_control;  ran = true }) man in
+        S_backw.D.join (leave_once first_call) (leave_once later_call)
+      in
+      let is_once = LibraryFunctions.find ~nowarn:true f in
+      (* If the prototpye for a library function is wrong, this will throw an exception. Such exceptions are usually unrelated to pthread_once, it is just that the call to `is_once.special` raises here *)
+      match is_once.special args with
+      | Once { once_control; init_routine } -> once once_control init_routine
+      | _  -> S_backw.special man man_forw lv f args
+    in
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let functions =
+      match e with
+      | Lval (Var v, NoOffset) ->
+        (* Handle statically known function call directly.
+           Allows deactivating base. *)
+        [v]
+      | _ ->
+        (*constructing fake forwards manager s.t. the inforamtion for the pointer information can be retireved*)
+        (* let r = ref [] in
+           let rec man_forw =
+           { ask     = (fun (type a) (q: a Queries.t) -> S_forw.query man_forw q)
+           ; emit    = (fun _ -> failwith "emit outside MCP")
+           ; node    = man.node
+           ; prev_node = man.prev_node (* this is problematic, as this is backwards *)
+           ; control_context = man.control_context
+           ; context = man.context
+           ; edge    = man.edge
+           ; local   = (getl_forw (man.node, man.context ())) (* accessing forward inforkation*)
+           ; global  = (fun _ -> failwith "whoops, query for resolving function pointer depends on globals")
+           ; spawn   = (fun ?multiple _ _ _ -> failwith "manager for resolving function pointer does not support spawn")
+           ; split   = (fun (d:S_forw.D.t) es -> assert (List.is_empty es); r := d::!r) (*what is this?*)
+           ; sideg   = (fun _ _ -> failwith "manager for resolving function pointer does not support sideg")
+           } in *)
+        let () = Logs.debug "manager info at call to function pointer %a" Node.pretty man_forw.node in
+        (* Depends on base for query. *)
+        let ad = man_forw.ask (Queries.EvalFunvar e) in
+        let res = Queries.AD.to_var_may ad in (* TODO: don't convert, handle UnknownPtr below *) 
+        (*PROBLEM: Pointer. Brauche Ergebnisse der anderen Analysen*)
+        (Logs.debug "(!) resolved function pointer to %d functions" (List.length res);
+         (match res with 
+          | x::xs -> 
+            List.iter (fun vi -> Logs.debug "      possible function: %s" vi.vname) res;
+          | _ -> ();
+         ));
+        res
+    in
+    let one_function f =
+      match Cil.unrollType f.vtype with
+      | TFun (_, params, var_arg, _)  ->
+        let arg_length = List.length args in
+        let p_length = Option.map_default List.length 0 params in
+        (* Check whether number of arguments fits. *)
+        (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *)
+        if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then
+          let d =
+            (match Cilfacade.find_varinfo_fundec f with
+             | fd when LibraryFunctions.use_special f.vname ->
+               M.info ~category:Analyzer "Using special for defined function %s" f.vname;
+               tf_special_call man man_forw f
+             | fd ->
+               tf_normal_call_backw man man_forw lv e fd args getl getl_forw sidel demandl getg getg_forw sideg
+             | exception Not_found ->
+               tf_special_call man man_forw f)
+          in
+          Some d
+        else begin
+          let geq = if var_arg then ">=" else "" in
+          M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
+          None
+        end
+      | _ ->
+        M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
+        None
+    in
+    let funs = List.filter_map one_function functions in
+    if [] = funs && not (S_backw.D.is_bot man.local) then begin
+      M.msg_final Warning ~category:Unsound ~tags:[Category Call] "No suitable function to call";
+      M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
+      d (* because LevelSliceLifter *)
+    end else
+      common_joins_backw man man_forw funs !r !spawns
+
+  let tf_asm_backw var edge prev_node getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.asm man man_forw in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  let tf_skip_backw var edge prev_node getl getl_forw sidel demandl getg getg_forw sideg d =
+    let man, r, spawns = common_man_backw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let man_forw = create_basic_man_forw var edge prev_node d getl getl_forw sidel demandl getg getg_forw sideg in
+    let d = S_backw.skip man man_forw in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join_backw man man_forw d !r !spawns
+
+  let tf_backw var getl getl_forw sidel demandl getg getg_forw sideg prev_node edge d =
+    begin match edge with
+      | Assign (lv,rv) -> tf_assign_backw var edge prev_node lv rv
+      | VDecl (v)      -> tf_vdecl_backw var edge prev_node v
+      | Proc (r,f,ars) -> tf_proc_backw var edge prev_node r f ars
+      | Entry f        -> tf_entry_backw var edge prev_node f
+      | Ret (r,fd)     -> tf_ret_backw var edge prev_node r fd
+      | Test (p,b)     -> tf_test_backw var edge prev_node p b
+      | ASM (_, _, _)  -> tf_asm_backw var edge prev_node (* TODO: use ASM fields for something? *)
+      | Skip           -> tf_skip_backw var edge prev_node
+    end getl getl_forw sidel demandl getg getg_forw sideg d
+
+  (* TODO: Don't call it prev_node when it is actually the next node. *)
+  let tf_backw var getl getl_forw sidel demandl getg getg_forw sideg prev_node (_,edge) d (f,t) =
+    (* let old_loc  = !Goblint_tracing.current_loc in
+       let old_loc2 = !Goblint_tracing.next_loc in
+       Goblint_tracing.current_loc := f;
+       Goblint_tracing.next_loc := t;
+       Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () ->
+        Goblint_tracing.current_loc := old_loc;
+        Goblint_tracing.next_loc := old_loc2
+       ) (fun () ->
+        let d       = tf_backw var getl sidel demandl getg sideg prev_node edge d in
+        d
+       ) *)
+    tf_backw var getl getl_forw sidel demandl getg getg_forw sideg prev_node edge d
+
+  let tf_backw (v,c) (edges, u) getl getl_forw sidel demandl getg getg_forw sideg =
+    let pval = getl (u,c) in
+    let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in
+    List.fold_left2 (|>) pval (List.map (tf_backw (v,Obj.repr (fun () -> c)) getl getl_forw sidel demandl getg getg_forw sideg u) edges) locs
+
+  let tf_backw (v,c) (e,u) getl getl_forw sidel demandl getg getg_forw sideg =
+    let old_node = !current_node in
+    let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
+    let new_fd = Node.find_fundec v in
+    if not (CilType.Fundec.equal old_fd new_fd) then
+      Timing.Program.enter new_fd.svar.vname;
+    let old_context = !M.current_context in
+    current_node := Some u;
+    M.current_context := Some (Obj.magic c); (* magic is fine because Spec is top-level Control Spec *)
+    Fun.protect ~finally:(fun () ->
+        current_node := old_node;
+        M.current_context := old_context;
+        if not (CilType.Fundec.equal old_fd new_fd) then
+          Timing.Program.exit new_fd.svar.vname
+      ) (fun () ->
+        let d       = tf_backw (v,c) (e,u) getl getl_forw sidel demandl getg getg_forw sideg in
+        d
+      )
+
+  let system_backw (v,c) =
+
+    match v with
+    | Function _ -> None
+    | _ ->
+      let tf_backw getl sidel demandl getg sideg =
+        let getl_backw d =  getl (`L_backw d) |> to_backw_d in
+        let getl_forw d =  getl (`L_forw d) |> to_forw_d in
+        let getg_backw v = getg (`Backw v) |> to_backw_g in
+        let getg_forw v = getg (`Forw v) |> to_forw_g in
+        let tf' eu = tf_backw (v,c) eu getl_backw getl_forw sidel demandl getg_backw getg_forw sideg in
+        let xs = List.map tf' (Cfg.next v) in
+        List.fold_left S_backw.D.join (S_backw.D.bot ()) xs
+      in
+      Some tf_backw
+
+  let system var =
+
+    (* let log () = 
+       match var with
+       | `L_forw (v, _)  -> Logs.debug "(*) Creating tf for forward variable %a" Node.pretty v
+       | `L_backw (v, _) -> Logs.debug "(*) Creating tf for backward variable %a" Node.pretty v
+       in
+       log(); *)
+
+    match var with
+    | `L_forw v ->
+      Forward.system v
+      |> Option.map (fun tf getl sidel demandl getg sideg ->
+          let getl' v = getl (`L_forw v) |> to_forw_d in
+          let sidel' v d = sidel (`L_forw v) (`Lifted1 d) in
+          let demandl' v = demandl (`L_forw v) in
+          let getg' v = getg (`Forw v) |> to_forw_g in
+          let sideg' v d = sideg (`Forw v) (of_forw_g d) in
+          tf getl' sidel' demandl' getg' sideg' |> (fun d -> `Lifted1 d)
+        )
+    | `L_backw v ->
+      system_backw v
+      |> Option.map (fun tf getl sidel demandl getg sideg ->
+          let sidel' v d = sidel (`L_backw v) (`Lifted2 d) in
+          let demandl' v = demandl (`L_backw v) in
+          let sideg' v d = sideg (`Backw v) (of_backw_g d) in
+          tf getl sidel' demandl' getg sideg' |> (fun d -> `Lifted2 d)
+        )
+
+  let iter_vars getl getg vq fl fg =
+    failwith "iter_vars not implemented for bidirectional constraint system."
+
+  let sys_change getl getg =
+    failwith "sys_change not implemented for bidirectional constraint system."
+
+  let postmortem_backw v =
+    failwith "postmortem not implemented for backward analysis"
+  (* match v with
+     | Function fd, c -> [(FunctionEntry fd, c)]
+     | _ -> [] *)
+
+  let postmortem = function
+    | `L_forw v -> List.map (fun v -> `L_forw v) (Forward.postmortem v)
+    | `L_backw v -> List.map (fun v -> `L_backw (v)) (postmortem_backw v)
+end
\ No newline at end of file
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 06b07e6f41..d9fd6a79bb 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -6,12 +6,14 @@ open Batteries
 open GoblintCil
 open MyCFG
 open Analyses
+open BackwAnalyses
 open Goblint_constraint.ConstrSys
 open Goblint_constraint.Translators
 open Goblint_constraint.SolverTypes
 open GobConfig
 open Constraints
 open SpecLifters
+open BidirConstrains
 
 module type S2S = Spec2Spec
 
@@ -153,7 +155,7 @@ struct
       let open Cilfacade in
       let warn_for_upjumps fundec gotos =
         if FunSet.mem live_funs fundec then (
-          (* set nortermiantion flag *)
+          (* set nontermination flag *)
           AnalysisState.svcomp_may_not_terminate := true;
           (* iterate through locations to produce warnings *)
           LocSet.iter (fun l _ ->
@@ -248,7 +250,7 @@ struct
 
     AnalysisState.should_warn := false; (* reset for server mode *)
 
-    (* exctract global xml from result *)
+    (* extract global xml from result *)
     let make_global_fast_xml f g =
       let open Printf in
       let print_globals k v =
@@ -843,16 +845,833 @@ struct
     Timing.wrap "result output" (ResultOutput.output (lazy local_xml) liveness gh make_global_fast_xml) (module FileCfg)
 end
 
-(* This function was originally a part of the [AnalyzeCFG] module, but
-   now that [AnalyzeCFG] takes [Spec] as a functor parameter,
-   [analyze_loop] cannot reside in it anymore since each invocation of
-   [get_spec] in the loop might/should return a different module, and we
-   cannot swap the functor parameter from inside [AnalyzeCFG]. *)
+(** Given a [Cfg], a [Spec_forw], [Spec_back], and an unused [Inc], computes the solution*)
+module AnalyzeCFG_bidir (Cfg:CfgBidirSkip) (Spec_forw:Spec) (BackwSpecSpec : BackwAnalyses.BackwSpecSpec) (Inc:Increment) =
+struct
+  module Spec_backw = BackwSpecSpec (Spec_forw)
+  (* The Equation system *)
+  module EQSys = BidirConstrains.BidirFromSpec (Spec_forw) (Spec_backw) (Cfg) (Inc)
+
+  (* Hashtbl for locals *)
+  module LHT   = BatHashtbl.Make (EQSys.LVar)
+  (* Hashtbl for globals *)
+  module GHT   = BatHashtbl.Make (EQSys.GVar)
+
+  (* The solver *)
+  module PostSolverArg =
+  struct
+    let should_prune = true
+    let should_verify = get_bool "verify"
+    let should_warn = get_string "warn_at" <> "never"
+    let should_save_run =
+      (* copied from solve_and_postprocess *)
+      let gobview = get_bool "gobview" in
+      let save_run = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
+      save_run <> ""
+  end
+  module Slvr  = (GlobSolverFromEqSolver (Goblint_solver.Selector.Make (PostSolverArg))) (EQSys) (LHT) (GHT)
+
+  (* Forward result module *)
+  (* Triple of the function, context, and the local value. It uses Spec and therefore has the wrong types.*)
+  module type ResultBundle = sig
+    module Spec : Spec
+    module RT : module type of AnalysisResult.ResultType2 (Spec)
+    module LT : module type of SetDomain.HeadlessSet (RT)
+    module Result : module type of AnalysisResult.Result (LT) (struct let result_name = "" end)
+    module ResultOutput : module type of AnalysisResultOutput.Make (Result)
+  end
+
+  module ResBundle_forw : ResultBundle with module Spec = Spec_forw = 
+  struct
+    module Spec = Spec_forw
+    module RT = AnalysisResult.ResultType2 (Spec_forw)
+    module LT = SetDomain.HeadlessSet (RT)
+    module Result = AnalysisResult.Result (LT) (struct let result_name = "analysis_forw" end)
+    module ResultOutput = AnalysisResultOutput.Make (Result)
+  end
+
+  (** this function converts the LHT to two Results of forward type*)
+  let solver2source_result h  = 
+    let res_forw = ResBundle_forw.Result.create 113 in
+    (* let res_backw = ResBundle_backw.Result.create 113 in *)
+
+    (* Adding the state at each system variable to the final result *)
+    let add_local_var_forw (n,es) state  =
+      (* Not using Node.location here to have updated locations in incremental analysis.
+          See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
+      let state = match state with
+        | `Lifted1 s -> s
+        | `Bot -> Spec_forw.D.bot ()
+        | `Top -> Spec_forw.D.top ()
+        | `Lifted2 _ -> failwith "Unexpected backward state in forward result"
+      in
+
+      let loc = UpdateCil.getLoc n in
+      if loc <> locUnknown then try
+          let fundec = Node.find_fundec n in
+          if ResBundle_forw.Result.mem res_forw n then
+            (* If this source location has been added before, we look it up
+              * and add another node to it information to it. *)
+            let prev = ResBundle_forw.Result.find res_forw n in
+            ResBundle_forw.Result.replace res_forw n (ResBundle_forw.LT.add (es,state,fundec) prev)
+          else
+            ResBundle_forw.Result.add res_forw n (ResBundle_forw.LT.singleton (es,state,fundec))
+        (* If the function is not defined, and yet has been included to the
+          * analysis result, we generate a warning. *)
+        with Not_found ->
+          Messages.debug ~category:Analyzer ~loc:(CilLocation loc) "Calculated state for undefined function: unexpected node %a" Node.pretty_trace n
+    in
+
+    LHT.iter (fun key -> 
+        match key with  
+        | `L_forw (n,es) -> add_local_var_forw (n,es)
+        | `L_backw (n,es) -> (fun _ -> ())  (* add_local_var_backw (n, es))*) ) h;
+
+    res_forw(*, res_backw*)
+
+
+  (** [analyze file startfuns exitfuns otherfuns] is the main function to preform the selected analyses.*)
+  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) =
+    let module FileCfg: FileCfg =
+    struct
+      let file = file
+      module Cfg = Cfg
+    end
+    in
+
+    let module GV_forw = GVarF (Spec_forw.V) in
+    let module GV_backw = GVarF (Spec_backw.V) in
+
+    let module G_forw = GVarG (Spec_forw.G) (Spec_forw.C) in
+    let module G_backw = GVarG (Spec_backw.G) (Spec_backw.C) in
+
+
+    let log_analysis_setup () =
+      let log_fun_list name funs =
+        let fun_names = List.map (fun f -> f.svar.vname) funs in
+        Logs.debug "%s functions: %s" name (String.concat ", " fun_names)
+      in
+      Logs.debug "================= Analysis Setup ================";
+      log_fun_list "Start" startfuns;
+      log_fun_list "Exit" exitfuns;
+      log_fun_list "Other" otherfuns;
+      Logs.debug "=================================================";
+    in
+    log_analysis_setup ();
+
+    AnalysisState.should_warn := false; 
+
+    (* initialize hastable for globals*)
+    let gh = GHT.create 13 in
+    let getg v = GHT.find_default gh v (EQSys.G.bot ()) in
+    let sideg v d = GHT.replace gh v (EQSys.G.join (getg v) d)
+    in
+
+    (** this function calculates and returns  [startvars'_forw] and [entrystates_forw] *)
+    let do_forward_inits () : (node * Spec_forw.C.t) list * ((node * Spec_forw.C.t) * Spec_forw.D.t) list = 
+
+      (* wrapping functions accessing and modifying global variables *)
+      let sideg_forw v d = sideg (`Forw (v)) ((`Lifted1 d)) in
+
+      (* the intit globals should not depend on each other*)
+      let getg_forw v = G_forw.bot () in
+
+      let do_extern_inits_forw man (file: file) : Spec_forw.D.t =
+        let module VS = Set.Make (Basetype.Variables) in
+        let add_glob s = function
+          | GVar (v,_,_) -> VS.add v s
+          | _            -> s
+        in
+        let vars = foldGlobals file add_glob VS.empty in
+        let set_bad v st =
+          Spec_forw.assign {man with local = st} (var v) MyCFG.unknown_exp
+        in
+        let is_std = function
+          | {vname = ("__tzname" | "__daylight" | "__timezone"); _} (* unix time.h *)
+          | {vname = ("tzname" | "daylight" | "timezone"); _} (* unix time.h *)
+          | {vname = "getdate_err"; _} (* unix time.h, but somehow always in MacOS even without include *)
+          | {vname = ("stdin" | "stdout" | "stderr"); _} (* standard stdio.h *)
+          | {vname = ("optarg" | "optind" | "opterr" | "optopt" ); _} (* unix unistd.h *)
+          | {vname = ("__environ"); _} -> (* Linux Standard Base Core Specification *)
+            true
+          | _ -> false
+        in
+        let add_externs s = function
+          | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) && not (get_bool "exp.hide-std-globals" && is_std v) -> set_bad v s
+          | _ -> s
+        in
+        Logs.debug "startstate of Spec_forw: %a" Spec_forw.D.pretty (Spec_forw.startstate MyCFG.dummy_func.svar);
+        foldGlobals file add_externs (Spec_forw.startstate MyCFG.dummy_func.svar)
+      in
+
+      (** this function uses cil's global-inits function to get a starting state *)
+      let do_global_inits_forw (file: file) : Spec_forw.D.t * fundec list =
+        let man =
+          { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+          ; emit   = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
+          ; node    = MyCFG.dummy_node
+          ; prev_node = MyCFG.dummy_node
+          ; control_context = (fun () -> man_failwith "Global initializers have no context.")
+          ; context = (fun () -> man_failwith "Global initializers have no context.")
+          ; edge    = MyCFG.Skip
+          ; local   = Spec_forw.D.top ()
+          ; global  = (fun g -> G_forw.spec (getg_forw (GV_forw.spec g)))
+          ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+          ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
+          ; sideg   = (fun g d -> sideg_forw (GV_forw.spec g) (G_forw.create_spec d))
+          }
+        in
+
+        let edges = CfgTools.getGlobalInits file in
+        Logs.debug "Executing %d assigns." (List.length edges);
+        let funs = ref [] in
+
+        let transfer_func (st : Spec_forw.D.t) (loc, edge) : Spec_forw.D.t =
+          match edge with
+          | MyCFG.Entry func        -> Spec_forw.body {man with local = st} func
+          | MyCFG.Assign (lval,exp) ->
+            begin match lval, exp with
+              | (Var v,o), (AddrOf (Var f,NoOffset))
+                when v.vstorage <> Static && isFunctionType f.vtype ->
+                (try funs := Cilfacade.find_varinfo_fundec f :: !funs with Not_found -> ())
+              | _ -> ()
+            end;
+            let res = Spec_forw.assign {man with local = st} lval exp in
+            (* Needed for privatizations (e.g. None) that do not side immediately *)
+            let res' = Spec_forw.sync {man with local = res} `Normal in
+            res'
+          | _                       -> failwith "Unsupported global initializer edge"
+        in
+
+        let with_externs = do_extern_inits_forw man file in
+        Logs.debug "witch_externs: %a" Spec_forw.D.pretty with_externs;
+        let result : Spec_forw.D.t = List.fold_left transfer_func with_externs edges in
+        result, !funs
+      in
+
+      let startstate, _ = do_global_inits_forw file in
+
+      (** calculate startvars *)
+      let calculate_startvars_forw ()  =
+
+        let enter_with st fd =
+          let st = st fd.svar in
+          let man =
+            { 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 () -> man_failwith "enter_with has no control_context.")
+            ; context = Spec_forw.startcontext
+            ; edge    = MyCFG.Skip
+            ; local   = st
+            ; global  = (fun g -> G_forw.spec (getg_forw (GV_forw.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_forw (GV_forw.spec g) (G_forw.create_spec (d)))
+            }
+          in
+          let args = List.map (fun x -> MyCFG.unknown_exp) fd.sformals in
+          let ents = Spec_forw.enter man None fd args in
+          List.map (fun (_,s) -> fd, s) ents
+        in
+
+        (try MyCFG.dummy_func.svar.vdecl <- (List.hd otherfuns).svar.vdecl with Failure _ -> ());
+
+        let startvars =
+          if startfuns = []
+          then [[MyCFG.dummy_func, startstate]]
+          else
+            let morph f = Spec_forw.morphstate f startstate in
+            List.map (enter_with morph) startfuns
+        in
+
+        let exitvars = List.map (enter_with Spec_forw.exitstate) exitfuns in
+        let otherstate st v =
+          let man =
+            { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit   = (fun _ -> failwith "Cannot \"emit\" in otherstate context.")
+            ; node    = MyCFG.dummy_node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "enter_func has no context.")
+            ; context = (fun () -> man_failwith "enter_func has no context.")
+            ; edge    = MyCFG.Skip
+            ; local   = st
+            ; global  = (fun g -> G_forw.spec (getg_forw (GV_forw.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_forw  (GV_forw.spec g) (G_forw.create_spec (d)))
+            }
+          in
+          (* TODO: don't hd *)
+          List.hd (Spec_forw.threadenter man ~multiple:false None v [])
+          (* TODO: do threadspawn to mainfuns? *)
+        in
+        let prestartstate = Spec_forw.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *)
+        let othervars = List.map (enter_with (otherstate prestartstate)) otherfuns in
+        let startvars = List.concat (startvars @ exitvars @ othervars) in
+        if startvars = [] then
+          failwith "BUG: Empty set of start variables; may happen if enter_func of any analysis returns an empty list.";
+
+        AnalysisState.global_initialization := false;
+
+        let man 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 () -> man_failwith "enter_with has no control_context.")
+          ; context = Spec_forw.startcontext
+          ; edge    = MyCFG.Skip
+          ; local   = e
+          ; global  = (fun g -> G_forw.spec (getg_forw (GV_forw.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_forw (GV_forw.spec g) (G_forw.create_spec d))
+          }
+        in
+        let startvars' = List.map (fun (n,e) -> (MyCFG.Function n, Spec_forw.context (man e) n e)) startvars in
+        let entrystates = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec_forw.context (man e) n e), e) startvars in
+
+        startvars', entrystates
+      in
+
+      calculate_startvars_forw ()
+    in
+
+    (** this function calculates and returns  [startvars'_backw] and [entrystates_backw] *)
+    let do_backward_inits () : (node * Spec_backw.C.t) list * ((node * Spec_forw.C.t) * Spec_backw.D.t) list = 
+
+      let sideg_backw v d = sideg (`Backw v) (EQSys.G.create_spec (`Lifted2 d)) in
+
+      (* the intit globals should not depend on each other*)
+      let getg_backw v = G_backw.bot () in
+
+      let do_extern_inits_backw man man_forw (file: file) : Spec_backw.D.t =
+        let module VS = Set.Make (Basetype.Variables) in
+        let add_glob s = function
+          | GVar (v,_,_) -> VS.add v s
+          | _            -> s
+        in
+        let vars = foldGlobals file add_glob VS.empty in
+        let set_bad v st =
+          Spec_backw.assign {man with local = st} man_forw (var v) MyCFG.unknown_exp
+        in
+        let is_std = function
+          | {vname = ("__tzname" | "__daylight" | "__timezone"); _} (* unix time.h *)
+          | {vname = ("tzname" | "daylight" | "timezone"); _} (* unix time.h *)
+          | {vname = "getdate_err"; _} (* unix time.h, but somehow always in MacOS even without include *)
+          | {vname = ("stdin" | "stdout" | "stderr"); _} (* standard stdio.h *)
+          | {vname = ("optarg" | "optind" | "opterr" | "optopt" ); _} (* unix unistd.h *)
+          | {vname = ("__environ"); _} -> (* Linux Standard Base Core Specification *)
+            true
+          | _ -> false
+        in
+        let add_externs s = function
+          | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) && not (get_bool "exp.hide-std-globals" && is_std v) -> set_bad v s
+          | _ -> s
+        in
+        foldGlobals file add_externs (Spec_backw.startstate MyCFG.dummy_func.svar)
+      in
+
+      (** This function analyses cil's global-inits function to get a starting state *)
+      let do_global_inits_backw (file: file) : Spec_backw.D.t * fundec list =
+
+        let man =
+          { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+          ; emit   = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
+          ; node    = MyCFG.dummy_node
+          ; prev_node = MyCFG.dummy_node
+          ; control_context = (fun () -> man_failwith "Global initializers have no context.")
+          ; context = (fun () -> man_failwith "Global initializers have no context.")
+          ; edge    = MyCFG.Skip
+          ; local   = Spec_backw.D.top ()
+          ; global  = (fun g -> G_backw.spec (getg_backw (GV_backw.spec g)))
+          ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+          ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
+          ; sideg   = (fun g d -> sideg_backw (GV_backw.spec g) d)
+          }
+        in
+
+        let man_forw =
+          { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+          ; emit   = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
+          ; node    = MyCFG.dummy_node
+          ; prev_node = MyCFG.dummy_node
+          ; control_context = (fun () -> man_failwith "Global initializers have no context.")
+          ; context = (fun () -> man_failwith "Global initializers have no context.")
+          ; edge    = MyCFG.Skip
+          ; local   = Spec_forw.D.top () (*Should probably use local from already initialized forward variable.*)
+          ; global  = (fun _ -> Spec_forw.G.bot ())
+          ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+          ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
+          ; sideg   = (fun _ _ -> failwith "forw_man in the backwards initialization should not be used to sideeffect globals.")
+          }
+        in
+
+        let edges = CfgTools.getGlobalInits file in
+        Logs.debug "Executing %d assigns." (List.length edges);
+        let funs = ref [] in
+
+        let transfer_func (st : Spec_backw.D.t) (loc, edge) : Spec_backw.D.t =
+          match edge with
+          | MyCFG.Entry func        -> Spec_backw.body {man with local = st} man_forw func
+          | MyCFG.Assign (lval,exp) ->
+            begin match lval, exp with
+              | (Var v,o), (AddrOf (Var f,NoOffset))
+                when v.vstorage <> Static && isFunctionType f.vtype ->
+                (try funs := Cilfacade.find_varinfo_fundec f :: !funs with Not_found -> ())
+              | _ -> ()
+            end;
+            let res = Spec_backw.assign {man with local = st} man_forw lval exp in
+            (* Needed for privatizations (e.g. None) that do not side immediately *)
+            let res' = Spec_backw.sync {man with local = res} man_forw `Normal in
+            res'
+          | _                       -> failwith "Unsupported global initializer edge"
+        in
+
+        let with_externs = do_extern_inits_backw man man_forw file in
+        let result : Spec_backw.D.t = List.fold_left transfer_func with_externs edges in
+        result, !funs
+      in
+
+      let startstate, _ = do_global_inits_backw file in
+
+      (** calculate startvars *)
+      let calculate_startvars_backw ()  =
+
+        let enter_with st fd =
+          let st = st fd.svar in
+          let man =
+            { 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 () -> man_failwith "enter_with has no control_context.")
+            ; context = Spec_forw.startcontext
+            ; edge    = MyCFG.Skip
+            ; local   = st
+            ; global  = (fun g -> G_backw.spec (getg_backw (GV_backw.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_backw (GV_backw.spec g) d)
+            }
+          in
+          let man_forw =
+            { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit   = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
+            ; node    = man.node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "Global initializers have no context.")
+            ; context = man.context
+            ; edge    = MyCFG.Skip
+            ; local   = Spec_forw.D.top () (*Should probably use local from already initialized forward variable.*)
+            ; global  = (fun _ -> Spec_forw.G.bot ())
+            ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+            ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
+            ; sideg   = (fun _ _ -> failwith "forw_man in the backwards initialization should not be used to sideeffect globals.")
+            }
+          in
+
+          let args = List.map (fun x -> MyCFG.unknown_exp) fd.sformals in
+          let ents = Spec_backw.enter man man_forw None fd args in
+          List.map (fun (_,s) -> fd, s) ents
+        in
+
+        (try MyCFG.dummy_func.svar.vdecl <- (List.hd otherfuns).svar.vdecl with Failure _ -> ());
+
+        let startvars =
+          if startfuns = []
+          then [[MyCFG.dummy_func, startstate]]
+          else
+            let morph f = Spec_backw.morphstate f startstate in
+            List.map (enter_with morph) startfuns
+        in
+
+        let exitvars = List.map (enter_with Spec_backw.exitstate) exitfuns in
+        let otherstate st v =
+          let man =
+            { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit   = (fun _ -> failwith "Cannot \"emit\" in otherstate context.")
+            ; node    = MyCFG.dummy_node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "enter_func has no context.")
+            ; context = (fun () -> man_failwith "enter_func has no context.")
+            ; edge    = MyCFG.Skip
+            ; local   = st
+            ; global  = (fun g -> G_backw.spec (getg_backw (GV_backw.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_backw (GV_backw.spec g) d)
+            }
+          in
+
+          let man_forw =
+            { ask     = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit   = (fun _ -> failwith "Cannot \"emit\" in otherstate context.")
+            ; node    = man.node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "enter_func has no context.")
+            ; context = (fun () -> man_failwith "enter_func has no context.")
+            ; edge    = MyCFG.Skip
+            ; local   = Spec_forw.D.top () (*TODO: SOULD I GET THE VALUE FROM THE FORWARD INITIALIZATION?*)
+            ; global  = (fun _ -> Spec_forw.G.bot ()) (*TODO: SHOULD I ALLOW TO ASK FOR GLOBALS?*)
+            ; 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 _ _ -> failwith "forw_man in the backwards initialization should not be used to sideeffect globals.")
+            }
+          in
+          (* TODO: don't hd *)
+          List.hd (Spec_backw.threadenter man man_forw ~multiple:false None v [])
+          (* TODO: do threadspawn to mainfuns? *)
+        in
+        let prestartstate = Spec_backw.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *)
+        let othervars = List.map (enter_with (otherstate prestartstate)) otherfuns in
+        let startvars = List.concat (startvars @ exitvars @ othervars) in
+        if startvars = [] then
+          failwith "BUG: Empty set of start variables; may happen if enter_func of any analysis returns an empty list.";
+
+        AnalysisState.global_initialization := false;
+
+        (*
+        let man 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 () -> man_failwith "enter_with has no control_context.")
+          ; context = Spec_forw.startcontext
+          ; edge    = MyCFG.Skip
+          ; local   = e
+          ; global  = (fun g -> G_backw.spec (getg_backw (GV_backw.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_backw (GV_backw.spec g) d)
+          }
+        in
+        let startvars' = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec_backw.context (man e) n e)) startvars in
+        let entrystates = List.map (fun (n,e) -> (MyCFG.Function n, Spec_backw.context (man e) n e), e) startvars in *)
+
+        (* Using dummy contexts which will be replaced by the contexts of the forward functions*)
+        let startvars' = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec_forw.startcontext ())) startvars in
+        let entrystates = List.map (fun (n,e) -> (MyCFG.Function n, Spec_forw.startcontext ()), e) startvars in
+
+        startvars', entrystates
+      in
+
+      calculate_startvars_backw ()
+    in
+
+    (** calculates and combines the solver input calculation from the forwards and backwards part of the constraint system. Returns [startvars'] and [entrystate] and [entrystates_global].*)
+    let calculate_solver_input () =
+      (* Spec_forw (MCP) initialization *)
+      AnalysisState.should_warn := PostSolverArg.should_warn;
+      Spec_forw.init None;
+      Access.init file;
+      AnalysisState.should_warn := false;
+
+
+      let entrystates_global = GHT.to_list gh in
+      let startvars'_forw, entrystates_forw = do_forward_inits () in
+      let startvars'_backw, entrystates_backw = do_backward_inits () in
+
+      (* Let's assume there is only one entrystate and startvar each. In what examples is this not the case?*)
+      let forward_context = match startvars'_forw with
+        | (_, ctx) :: _ -> ctx
+        | [] -> failwith "No startvars from forward analysis"
+      in 
+      let startvars'_backw = List.map (fun (n, _) -> (n, forward_context)) startvars'_backw in
+      let entrystates_backw = List.map (fun ((n, _), d) -> ((n, forward_context), d)) entrystates_backw in
+
+      (* Lifting and combining the startvars and entrystates from forwards and backwards analysis*)
+      let startvars' = List. append (List.map (fun v -> `L_forw v) startvars'_forw) (List.map (fun v -> `L_backw v) startvars'_backw) in
+      (* let startvars' = List. append (List.map (fun v -> `L_backw v) startvars'_backw) (List.map (fun v -> `L_forw v) startvars'_forw) in *)
+      let entrystates = List.append (List.map (fun (v, d) -> (`L_forw v, `Lifted1 d)) entrystates_forw) (List.map (fun (v, d) -> (`L_backw v, `Lifted2 d)) entrystates_backw) in
+
+      startvars', entrystates, entrystates_global
+    in
+
+
+    (** solves constraint system*)
+    let solve () = 
+      let solver_data = None in
+      let startvars', entrystates, entrystates_global = calculate_solver_input () in
+
+      let log_analysis_inputs () =
+        Logs.debug "================= Analysis Inputs ================";
+
+        (* Log entrystates *)
+        Logs.debug "--- Entry States (count: %d) ---" (List.length entrystates);
+        List.iteri (fun i (v, state) ->
+            Logs.debug "EntryState %d:" (i + 1);
+            Logs.debug "  Var: %a" EQSys.LVar.pretty_trace v;
+            (* (match v with
+               | `L_forw (node, ctx)
+               | `L_backw (node, ctx) ->
+               Logs.debug "  Node: %a" Node.pretty_trace node;
+               Logs.debug "  Context: %a" Spec_forw.C.pretty ctx
+               ); *)
+            (match state with 
+             | `Lifted1 d ->
+               Logs.debug "  State: %a" Spec_forw.D.pretty d
+             | `Lifted2 d ->
+               Logs.debug "  State: %a" Spec_backw.D.pretty d
+             | `Top ->
+               Logs.debug "  State kind: Top";
+             | `Bot ->
+               Logs.debug "  State kind: Bot"
+            );
+          ) entrystates;
+
+        (* Log entrystates_global *)
+        Logs.debug "--- Global Entry States (count: %d) ---" (List.length entrystates_global);
+        List.iteri (fun i (gvar, gstate) ->
+            Logs.debug "GlobalEntryState %d:" (i + 1);
+            Logs.debug "  GVar: %a" EQSys.GVar.pretty_trace gvar;
+            Logs.debug "  GState: %a" EQSys.G.pretty gstate;
+          ) entrystates_global;
+
+        (* Log startvars' *)
+        Logs.debug "--- Start Variables (count: %d) ---" (List.length startvars');
+        List.iteri (fun i v ->
+            Logs.debug "StartVar %d:" (i + 1);
+            Logs.debug "  Var: %a" EQSys.LVar.pretty_trace v;
+            (* (match v with
+               | `L_forw (node, ctx)
+               | `L_backw (node, ctx) ->
+               Logs.debug "  Node: %a" Node.pretty_trace node;
+               Logs.debug "  Context: %a" Spec_forw.C.pretty ctx
+               ) *)
+          ) startvars';
+        Logs.debug "=============== End Analysis Inputs =============="
+      in
+      log_analysis_inputs ();
+
+      AnalysisState.should_warn := true; 
+
+      let (lh, gh), solver_data = Slvr.solve entrystates entrystates_global startvars' solver_data in
+
+      let log_lh_contents lh = 
+        let print_forw_entries : bool = false in
+        let print_backw_entries : bool = false in
+
+        if print_forw_entries || print_backw_entries then (
+
+          Logs.debug "================= LHT Contents ===================";
+          Logs.debug "LHT size: %d" (LHT.length lh);
+          let count = ref 0 in
+
+          Logs.debug "--- Full entry details ---";
+          LHT.iter (fun v state ->
+              incr count;
+              Logs.debug "Entry %d:" !count;
+              if (match v with `L_forw _ -> print_forw_entries | `L_backw _ -> print_backw_entries)
+              then (
+                Logs.debug "  Var: %a" EQSys.LVar.pretty_trace v;
+                Logs.debug "  Context: %a" Spec_forw.C.pretty (match v with
+                    | `L_forw (_, ctx)
+                    | `L_backw (_, ctx) -> ctx);
+                (match state with 
+                 | `Lifted1 d -> 
+                   (try
+                      Logs.debug "  State:%a" Spec_forw.D.pretty d
+                    with e ->
+                      Logs.debug "  State: ERROR - %s" (Printexc.to_string e))
+                 | `Lifted2 d ->
+                   (try
+                      Logs.debug "  State: %a" Spec_backw.D.pretty d
+                    with e ->
+                      Logs.debug "  State: ERROR - %s" (Printexc.to_string e)
+                   );
+                 | `Top ->
+                   Logs.debug "  State kind: Top";
+                 | `Bot ->
+                   Logs.debug "  State kind: Bot"
+                );
+              ) else (
+                Logs.debug "  (Entry skipped in log)"
+              )
+            )
+            lh;
+          Logs.debug "Total entries in LHT: %d" !count;
+          Logs.debug "=============== End LHT Contents =================";
+        ) else ();
+      in
+      log_lh_contents lh;
+
+      (* To check for unnacessary assigns, one has to take the join over all variables for that programm point*)
+      let warn_unnecessary_assignments () =
+        let post_backward_states_for_node (node: Node.t) : Spec_backw.D.t list =
+          let succ_nodes = List.map snd (Cfg.next node) in
+          LHT.fold (fun key state acc ->
+              match key, state with
+              | `L_backw (node', _), `Lifted2 d when List.exists (Node.equal node') succ_nodes -> d :: acc
+              | _ -> acc
+            ) lh []
+        in
+
+        let may_be_dead_assignment_in_state (node: Node.t) (state: Spec_backw.D.t) (lv: lval) : bool =
+          (* log *)
+          (* Logs.debug "Checking if assignment may be dead at node %a in state %a" Node.pretty_trace node Spec_backw.D.pretty state; *)
+
+          let man_backw =
+            { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit = (fun _ -> failwith "Cannot \"emit\" in dead-assignment query helper.")
+            ; node = node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "dead-assignment query helper has no control_context.")
+            ; context = (fun () -> man_failwith "dead-assignment query helper has no context.")
+            ; edge = MyCFG.Skip
+            ; local = state
+            ; global = (fun _ -> Spec_backw.G.bot ())
+            ; spawn = (fun ?(multiple=false) _ -> failwith "dead-assignment query helper cannot spawn threads.")
+            ; split = (fun _ -> failwith "dead-assignment query helper cannot split paths.")
+            ; sideg = (fun _ _ -> failwith "dead-assignment query helper cannot side-effect globals.")
+            }
+          in
+          let man_forw =
+            { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+            ; emit = (fun _ -> failwith "Cannot \"emit\" in dead-assignment query helper.")
+            ; node = node
+            ; prev_node = MyCFG.dummy_node
+            ; control_context = (fun () -> man_failwith "dead-assignment query helper has no control_context.")
+            ; context = (fun () -> man_failwith "dead-assignment query helper has no context.")
+            ; edge = MyCFG.Skip
+            ; local = Spec_forw.D.top ()
+            ; global = (fun _ -> Spec_forw.G.bot ())
+            ; spawn = (fun ?(multiple=false) _ -> failwith "dead-assignment query helper cannot spawn threads.")
+            ; split = (fun _ -> failwith "dead-assignment query helper cannot split paths.")
+            ; sideg = (fun _ _ -> failwith "dead-assignment query helper cannot side-effect globals.")
+            }
+          in
+          Spec_backw.query man_backw man_forw (Queries.MayBeDeadAssignment lv)
+        in
+
+        let assigned_lvals_of_stmt (s: stmt) : lval list =
+          match s.skind with
+          | Instr instrs ->
+            List.fold_left (fun acc instr ->
+                match instr with
+                | Set (lv, _, _, _) -> lv :: acc
+                | Call (Some lv, _, _, _, _) -> lv :: acc
+                | _ -> acc
+              ) [] instrs
+          | _ -> []
+        in
+
+        let warn_assignment_stmt (s: stmt) =
+          let node = Statement s in
+          let assigned_lvals = assigned_lvals_of_stmt s in
+          match assigned_lvals with
+          | [] -> ()
+          | _ ->
+            let states = post_backward_states_for_node node in
+            if states <> [] then (
+              List.iter (fun lv ->
+                  let dead_in_all_contexts =
+                    List.for_all (fun st -> may_be_dead_assignment_in_state node st lv) states
+                  in
+                  if dead_in_all_contexts then
+                    M.warn ~loc:(M.Location.Node node) ~category:MessageCategory.Program "Unnecessary assignment: this assignment may be dead in every post-assignment context."
+                ) assigned_lvals
+            )
+        in
+        List.iter (function
+            | GFun (fd, _) -> List.iter warn_assignment_stmt fd.sallstmts
+            | _ -> ()
+          ) file.globals
+      in
+      warn_unnecessary_assignments ();
+
+      let make_global_fast_xml f g =
+        let open Printf in
+        let print_globals k v =
+          fprintf f "\n<glob><key>%s</key>%a</glob>" (XmlUtil.escape (EQSys.GVar.show k)) EQSys.G.printXml v;
+        in
+        GHT.iter print_globals g
+      in
+
+      let liveness _ = true in
+
+      let local_xml_forw = solver2source_result lh in
+
+      ResBundle_forw.ResultOutput.output (lazy local_xml_forw) liveness gh make_global_fast_xml (module FileCfg); 
+
+      (*This is disgusting, but I have more important things to do right now.*)
+      let output_wp_results_to_xml lh =
+        (* iterate through all nodes and update corresponding .xml in result/nodes *)
+        LHT.iter (fun v state ->
+            match v with
+            | `L_forw _ -> ()
+            | `L_backw (node, c) -> (
+                let state = match state with
+                  | `Lifted2 d -> d
+                  | _ -> failwith "Expected backward state"
+                in
+                try
+                  let node_id_str = Node.show_id node in
+
+                  let xml_path = Filename.concat "./result/nodes" (node_id_str ^ ".xml") in
+                  if Sys.file_exists xml_path then (
+                    (* Read existing XML *)
+                    let ic = Stdlib.open_in xml_path in
+                    let content = Stdlib.really_input_string ic (Stdlib.in_channel_length ic) in
+                    Stdlib.close_in ic;
+
+                    (* Create WP analysis data *)
+                    let wp_res = Pretty.sprint ~width:100 (Spec_backw.D.pretty () state) in
+                    let wp_res_escaped = XmlUtil.escape wp_res in
+                    let wp_data =
+                      "\n<wp_path>\n<analysis name=\"wp_test\">\n<value>\n<data>" ^ wp_res_escaped ^" \n</data>\n</value>\n</analysis>\n</wp_path>\n"
+                    in
+
+                    (* Insert before </path>*)
+                    let close_pattern = "</call>" in
+                    let updated_content =
+                      try
+                        let insert_pos = Str.search_backward (Str.regexp_string close_pattern) content (String.length content) in
+                        let before = String.sub content 0 insert_pos in
+                        let after = String.sub content insert_pos (String.length content - insert_pos) in
+                        before ^ wp_data ^ after
+                      with Not_found ->
+                        content ^ wp_data
+                    in
+
+                    (* Write back *)
+                    let oc = Stdlib.open_out xml_path in
+                    Stdlib.output_string oc updated_content;
+                    Stdlib.close_out oc;
+                    (* Logs.debug "Updated XML file for node %s" node_id_str *)
+                  )
+                with _ -> ()  (* Skip errors silently *)
+              )
+          ) lh
+      in
+      output_wp_results_to_xml lh;
+    in
+
+    solve();
+end
+
+(** This function was originally a part of the [AnalyzeCFG] module, but
+    now that [AnalyzeCFG] takes [Spec] as a functor parameter,
+    [analyze_loop] cannot reside in it anymore since each invocation of
+    [get_spec] in the loop might/should return a different module, and we
+    cannot swap the functor parameter from inside [AnalyzeCFG]. *)
 let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info =
   try
+
     let (module Spec) = get_spec () in
-    let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in
-    GobConfig.with_immutable_conf (fun () -> A.analyze file fs)
+
+    if (GobConfig.get_bool "ana.wp_run") then (
+      let module LivenesSpec = Liveness.BackwSpec in
+      let module A = AnalyzeCFG_bidir (CFG) (Spec) (LivenesSpec) (struct let increment = change_info end) in
+      GobConfig.with_immutable_conf (fun () -> A.analyze file fs) 
+    ) else (
+      let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in
+      GobConfig.with_immutable_conf (fun () -> A.analyze file fs)
+    )
+
   with Refinement.RestartAnalysis ->
     (* Tail-recursively restart the analysis again, when requested.
         All solving starts from scratch.
diff --git a/tests/regression/99-tutorials/05-basic_liveness.c b/tests/regression/99-tutorials/05-basic_liveness.c
new file mode 100644
index 0000000000..6b886e91af
--- /dev/null
+++ b/tests/regression/99-tutorials/05-basic_liveness.c
@@ -0,0 +1,18 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+int main()
+{
+  int x = 1;
+  int y = 2;
+  int z = 3;  // this assignment should yield a warning
+
+  int a = rand();
+
+  if (a) {
+    x = x + y;
+  } 
+
+  return x;
+}
+
diff --git a/tests/regression/99-tutorials/06-forward_branch_info.c b/tests/regression/99-tutorials/06-forward_branch_info.c
new file mode 100644
index 0000000000..b5a377c7f4
--- /dev/null
+++ b/tests/regression/99-tutorials/06-forward_branch_info.c
@@ -0,0 +1,14 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int main()
+{
+  int x = 1;
+  int y = 2; // this assignment should yield a warning, as the path where y is used is never taken
+  int z = 0; 
+
+  if (z) {
+    x = x + y;
+  } 
+
+  return x;
+}
diff --git a/tests/regression/99-tutorials/07-basic_function_call.c b/tests/regression/99-tutorials/07-basic_function_call.c
new file mode 100644
index 0000000000..99d6702f96
--- /dev/null
+++ b/tests/regression/99-tutorials/07-basic_function_call.c
@@ -0,0 +1,21 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int f(int a, int b) {
+  
+  if (a < 0) {
+    return a + b;
+  } else {
+    return a;
+  }
+
+}
+
+int main()
+{
+  int x = 1;
+  int y = 2; // this assignment should yield a warning, as y is not used in the path taken in the called function
+
+  int z = f(x, y);
+
+  return z;
+}
diff --git a/tests/regression/99-tutorials/08-function_pointer_resolve.c b/tests/regression/99-tutorials/08-function_pointer_resolve.c
new file mode 100644
index 0000000000..ba7a3fcafe
--- /dev/null
+++ b/tests/regression/99-tutorials/08-function_pointer_resolve.c
@@ -0,0 +1,23 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int f(int a, int b) {
+  
+  if (a < 0) {
+    return a + b;
+  } else {
+    return a;
+  }
+
+}
+
+int main()
+{
+  int x = 1;
+  int y = 2; // this assignment should yield a warning, as y is not used in the path taken in the called function
+
+  int (*h) (int, int) = &f;
+
+  int z = h(x, y);
+
+  return z;
+}
diff --git a/tests/regression/99-tutorials/09-ambigious_function_pointer.c b/tests/regression/99-tutorials/09-ambigious_function_pointer.c
new file mode 100644
index 0000000000..976a1c1ecf
--- /dev/null
+++ b/tests/regression/99-tutorials/09-ambigious_function_pointer.c
@@ -0,0 +1,41 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+int f(int a, int b) {
+  
+  if (a > 0) {
+    return a + b;
+  } else {
+    return a;
+  }
+
+}
+
+int g(int a, int b) {
+  
+  if (a < 0) {
+    return a - b;
+  } else {
+    return a;
+  }
+
+}
+
+int main()
+{
+  int x = 1;
+  int y = 2;
+
+  int (*h) (int, int) = &f;
+
+  int c = rand();
+  if (c) {
+    h = &g;
+  }
+
+  int z = h(x, y);
+
+  return z;
+}
+
+// no warnings here, since we cannot determine which function is called and y is used if h evaluates to f, so we have to assume that y is used
\ No newline at end of file
diff --git a/tests/regression/99-tutorials/10-function_call_complex_attributes.c b/tests/regression/99-tutorials/10-function_call_complex_attributes.c
new file mode 100644
index 0000000000..a838d779ce
--- /dev/null
+++ b/tests/regression/99-tutorials/10-function_call_complex_attributes.c
@@ -0,0 +1,25 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+int f(int a, int b) {
+  
+  if (a > 0) {
+    return a + b;
+  } else {
+    return a;
+  }
+
+}
+
+
+int main()
+{
+  int x = 1;
+  int y = 2;
+
+  int z = f(x + (y * y), 0);
+
+  return z;
+}
+
+// now warnings here. Both variables are relevant as they are used in an expression passed to a live parameter of the function call.
\ No newline at end of file
diff --git a/tests/regression/99-tutorials/11-function_call_return_val_mem.c b/tests/regression/99-tutorials/11-function_call_return_val_mem.c
new file mode 100644
index 0000000000..0bb813110f
--- /dev/null
+++ b/tests/regression/99-tutorials/11-function_call_return_val_mem.c
@@ -0,0 +1,24 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+int f(int a, int b) {
+  
+  if (a > 0) {
+    return a + b;
+  } else {
+    return a;
+  }
+
+}
+
+int main()
+{
+  int i = 1;
+  int x = -1;
+  int y = 2;
+  int *p = malloc(sizeof(int) * i);
+
+  p[0] = f(x, y);
+
+  return x;
+}
diff --git a/tests/regression/99-tutorials/12-memory_write_in_call.c b/tests/regression/99-tutorials/12-memory_write_in_call.c
new file mode 100644
index 0000000000..a6eeef997d
--- /dev/null
+++ b/tests/regression/99-tutorials/12-memory_write_in_call.c
@@ -0,0 +1,18 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+int f(int a, int* b) {
+  b[0] = a ;
+  return 0;
+}
+
+
+int main()
+{
+  int x = 1;
+  int *p = malloc(sizeof(int));
+
+  f(x, p);
+
+  return x;
+}
diff --git a/tests/regression/99-tutorials/13-pointer_used.c b/tests/regression/99-tutorials/13-pointer_used.c
new file mode 100644
index 0000000000..e40d102982
--- /dev/null
+++ b/tests/regression/99-tutorials/13-pointer_used.c
@@ -0,0 +1,19 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+#include <stdlib.h>
+
+
+int main()
+{
+  int x = 1;
+  int y = 2;
+
+  int *p = &x;
+
+  *p = 3; // x is now 3 and should not be live before this point anymore
+  int z = 2 * (*p);
+
+  return z;
+}
+
+/* This only works if we assume that if the query MayPointTo returns a single variable, then this variable is definietely the one pointed to.
+ */
\ No newline at end of file
diff --git a/tests/regression/99-tutorials/14-motivating_example.c b/tests/regression/99-tutorials/14-motivating_example.c
new file mode 100644
index 0000000000..d3f1196972
--- /dev/null
+++ b/tests/regression/99-tutorials/14-motivating_example.c
@@ -0,0 +1,31 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int f(int a, int b) 
+{
+  return a + b;
+}
+
+int g(int a, int b) 
+{ 
+  if (a > 0) {
+    return a - b;
+  } else {
+    return a;
+  }
+}
+
+int main()
+{
+  int x = 1;
+  int y = 2;
+  int *c = &x;
+  int (*h) (int, int) = &f;
+  
+  if (*c) {
+    h = &g;
+  }
+
+  *c = 0;
+  int z = h(x, y);
+  return z;
+}
diff --git a/tests/regression/99-tutorials/15-same_proc_different_results.c b/tests/regression/99-tutorials/15-same_proc_different_results.c
new file mode 100644
index 0000000000..4967a2c1b1
--- /dev/null
+++ b/tests/regression/99-tutorials/15-same_proc_different_results.c
@@ -0,0 +1,24 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int f(int a) 
+{
+  int b = 3; // no warning, as b is used in one call of f
+
+  if (a < 5) {
+    return a + b;
+  } else {
+    return a;
+  }
+}
+
+int main()
+{
+  int x = 0;
+
+  int u = f (x);
+
+  x = 10;
+
+  int v = f (x); 
+  return u + v;
+}
diff --git a/tests/regression/99-tutorials/16-global_variables.c b/tests/regression/99-tutorials/16-global_variables.c
new file mode 100644
index 0000000000..c26763d2d8
--- /dev/null
+++ b/tests/regression/99-tutorials/16-global_variables.c
@@ -0,0 +1,14 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+
+int x = 0;
+
+int f() 
+{
+  x ++;
+}
+
+int main()
+{
+  f();
+  return 0;
+}
diff --git a/tests/regression/99-tutorials/17-global_func_pointer_mod.c b/tests/regression/99-tutorials/17-global_func_pointer_mod.c
new file mode 100644
index 0000000000..b33f06422a
--- /dev/null
+++ b/tests/regression/99-tutorials/17-global_func_pointer_mod.c
@@ -0,0 +1,23 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+int (*h) (int);
+
+int g(int a) 
+{
+  return 0;
+}
+
+int f(int a) 
+{
+  h = &g;
+  return a;
+}
+
+int main()
+{
+  int x = 1;
+  h = &f;
+
+  int y = h(x);
+
+  return y;
+}
diff --git a/tests/regression/99-tutorials/18-pointer_to_partial_obj.c b/tests/regression/99-tutorials/18-pointer_to_partial_obj.c
new file mode 100644
index 0000000000..eb63006c90
--- /dev/null
+++ b/tests/regression/99-tutorials/18-pointer_to_partial_obj.c
@@ -0,0 +1,8 @@
+// SKIP TERM PARAM: --enable ana.wp_run 
+int main()
+{
+  int x[] = {1, 2, 3};
+  x [0] = 0;
+
+  return x[1];
+}
diff --git a/tests/regression/99-tutorials/19-struct_partial_update.c b/tests/regression/99-tutorials/19-struct_partial_update.c
new file mode 100644
index 0000000000..69c14d3c46
--- /dev/null
+++ b/tests/regression/99-tutorials/19-struct_partial_update.c
@@ -0,0 +1,14 @@
+// SKIP TERM PARAM: --enable ana.wp_run
+
+struct Pair {
+  int a;
+  int b;
+};
+
+int main()
+{
+  struct Pair p;
+  p.b = 42; 
+  p.a = 1; 
+  return p.b;
+}
diff --git a/tests/regression/99-tutorials/20-struct_ptr_partial_update.c b/tests/regression/99-tutorials/20-struct_ptr_partial_update.c
new file mode 100644
index 0000000000..d916c19d60
--- /dev/null
+++ b/tests/regression/99-tutorials/20-struct_ptr_partial_update.c
@@ -0,0 +1,17 @@
+// SKIP TERM PARAM: --enable ana.wp_run
+
+struct Pair {
+  int a;
+  int b;
+};
+
+int main()
+{
+  struct Pair p;
+  struct Pair *pp = &p;
+
+  pp->b = 42;
+  pp->a = 1;
+
+  return p.b;
+}
diff --git a/xslt/node.xsl b/xslt/node.xsl
index bb1ddcabfd..7d580adc79 100644
--- a/xslt/node.xsl
+++ b/xslt/node.xsl
@@ -101,6 +101,27 @@
     </xsl:choose>
   </xsl:template>
 
+  <xsl:template match="wp_path">
+    <xsl:choose>
+      <xsl:when test="analysis//value">
+        <div class="toggle">
+          <span>wp_path:</span>
+          <div>
+            <xsl:apply-templates select="analysis" />
+          </div>
+        </div>
+      </xsl:when>
+      <xsl:otherwise>
+        <div class="nontoggle">
+          <span>wp_path:</span>
+          <span>
+            <xsl:apply-templates select="analysis" />
+          </span>
+        </div>
+      </xsl:otherwise>
+    </xsl:choose>
+  </xsl:template>
+
   <xsl:template match="call">
     <a target="_top" class="node-wrap">
         <xsl:attribute name="href">../frame.html?file=<xsl:value-of select="@file"/>&amp;fun=<xsl:value-of select="@fun"/>&amp;node=<xsl:value-of select="@id" /></xsl:attribute>
@@ -118,6 +139,7 @@
       </div>
     </div>
     <xsl:apply-templates select="path" />
+    <xsl:apply-templates select="wp_path" />
   </xsl:template>
 
 
diff --git a/xy_easyprog.c b/xy_easyprog.c
new file mode 100644
index 0000000000..af09bd62e8
--- /dev/null
+++ b/xy_easyprog.c
@@ -0,0 +1,48 @@
+#include <stdlib.h>
+
+int f(int x, int y) {
+    int i = 2;
+    
+    if (x > 0) {
+        i = i + 2;
+        return i + y;
+    } else {
+        i = i + 3;
+        return i + x;
+    }
+}
+
+int g (int x, int y) {
+    int i = 2;
+    
+    if (x > 0) {
+        i = i + 2;
+        return i;
+    } else {
+        i = i + 3;
+        return i + x;
+    }
+}
+
+
+int main() {
+    int a = 0;
+    int c = 3;
+
+    int rand;
+
+    int (*h)(int, int); // function pointer to f
+    h = &f;
+
+    // if (rand) {
+    //     h = &g;
+    // }
+    int d = f (a, c);
+    
+    // a = -100;
+
+    // int b = (*h)(a, c);
+    return d;
+}
+
+//git diff --cached --name-only --diff-filter=ACM | grep -E '\.(ml|mli)$' | xargs -I {} ocp-indent -i {}
\ No newline at end of file