diff --git a/README.md b/README.md
index 4d97baa842..090d354203 100644
--- a/README.md
+++ b/README.md
@@ -24,7 +24,7 @@ For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs
 6. _Optional:_ See [`scripts/bash-completion.sh`](./scripts/bash-completion.sh) for setting up bash completion for Goblint arguments.
 
 ### MacOS
-1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
+1. Install GCC with `brew install gcc grep` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
 3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
 
diff --git a/docs/artifact-descriptions/vmcai24.md b/docs/artifact-descriptions/vmcai24.md
new file mode 100644
index 0000000000..860ef6c9fd
--- /dev/null
+++ b/docs/artifact-descriptions/vmcai24.md
@@ -0,0 +1,83 @@
+# VMCAI '24 Artifact Description
+## Correctness Witness Validation by Abstract Interpretation
+
+This is the artifact description for our [VMCAI '24 paper "Correctness Witness Validation by Abstract Interpretation"](https://doi.org/10.1007/978-3-031-50524-9_4).
+The artifact is available on [Zenodo](https://doi.org/10.5281/zenodo.8253000).
+
+This artifact contains everything mentioned in the evaluation section of the paper: Goblint implementation, scripts, benchmarks, manual witnesses and other tools.
+
+**The description here is provided for convenience and not maintained.**
+The artifact is based on [Goblint at `vmcai24` git tag](https://github.com/goblint/analyzer/releases/tag/vmcai24) and [Goblint benchmarks at `vmcai24` git tag](https://github.com/goblint/bench/releases/tag/vmcai24).
+
+## Requirements
+* [VirtualBox](https://www.virtualbox.org/).
+* 2 CPU cores.
+* 8 GB RAM.
+* 7 GB disk space.
+* ~45min.
+
+## Layout
+* `README.md`/`README.pdf` — this file.
+* `LICENSE`.
+* `unassume.ova` — VirtualBox virtual machine.
+
+    In `/home/vagrant` contains:
+
+    * `goblint/` ­— Goblint with unassume support, including source code.
+    * `CPAchecker-2.2-unix/` — CPAchecker from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
+    * `UAutomizer-linux/` — Ultimate Automizer from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
+    * `eval-prec/` — precision evaluation (script, benchmarks, manual witnesses).
+    * `eval-perf/` — performance evaluation (script, benchmarks, manual witnesses).
+    * `results/` — results (initially empty).
+
+* `results/` — evaluation results tables with data used for the paper.
+
+## Reproduction
+1. Import the virtual machine into VirtualBox.
+2. Start the virtual machine and log in with username "vagrant" (not "Ubuntu"!) and password "vagrant".
+3. Right click on the desktop and open Applications → Accessories → Terminal Emulator.
+
+### Precision evaluation
+1. Run `./eval-prec/run.sh` in the terminal emulator. This takes ~42min.
+2. Run `firefox results/eval-prec/table-generator.table.html` to view the results.
+
+    The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
+
+    1. Goblint w/o witness (true means verified).
+    2. Goblint w/ manual witness (true means witness validated).
+    3. Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
+    4. Goblint w/ witness from CPAchecker (true means witness validated).
+    5. Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
+    6. Goblint w/ witness from UAutomizer (true means witness validated).
+
+   Table 1 in the paper presents these results, except the rows are likely in a different order.
+
+### Performance evaluation
+1. Run `./eval-perf/run.sh` in the terminal emulator. This takes ~30s.
+2. Run `firefox results/eval-perf/table-generator.table.html` to view the results.
+
+    The HTML table contains the following relevant columns (others can be ignored):
+
+    1. Goblint w/o witness, evals.
+    2. Goblint w/o witness, cputime.
+    3. Goblint w/ manual witness, evals.
+    4. Goblint w/ manual witness, cputime.
+
+   Table 2 in the paper presents these results, except the rows are likely in a different order.
+
+
+## Goblint implementation
+[Goblint](https://github.com/goblint/analyzer) is an open source static analysis framework for C.
+Goblint itself is written in OCaml.
+Being open source, it allows existing implementations of analyses and abstract domains to be reused and modified.
+As a framework, it also allows new ones to be easily added.
+For more details, refer to the linked GitHub repository and related documentation.
+
+Key parts of the code related to this paper are the following:
+
+1. `src/analyses/unassumeAnalysis.ml`: analysis, which emits unassume operation events to other analyses for YAML-witness–guided verification.
+2. `src/analyses/base.ml` lines 2551–2641: propagating unassume for non-relational domains of the `base` analysis.
+3. `src/analyses/apron/relationAnalysis.apron.ml` lines 668–693: strengthening-based dual-narrowing unassume for relational Apron domains of the `apron` analysis.
+4. `src/cdomains/apron/apronDomain.apron.ml` lines 625–679: strengthening operator used for dual-narrowing of Apron domains.
+5. `src/util/wideningTokens.ml`: analysis lifter that adds widening tokens for delaying widenings from unassuming.
+6. `src/witness/yamlWitness.ml` lines 398–683: YAML witness validation.
diff --git a/mkdocs.yml b/mkdocs.yml
index 428e28078d..8064703c12 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -39,3 +39,4 @@ nav:
   - '📦 Artifact descriptions':
     - "🇸 SAS '21": artifact-descriptions/sas21.md
     - "🇪 ESOP '23": artifact-descriptions/esop23.md
+    - "🇻 VMCAI '24": artifact-descriptions/vmcai24.md
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index e572755930..c9f8cd750a 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -158,13 +158,14 @@ struct
         {st' with rel = rel''}
       )
     | (Mem v, NoOffset) ->
-      begin match ask.f (Queries.MayPointTo v) with
-        | ad when Queries.AD.is_top ad -> st
-        | ad ->
-          let mvals = Queries.AD.to_mval ad in
-          let ass' = List.map (fun mval -> assign_to_global_wrapper ask getg sideg st (ValueDomain.Addr.Mval.to_cil mval) f) mvals in
-          List.fold_right D.join ass' (D.bot ())
-      end
+      let ad = ask.f (Queries.MayPointTo v) in
+      Queries.AD.fold (fun addr acc ->
+          match addr with
+          | ValueDomain.Addr.Addr mval ->
+            D.join acc (assign_to_global_wrapper ask getg sideg st (ValueDomain.Addr.Mval.to_cil mval) f)
+          | UnknownPtr | NullPtr | StrPtr _ ->
+            D.join acc st (* Ignore assign *)
+        ) ad (D.bot ())
     (* Ignoring all other assigns *)
     | _ ->
       st
@@ -381,6 +382,8 @@ struct
     if M.tracing then M.tracel "combine" "relation f: %a\n" CilType.Varinfo.pretty f.svar;
     if M.tracing then M.tracel "combine" "relation formals: %a\n" (d_list "," CilType.Varinfo.pretty) f.sformals;
     if M.tracing then M.tracel "combine" "relation args: %a\n" (d_list "," d_exp) args;
+    if M.tracing then M.tracel "combine" "relation st: %a\n" D.pretty st;
+    if M.tracing then M.tracel "combine" "relation fun_st: %a\n" D.pretty fun_st;
     let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
     let arg_substitutes =
       let filter_actuals (x,e) =
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index b945f34f9d..ab457ed0e5 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -242,7 +242,7 @@ struct
     | _ -> false
 
   (* Evaluate binop for two abstract values: *)
-  let evalbinop_base (a: Q.ask) (st: store) (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value =
+  let evalbinop_base ~ctx (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value =
     if M.tracing then M.tracel "eval" "evalbinop %a %a %a\n" d_binop op VD.pretty a1 VD.pretty a2;
     (* We define a conversion function for the easy cases when we can just use
      * the integer domain operations. *)
@@ -339,7 +339,7 @@ struct
             let ax = AD.choose x in
             let ay = AD.choose y in
             let handle_address_is_multiple addr = begin match Addr.to_var addr with
-              | Some v when a.f (Q.IsMultiple v) ->
+              | Some v when ctx.ask (Q.IsMultiple v) ->
                 if M.tracing then M.tracel "addr" "IsMultiple %a\n" CilType.Varinfo.pretty v;
                 None
               | _ ->
@@ -436,9 +436,10 @@ struct
   let publish_all ctx reason =
     ignore (sync' reason ctx)
 
-  let get_var (a: Q.ask) (gs: glob_fun) (st: store) (x: varinfo): value =
-    if (!earlyglobs || ThreadFlag.has_ever_been_multi a) && is_global a x then
-      Priv.read_global a (priv_getg gs) st x
+  let get_var ~ctx (st: store) (x: varinfo): value =
+    let ask = Analyses.ask_of_ctx ctx in
+    if (!earlyglobs || ThreadFlag.has_ever_been_multi ask) && is_global ask x then
+      Priv.read_global ask (priv_getg ctx.global) st x
     else begin
       if M.tracing then M.tracec "get" "Singlethreaded mode.\n";
       CPA.find x st.cpa
@@ -448,7 +449,7 @@ struct
    *  adding proper dependencies.
    *  For the exp argument it is always ok to put None. This means not using precise information about
    *  which part of an array is involved.  *)
-  let rec get ?(top=VD.top ()) ?(full=false) a (gs: glob_fun) (st: store) (addrs:address) (exp:exp option): value =
+  let rec get ~ctx ?(top=VD.top ()) ?(full=false) (st: store) (addrs:address) (exp:exp option): value =
     let at = AD.type_of addrs in
     let firstvar = if M.tracing then match AD.to_var_may addrs with [] -> "" | x :: _ -> x.vname else "" in
     if M.tracing then M.traceli "get" ~var:firstvar "Address: %a\nState: %a\n" AD.pretty addrs CPA.pretty st.cpa;
@@ -456,8 +457,8 @@ struct
     let res =
       let f_addr (x, offs) =
         (* get hold of the variable value, either from local or global state *)
-        let var = get_var a gs st x in
-        let v = VD.eval_offset (Queries.to_value_domain_ask a) (fun x -> get a gs st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
+        let var = get_var ~ctx st x in
+        let v = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (fun x -> get ~ctx st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
         if M.tracing then M.tracec "get" "var = %a, %a = %a\n" VD.pretty var AD.pretty (AD.of_mval (x, offs)) VD.pretty v;
         if full then var else match v with
           | Blob (c,s,_) -> c
@@ -505,24 +506,24 @@ struct
     in
     List.fold_right f vals []
 
-  let rec reachable_from_value (ask: Q.ask) (gs:glob_fun) st (value: value) (t: typ) (description: string)  =
+  let rec reachable_from_value ask (value: value) (t: typ) (description: string)  =
     let empty = AD.empty () in
     if M.tracing then M.trace "reachability" "Checking value %a\n" VD.pretty value;
     match value with
     | Top ->
-      if VD.is_immediate_type t then () else M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty
+      if not (VD.is_immediate_type t) then M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty
     | Bot -> (*M.debug ~category:Analyzer "A bottom value when computing reachable addresses!";*) empty
     | Address adrs when AD.is_top adrs ->
       M.info ~category:Unsound "Unknown address in %s has escaped." description; AD.remove Addr.NullPtr adrs (* return known addresses still to be a bit more sane (but still unsound) *)
     (* The main thing is to track where pointers go: *)
     | Address adrs -> AD.remove Addr.NullPtr adrs
     (* Unions are easy, I just ingore the type info. *)
-    | Union (f,e) -> reachable_from_value ask gs st e t description
+    | Union (f,e) -> reachable_from_value ask e t description
     (* For arrays, we ask to read from an unknown index, this will cause it
      * join all its values. *)
-    | Array a -> reachable_from_value ask gs st (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description
-    | Blob (e,_,_) -> reachable_from_value ask gs st e t description
-    | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty
+    | Array a -> reachable_from_value ask (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description
+    | Blob (e,_,_) -> reachable_from_value ask e t description
+    | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask v t description) acc) s empty
     | Int _ -> empty
     | Float _ -> empty
     | MutexAttr _ -> empty
@@ -533,9 +534,9 @@ struct
   (* Get the list of addresses accessable immediately from a given address, thus
    * all pointers within a structure should be considered, but we don't follow
    * pointers. We return a flattend representation, thus simply an address (set). *)
-  let reachable_from_address (ask: Q.ask) (gs:glob_fun) st (adr: address): address =
+  let reachable_from_address ~ctx st (adr: address): address =
     if M.tracing then M.tracei "reachability" "Checking for %a\n" AD.pretty adr;
-    let res = reachable_from_value ask gs st (get ask gs st adr None) (AD.type_of adr) (AD.show adr) in
+    let res = reachable_from_value (Analyses.ask_of_ctx ctx) (get ~ctx st adr None) (AD.type_of adr) (AD.show adr) in
     if M.tracing then M.traceu "reachability" "Reachable addresses: %a\n" AD.pretty res;
     res
 
@@ -543,7 +544,7 @@ struct
    * This section is very confusing, because I use the same construct, a set of
    * addresses, as both AD elements abstracting individual (ambiguous) addresses
    * and the workset of visited addresses. *)
-  let reachable_vars (ask: Q.ask) (args: address list) (gs:glob_fun) (st: store): address list =
+  let reachable_vars ~ctx (st: store) (args: address list): address list =
     if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!\n" (d_list ", " AD.pretty) args;
     let empty = AD.empty () in
     (* We begin looking at the parameters: *)
@@ -556,7 +557,7 @@ struct
       (* ok, let's visit all the variables in the workset and collect the new variables *)
       let visit_and_collect var (acc: address): address =
         let var = AD.singleton var in (* Very bad hack! Pathetic really! *)
-        AD.union (reachable_from_address ask gs st var) acc in
+        AD.union (reachable_from_address ~ctx st var) acc in
       let collected = AD.fold visit_and_collect !workset empty in
       (* And here we remove the already visited variables *)
       workset := AD.diff collected !visited
@@ -565,7 +566,7 @@ struct
     if M.tracing then M.traceu "reachability" "All reachable vars: %a\n" AD.pretty !visited;
     List.map AD.singleton (AD.elements !visited)
 
-  let reachable_vars ask args gs st = Timing.wrap "reachability" (reachable_vars ask args gs) st
+  let reachable_vars ~ctx st args = Timing.wrap "reachability" (reachable_vars ~ctx st) args
 
   let drop_non_ptrs (st:CPA.t) : CPA.t =
     if CPA.is_top st then st else
@@ -652,7 +653,7 @@ struct
         | JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
         | Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *)
       in
-      reachable_from_value (get (Analyses.ask_of_ctx ctx) ctx.global ctx.local adr None)
+      reachable_from_value (get ~ctx ctx.local adr None)
     in
     let visited = ref empty in
     let work = ref ps in
@@ -672,14 +673,14 @@ struct
     !collected
 
   (* The evaluation function as mutually recursive eval_lv & eval_rv *)
-  let rec eval_rv (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value =
+  let rec eval_rv ~(ctx: _ ctx) (st: store) (exp:exp): value =
     if M.tracing then M.traceli "evalint" "base eval_rv %a\n" d_exp exp;
     let r =
       (* we have a special expression that should evaluate to top ... *)
       if exp = MyCFG.unknown_exp then
         VD.top ()
       else
-        eval_rv_ask_evalint a gs st exp
+        eval_rv_ask_evalint ~ctx st exp
     in
     if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a\n" d_exp exp VD.pretty r;
     r
@@ -688,14 +689,14 @@ struct
       Base itself also answers EvalInt, so recursion goes indirectly through queries.
       This allows every subexpression to also meet more precise value from other analyses.
       Non-integer expression just delegate to next eval_rv function. *)
-  and eval_rv_ask_evalint a gs st exp =
-    let eval_next () = eval_rv_no_ask_evalint a gs st exp in
+  and eval_rv_ask_evalint ~ctx st exp =
+    let eval_next () = eval_rv_no_ask_evalint ~ctx st exp in
     if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a\n" d_exp exp;
     let r:value =
       match Cilfacade.typeOf exp with
       | typ when Cil.isIntegralType typ && not (Cil.isConstant exp) -> (* don't EvalInt integer constants, base can do them precisely itself *)
         if M.tracing then M.traceli "evalint" "base ask EvalInt %a\n" d_exp exp;
-        let a = a.f (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *)
+        let a = ctx.ask (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *)
         if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a\n" d_exp exp Queries.ID.pretty a;
         begin match a with
           | `Bot -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *)
@@ -712,24 +713,24 @@ struct
   (** Evaluate expression without EvalInt query on outermost expression.
       This is used by base responding to EvalInt to immediately directly avoid EvalInt query cycle, which would return top.
       Recursive [eval_rv] calls on subexpressions still go through [eval_rv_ask_evalint]. *)
-  and eval_rv_no_ask_evalint a gs st exp =
-    eval_rv_base a gs st exp (* just as alias, so query doesn't weirdly have to call eval_rv_base *)
+  and eval_rv_no_ask_evalint ~ctx st exp =
+    eval_rv_base ~ctx st exp (* just as alias, so query doesn't weirdly have to call eval_rv_base *)
 
-  and eval_rv_back_up a gs st exp =
+  and eval_rv_back_up ~ctx st exp =
     if get_bool "ana.base.eval.deep-query" then
-      eval_rv a gs st exp
+      eval_rv ~ctx st exp
     else (
       (* duplicate unknown_exp check from eval_rv since we're bypassing it now *)
       if exp = MyCFG.unknown_exp then
         VD.top ()
       else
-        eval_rv_base a gs st exp (* bypass all queries *)
+        eval_rv_base ~ctx st exp (* bypass all queries *)
     )
 
   (** Evaluate expression structurally by base.
       This handles constants directly and variables using CPA.
       Subexpressions delegate to [eval_rv], which may use queries on them. *)
-  and eval_rv_base (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value =
+  and eval_rv_base ~ctx (st: store) (exp:exp): value =
     let eval_rv = eval_rv_back_up in
     if M.tracing then M.traceli "evalint" "base eval_rv_base %a\n" d_exp exp;
     let binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 =
@@ -751,7 +752,7 @@ struct
       match constFold true exp with
       (* Integer literals *)
       (* seems like constFold already converts CChr to CInt *)
-      | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
+      | Const (CChr x) -> eval_rv ~ctx st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
       | Const (CInt (num,ikind,str)) ->
         (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Z.to_string num) d_ikind ikind x | None -> ());
         Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
@@ -767,21 +768,21 @@ struct
       | Const _ -> VD.top ()
       (* Variables and address expressions *)
       | Lval lv ->
-        eval_rv_base_lval ~eval_lv a gs st exp lv
+        eval_rv_base_lval ~eval_lv ~ctx st exp lv
       (* Binary operators *)
       (* Eq/Ne when both values are equal and casted to the same type *)
       | BinOp ((Eq | Ne) as op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
-        let a1 = eval_rv a gs st e1 in
-        let a2 = eval_rv a gs st e2 in
+        let a1 = eval_rv ~ctx st e1 in
+        let a2 = eval_rv ~ctx st e2 in
         let extra_is_safe =
-          match evalbinop_base a st op t1 a1 t2 a2 typ with
+          match evalbinop_base ~ctx op t1 a1 t2 a2 typ with
           | Int i -> ID.to_bool i = Some true
           | _
           | exception IntDomain.IncompatibleIKinds _ -> false
         in
         let (e1, e2) = binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 in
         (* re-evaluate e1 and e2 in evalbinop because might be with cast *)
-        evalbinop a gs st op ~e1 ~t1 ~e2 ~t2 typ
+        evalbinop ~ctx st op ~e1 ~t1 ~e2 ~t2 typ
       | BinOp (LOr, e1, e2, typ) as exp ->
         let open GobOption.Syntax in
         (* split nested LOr Eqs to equality pairs, if possible *)
@@ -814,8 +815,8 @@ struct
         let eqs_value: value option =
           let* eqs = split exp in
           let* (e, es) = find_common eqs in
-          let v = eval_rv a gs st e in (* value of common exp *)
-          let vs = List.map (eval_rv a gs st) es in (* values of other sides *)
+          let v = eval_rv ~ctx st e in (* value of common exp *)
+          let vs = List.map (eval_rv ~ctx st) es in (* values of other sides *)
           let ik = Cilfacade.get_ikind typ in
           match v with
           | Address a ->
@@ -857,25 +858,25 @@ struct
         in
         begin match eqs_value with
           | Some x -> x
-          | None -> evalbinop a gs st LOr ~e1 ~e2 typ (* fallback to general case *)
+          | None -> evalbinop ~ctx st LOr ~e1 ~e2 typ (* fallback to general case *)
         end
       | BinOp (op,e1,e2,typ) ->
-        evalbinop a gs st op ~e1 ~e2 typ
+        evalbinop ~ctx st op ~e1 ~e2 typ
       (* Unary operators *)
       | UnOp (op,arg1,typ) ->
-        let a1 = eval_rv a gs st arg1 in
+        let a1 = eval_rv ~ctx st arg1 in
         evalunop op typ a1
       (* The &-operator: we create the address abstract element *)
-      | AddrOf lval -> Address (eval_lv a gs st lval)
+      | AddrOf lval -> Address (eval_lv ~ctx st lval)
       (* CIL's very nice implicit conversion of an array name [a] to a pointer
         * to its first element [&a[0]]. *)
       | StartOf lval ->
         let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
         let array_start = add_offset_varinfo array_ofs in
-        Address (AD.map array_start (eval_lv a gs st lval))
-      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv a gs st (Const (CStr (x,e))) (* TODO safe? *)
+        Address (AD.map array_start (eval_lv ~ctx st lval))
+      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE  (t, exp) ->
-        let v = eval_rv a gs st exp in
+        let v = eval_rv ~ctx st exp in
         VD.cast ~torg:(Cilfacade.typeOf exp) t v
       | SizeOf _
       | Real _
@@ -891,10 +892,10 @@ struct
     if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a\n" d_exp exp VD.pretty r;
     r
 
-  and eval_rv_base_lval ~eval_lv (a: Q.ask) (gs:glob_fun) (st: store) (exp: exp) (lv: lval): value =
+  and eval_rv_base_lval ~eval_lv ~ctx (st: store) (exp: exp) (lv: lval): value =
     match lv with
-    | (Var v, ofs) -> get a gs st (eval_lv a gs st (Var v, ofs)) (Some exp)
-    (*| Lval (Mem e, ofs) -> get a gs st (eval_lv a gs st (Mem e, ofs)) *)
+    | (Var v, ofs) -> get ~ctx st (eval_lv ~ctx st (Var v, ofs)) (Some exp)
+    (* | Lval (Mem e, ofs) -> get ~ctx st (eval_lv ~ctx (Mem e, ofs)) *)
     | (Mem e, ofs) ->
       (*M.tracel "cast" "Deref: lval: %a\n" d_plainlval lv;*)
       let rec contains_vla (t:typ) = match t with
@@ -906,7 +907,7 @@ struct
       in
       let b = Mem e, NoOffset in (* base pointer *)
       let t = Cilfacade.typeOfLval b in (* static type of base *)
-      let p = eval_lv a gs st b in (* abstract base addresses *)
+      let p = eval_lv ~ctx st b in (* abstract base addresses *)
       (* pre VLA: *)
       (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *)
       let cast_ok a =
@@ -938,35 +939,35 @@ struct
       let lookup_with_offs addr =
         let v = (* abstract base value *)
           if cast_ok addr then
-            get ~top:(VD.top_value t) a gs st (AD.singleton addr) (Some exp)  (* downcasts are safe *)
+            get ~ctx ~top:(VD.top_value t) st (AD.singleton addr) (Some exp)  (* downcasts are safe *)
           else
             VD.top () (* upcasts not! *)
         in
         let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *)
         if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v';
-        let v' = VD.eval_offset (Queries.to_value_domain_ask a) (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *)
+        let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (fun x -> get ~ctx st x (Some exp)) v' (convert_offset ~ctx st ofs) (Some exp) None t in (* handle offset *)
         v'
       in
       AD.fold (fun a acc -> VD.join acc (lookup_with_offs a)) p (VD.bot ())
 
-  and evalbinop (a: Q.ask) (gs:glob_fun) (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value =
-    evalbinop_mustbeequal a gs st op ~e1 ?t1 ~e2 ?t2 t
+  and evalbinop ~ctx (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value =
+    evalbinop_mustbeequal ~ctx st op ~e1 ?t1 ~e2 ?t2 t
 
   (** Evaluate BinOp using MustBeEqual query as fallback. *)
-  and evalbinop_mustbeequal (a: Q.ask) (gs:glob_fun) (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value =
+  and evalbinop_mustbeequal ~ctx (st: store) (op: binop) ~(e1:exp) ?(t1:typ option) ~(e2:exp) ?(t2:typ option) (t:typ): value =
     (* Evaluate structurally using base at first. *)
-    let a1 = eval_rv a gs st e1 in
-    let a2 = eval_rv a gs st e2 in
+    let a1 = eval_rv ~ctx st e1 in
+    let a2 = eval_rv ~ctx st e2 in
     let t1 = Option.default_delayed (fun () -> Cilfacade.typeOf e1) t1 in
     let t2 = Option.default_delayed (fun () -> Cilfacade.typeOf e2) t2 in
-    let r = evalbinop_base a st op t1 a1 t2 a2 t in
+    let r = evalbinop_base ~ctx op t1 a1 t2 a2 t in
     if Cil.isIntegralType t then (
       match r with
       | Int i when ID.to_int i <> None -> r (* Avoid fallback, cannot become any more precise. *)
       | _ ->
         (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *)
         let must_be_equal () =
-          let r = Q.must_be_equal a e1 e2 in
+          let r = Q.must_be_equal (Analyses.ask_of_ctx ctx) e1 e2 in
           if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b\n" d_exp e1 d_exp e2 r;
           r
         in
@@ -995,48 +996,48 @@ struct
 
   (* A hackish evaluation of expressions that should immediately yield an
    * address, e.g. when calling functions. *)
-  and eval_fv a (gs:glob_fun) st (exp:exp): AD.t =
+  and eval_fv ~ctx st (exp:exp): AD.t =
     match exp with
-    | Lval lval -> eval_lv a gs st lval
-    | _ -> eval_tv a gs st exp
+    | Lval lval -> eval_lv ~ctx st lval
+    | _ -> eval_tv ~ctx st exp
   (* Used also for thread creation: *)
-  and eval_tv a (gs:glob_fun) st (exp:exp): AD.t =
-    match (eval_rv a gs st exp) with
+  and eval_tv ~ctx st (exp:exp): AD.t =
+    match eval_rv ~ctx st exp with
     | Address x -> x
     | _          -> failwith "Problems evaluating expression to function calls!"
-  and eval_int a gs st exp =
-    match eval_rv a gs st exp with
+  and eval_int ~ctx st exp =
+    match eval_rv ~ctx st exp with
     | Int x -> x
     | _ -> ID.top_of (Cilfacade.get_ikind_exp exp)
   (* A function to convert the offset to our abstract representation of
    * offsets, i.e.  evaluate the index expression to the integer domain. *)
-  and convert_offset a (gs:glob_fun) (st: store) (ofs: offset) =
+  and convert_offset ~ctx (st: store) (ofs: offset) =
     let eval_rv = eval_rv_back_up in
     match ofs with
     | NoOffset -> `NoOffset
-    | Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs)
+    | Field (fld, ofs) -> `Field (fld, convert_offset ~ctx st ofs)
     | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
-      `Index (IdxDom.top (), convert_offset a gs st ofs)
+      `Index (IdxDom.top (), convert_offset ~ctx st ofs)
     | Index (exp, ofs) ->
-      match eval_rv a gs st exp with
-      | Int i -> `Index (iDtoIdx i, convert_offset a gs st ofs)
-      | Address add -> `Index (AD.to_int add, convert_offset a gs st ofs)
-      | Top   -> `Index (IdxDom.top (), convert_offset a gs st ofs)
-      | Bot -> `Index (IdxDom.bot (), convert_offset a gs st ofs)
+      match eval_rv ~ctx st exp with
+      | Int i -> `Index (iDtoIdx i, convert_offset ~ctx st ofs)
+      | Address add -> `Index (AD.to_int add, convert_offset ~ctx st ofs)
+      | Top   -> `Index (IdxDom.top (), convert_offset ~ctx st ofs)
+      | Bot -> `Index (IdxDom.bot (), convert_offset ~ctx st ofs)
       | _ -> failwith "Index not an integer value"
   (* Evaluation of lvalues to our abstract address domain. *)
-  and eval_lv (a: Q.ask) (gs:glob_fun) st (lval:lval): AD.t =
+  and eval_lv ~ctx st (lval:lval): AD.t =
     let eval_rv = eval_rv_back_up in
     match lval with
     (* The simpler case with an explicit variable, e.g. for [x.field] we just
      * create the address { (x,field) } *)
     | Var x, ofs ->
-      AD.singleton (Addr.of_mval (x, convert_offset a gs st ofs))
+      AD.singleton (Addr.of_mval (x, convert_offset ~ctx st ofs))
     (* The more complicated case when [exp = & x.field] and we are asked to
      * evaluate [(\*exp).subfield]. We first evaluate [exp] to { (x,field) }
      * and then add the subfield to it: { (x,field.subfield) }. *)
     | Mem n, ofs -> begin
-        match (eval_rv a gs st n) with
+        match eval_rv ~ctx st n with
         | Address adr ->
           (
             if AD.is_null adr then (
@@ -1049,14 +1050,14 @@ struct
             );
             (* Warn if any of the addresses contains a non-local and non-global variable *)
             if AD.exists (function
-                | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v)
+                | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global (Analyses.ask_of_ctx ctx) v)
                 | _ -> false
               ) adr then (
               AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
               M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval
             )
           );
-          AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
+          AD.map (add_offset_varinfo (convert_offset ~ctx st ofs)) adr
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
           AD.unknown_ptr
@@ -1068,17 +1069,17 @@ struct
 
   (* run eval_rv from above, but change bot to top to be sound for programs with undefined behavior. *)
   (* Previously we only gave sound results for programs without undefined behavior, so yielding bot for accessing an uninitialized array was considered ok. Now only [invariant] can yield bot/Deadcode if the condition is known to be false but evaluating an expression should not be bot. *)
-  let eval_rv (a: Q.ask) (gs:glob_fun) (st: store) (exp:exp): value =
+  let eval_rv ~ctx (st: store) (exp:exp): value =
     try
-      let r = eval_rv a gs st exp in
+      let r = eval_rv ~ctx st exp in
       if M.tracing then M.tracel "eval" "eval_rv %a = %a\n" d_exp exp VD.pretty r;
       if VD.is_bot r then VD.top_value (Cilfacade.typeOf exp) else r
     with IntDomain.ArithmeticOnIntegerBot _ ->
       ValueDomain.Compound.top_value (Cilfacade.typeOf exp)
 
-  let query_evalint ask gs st e =
+  let query_evalint ~ctx st e =
     if M.tracing then M.traceli "evalint" "base query_evalint %a\n" d_exp e;
-    let r = match eval_rv_no_ask_evalint ask gs st e with
+    let r = match eval_rv_no_ask_evalint ~ctx st e with
       | Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
       | Bot   -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *)
       | Top   -> Queries.ID.top () (* some float computations cause top (57-float/01-base), but query result should then be unknown *)
@@ -1098,19 +1099,32 @@ struct
       if Queries.Set.mem anyq asked then
         Queries.Result.top q (* query cycle *)
       else (
-        let asked' = Queries.Set.add anyq asked in
         match q with
-        | EvalInt e -> query_evalint (ask asked') gs st e (* mimic EvalInt query since eval_rv needs it *)
+        | EvalInt e -> query_evalint ~ctx:(ctx' (Queries.Set.add anyq asked)) st e (* mimic EvalInt query since eval_rv needs it *)
         | _ -> Queries.Result.top q
       )
-    and ask asked = { Queries.f = fun (type a) (q: a Queries.t) -> query asked q } (* our version of ask *)
-    and gs = function `Left _ -> `Lifted1 (Priv.G.top ()) | `Right _ -> `Lifted2 (VD.top ()) in (* the expression is guaranteed to not contain globals *)
-    match (eval_rv (ask Queries.Set.empty) gs st exp) with
+    and gs = function `Left _ -> `Lifted1 (Priv.G.top ()) | `Right _ -> `Lifted2 (VD.top ()) (* the expression is guaranteed to not contain globals *)
+    and ctx' asked =
+      { ask = (fun (type a) (q: a Queries.t) -> query asked q)
+      ; emit   = (fun _ -> failwith "Cannot \"emit\" in base eval_exp context.")
+      ; node    = MyCFG.dummy_node
+      ; prev_node = MyCFG.dummy_node
+      ; control_context = (fun () -> ctx_failwith "Base eval_exp has no context.")
+      ; context = (fun () -> ctx_failwith "Base eval_exp has no context.")
+      ; edge    = MyCFG.Skip
+      ; local   = st
+      ; global  = gs
+      ; spawn   = (fun ?(multiple=false) _ -> failwith "Base eval_exp should never spawn threads. What is going on?")
+      ; split   = (fun _ -> failwith "Base eval_exp trying to split paths.")
+      ; sideg   = (fun g d -> failwith "Base eval_exp trying to side effect.")
+      }
+    in
+    match eval_rv ~ctx:(ctx' Queries.Set.empty) st exp with
     | Int x -> ValueDomain.ID.to_int x
     | _ -> None
 
   let eval_funvar ctx fval: Queries.AD.t =
-    let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
+    let fp = eval_fv ~ctx ctx.local fval in
     if AD.is_top fp then (
       if AD.cardinal fp = 1 then
         M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval
@@ -1121,14 +1135,14 @@ struct
 
   (** Evaluate expression as address.
       Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *)
-  let eval_rv_address ask gs st e =
+  let eval_rv_address ~ctx st e =
     (* no way to do eval_rv with expected type, so filter expression beforehand *)
     match Cilfacade.typeOf e with
     | t when Cil.isArithmeticType t -> (* definitely not address *)
       VD.top_value t
     | exception Cilfacade.TypeOfError _ (* something weird, might be address *)
     | _ ->
-      eval_rv ask gs st e
+      eval_rv ~ctx st e
 
   (* interpreter end *)
 
@@ -1147,7 +1161,7 @@ struct
     struct
       let context = context
       let scope = Node.find_fundec ctx.node
-      let find v = get_var ask ctx.global ctx.local v
+      let find v = get_var ~ctx ctx.local v
     end
     in
     let module I = ValueDomain.ValueInvariant (Arg) in
@@ -1220,11 +1234,11 @@ struct
     | Q.EvalFunvar e ->
       eval_funvar ctx e
     | Q.EvalJumpBuf e ->
-      begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+      begin match eval_rv_address ~ctx ctx.local e with
         | Address jmp_buf ->
           if AD.mem Addr.UnknownPtr jmp_buf then
             M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
-          begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
+          begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with
             | JmpBuf (x, copied) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
@@ -1241,15 +1255,15 @@ struct
           JmpBufDomain.JmpBufSet.top ()
       end
     | Q.EvalInt e ->
-      query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
+      query_evalint ~ctx ctx.local e
     | Q.EvalMutexAttr e -> begin
         let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in
-        match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv ~ctx ctx.local e with
         | MutexAttr a -> a
         | v -> MutexAttrDomain.top ()
       end
     | Q.EvalLength e -> begin
-        match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv_address ~ctx ctx.local e with
         | Address a ->
           let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in
           let lenOf = function
@@ -1264,9 +1278,9 @@ struct
         | _ -> Queries.Result.top q
       end
     | Q.EvalValue e ->
-      eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
+      eval_rv ~ctx ctx.local e
     | Q.BlobSize {exp = e; base_address = from_base_addr} -> begin
-        let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
+        let p = eval_rv_address ~ctx ctx.local e in
         (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *)
         match p with
         | Address a ->
@@ -1285,7 +1299,7 @@ struct
               else
                 a
             in
-            let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
+            let r = get ~ctx ~full:true ctx.local a None in
             (* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
             (match r with
              | Array a ->
@@ -1300,14 +1314,14 @@ struct
         | _ -> Queries.Result.top q
       end
     | Q.MayPointTo e -> begin
-        match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv_address ~ctx ctx.local e with
         | Address a -> a
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Int i -> AD.of_int i
         | _ -> Queries.Result.top q
       end
     | Q.EvalThread e -> begin
-        let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
+        let v = eval_rv ~ctx ctx.local e in
         (* ignore (Pretty.eprintf "evalthread %a (%a): %a" d_exp e d_plainexp e VD.pretty v); *)
         match v with
         | Thread a -> a
@@ -1315,12 +1329,12 @@ struct
         | _ -> Queries.Result.top q
       end
     | Q.ReachableFrom e -> begin
-        match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv_address ~ctx ctx.local e with
         | Top -> Queries.Result.top q
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Address a ->
           let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
-          let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
+          let addrs = reachable_vars ~ctx ctx.local [a'] in
           let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
           if AD.may_be_unknown a then
             AD.add UnknownPtr addrs' (* add unknown back *)
@@ -1335,7 +1349,7 @@ struct
         | _ -> AD.empty ()
       end
     | Q.ReachableUkTypes e -> begin
-        match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv_address ~ctx ctx.local e with
         | Top -> Queries.Result.top q
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Address a when AD.is_top a || AD.mem Addr.UnknownPtr a ->
@@ -1345,7 +1359,7 @@ struct
         | _ -> Q.TS.empty ()
       end
     | Q.EvalStr e -> begin
-        match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        match eval_rv_address ~ctx ctx.local e with
         (* exactly one string in the set (works for assignments of string constants) *)
         | Address a when List.compare_length_with (AD.to_string a) 1 = 0 -> (* exactly one string *)
           `Lifted (List.hd (AD.to_string a))
@@ -1410,7 +1424,7 @@ struct
   (** [set st addr val] returns a state where [addr] is set to [val]
    * it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining
    * precise information about arrays. *)
-  let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
+  let set ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
     let update_variable x t y z =
       if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\n\n" x.vname VD.pretty y CPA.pretty z;
       let r = update_variable x t y z in (* refers to defintion that is outside of set *)
@@ -1423,11 +1437,12 @@ struct
     (* Updating a single varinfo*offset pair. NB! This function's type does
      * not include the flag. *)
     let update_one_addr (x, offs) (st: store): store =
+      let ask = Analyses.ask_of_ctx ctx in
       let cil_offset = Offs.to_cil_offset offs in
       let t = match t_override with
         | Some t -> t
         | None ->
-          if a.f (Q.IsAllocVar x) then
+          if ctx.ask (Q.IsAllocVar x) then
             (* the vtype of heap vars will be TVoid, so we need to trust the pointer we got to this to be of the right type *)
             (* i.e. use the static type of the pointer here *)
             lval_type
@@ -1442,8 +1457,8 @@ struct
       in
       let update_offset old_value =
         (* Projection globals to highest Precision *)
-        let projected_value = project_val (Queries.to_value_domain_ask a) None None value (is_global a x) in
-        let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in
+        let projected_value = project_val (Queries.to_value_domain_ask ask) None None value (is_global ask x) in
+        let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask ask) old_value offs projected_value lval_raw ((Var x), cil_offset) t in
         if WeakUpdates.mem x st.weak then
           VD.join old_value new_value
         else if invariant then (
@@ -1467,20 +1482,20 @@ struct
       end else
         (* Check if we need to side-effect this one. We no longer generate
          * side-effects here, but the code still distinguishes these cases. *)
-      if (!earlyglobs || ThreadFlag.has_ever_been_multi a) && is_global a x then begin
+      if (!earlyglobs || ThreadFlag.has_ever_been_multi ask) && is_global ask x then begin
         if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: update a global var '%s' ...\n" x.vname;
-        let priv_getg = priv_getg gs in
+        let priv_getg = priv_getg ctx.global in
         (* Optimization to avoid evaluating integer values when setting them.
            The case when invariant = true requires the old_value to be sound for the meet.
            Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *)
-        let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsAllocVar x)) && offs = `NoOffset then begin
+        let old_value = if not invariant && Cil.isIntegralType x.vtype && not (ctx.ask (IsAllocVar x)) && offs = `NoOffset then begin
             VD.bot_value ~varAttr:x.vattr lval_type
           end else
-            Priv.read_global a priv_getg st x
+            Priv.read_global ask priv_getg st x
         in
         let new_value = update_offset old_value in
         if M.tracing then M.tracel "set" "update_offset %a -> %a\n" VD.pretty old_value VD.pretty new_value;
-        let r = Priv.write_global ~invariant a priv_getg (priv_sideg ctx.sideg) st x new_value in
+        let r = Priv.write_global ~invariant ask priv_getg (priv_sideg ctx.sideg) st x new_value in
         if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a\n\n" x.vname D.pretty r;
         r
       end else begin
@@ -1557,7 +1572,7 @@ struct
         else
           let x_updated = update_variable x t new_value st.cpa in
           let with_dep = add_partitioning_dependencies x new_value {st with cpa = x_updated } in
-          effect_on_arrays a with_dep
+          effect_on_arrays ask with_dep
       end
     in
     let update_one x store =
@@ -1580,10 +1595,10 @@ struct
       (* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'\n" x; *)
       M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st
 
-  let set_many ~ctx a (gs:glob_fun) (st: store) lval_value_list: store =
+  let set_many ~ctx (st: store) lval_value_list: store =
     (* Maybe this can be done with a simple fold *)
     let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store =
-      set ~ctx a gs acc lval typ value
+      set ~ctx acc lval typ value
     in
     (* And fold over the list starting from the store turned wstore: *)
     List.fold_left f st lval_value_list
@@ -1632,12 +1647,12 @@ struct
     let convert_offset = convert_offset
 
     let get_var = get_var
-    let get a gs st addrs exp = get a gs st addrs exp
-    let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:true gs st lval lval_type ?lval_raw value
+    let get ~ctx st addrs exp = get ~ctx st addrs exp
+    let set ~ctx st lval lval_type ?lval_raw value = set ~ctx ~invariant:true st lval lval_type ?lval_raw value
 
     let refine_entire_var = true
     let map_oldval oldval _ = oldval
-    let eval_rv_lval_refine a gs st exp lval = eval_rv a gs st (Lval lval)
+    let eval_rv_lval_refine ~ctx st exp lval = eval_rv ~ctx st (Lval lval)
 
     let id_meet_down ~old ~c = ID.meet old c
     let fd_meet_down ~old ~c = FD.meet old c
@@ -1650,11 +1665,11 @@ struct
   let invariant = Invariant.invariant
 
 
-  let set_savetop ~ctx ?lval_raw ?rval_raw ask (gs:glob_fun) st adr lval_t v : store =
+  let set_savetop ~ctx ?lval_raw ?rval_raw st adr lval_t v : store =
     if M.tracing then M.tracel "set" "savetop %a %a %a\n" AD.pretty adr d_type lval_t VD.pretty v;
     match v with
-    | Top -> set ~ctx ask gs st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw
-    | v -> set ~ctx ask gs st adr lval_t v ?lval_raw ?rval_raw
+    | Top -> set ~ctx st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw
+    | v -> set ~ctx st adr lval_t v ?lval_raw ?rval_raw
 
 
   (**************************************************************************
@@ -1697,9 +1712,9 @@ struct
       | _ -> ()
     in
     char_array_hack ();
-    let rval_val = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local rval in
+    let rval_val = eval_rv ~ctx ctx.local rval in
     let rval_val = VD.mark_jmpbufs_as_copied rval_val in
-    let lval_val = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
+    let lval_val = eval_lv ~ctx ctx.local lval in
     (* let sofa = AD.short 80 lval_val^" = "^VD.short 80 rval_val in *)
     (* M.debug ~category:Analyzer @@ sprint ~width:max_int @@ dprintf "%a = %a\n%s" d_plainlval lval d_plainexp rval sofa; *)
     let not_local xs =
@@ -1731,7 +1746,7 @@ struct
           assert (offs = NoOffset);
           VD.Bot
         end else
-          eval_rv_keep_bot (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Lval (Var v, NoOffset))
+          eval_rv_keep_bot ~ctx ctx.local (Lval (Var v, NoOffset))
       in
       begin match current_val with
         | Bot -> (* current value is VD Bot *)
@@ -1741,28 +1756,28 @@ struct
               let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *)
               if M.tracing then M.tracel "set" "init bot value: %a\n" VD.pretty iv;
               let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
-              set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
+              set_savetop ~ctx  ctx.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
             | None ->
-              set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
+              set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
           end
         | _ ->
-          set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
+          set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
       end
     | _ ->
-      set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
+      set_savetop ~ctx ctx.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval
 
 
   let branch ctx (exp:exp) (tv:bool) : store =
-    let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
+    let valu = eval_rv ~ctx ctx.local exp in
     let refine () =
-      let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in
+      let res = invariant ctx ctx.local exp tv in
       if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp));
       if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp));
       if M.tracing then M.traceu "branch" "Invariant enforced!\n";
       match ctx.ask (Queries.CondVars exp) with
       | s when Queries.ES.cardinal s = 1 ->
         let e = Queries.ES.choose s in
-        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
+        invariant ctx res e tv
       | _ -> res
     in
     if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu;
@@ -1802,11 +1817,12 @@ struct
     let init_var v = (AD.of_var v, v.vtype, VD.init_value ~varAttr:v.vattr v.vtype) in
     (* Apply it to all the locals and then assign them all *)
     let inits = List.map init_var f.slocals in
-    set_many ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local inits
+    set_many ~ctx ctx.local inits
 
   let return ctx exp fundec: store =
     if Cil.hasAttribute "noreturn" fundec.svar.vattr then
       M.warn ~category:(Behavior (Undefined Other)) "Function declared 'noreturn' could return";
+    let ask = Analyses.ask_of_ctx ctx in
     let st: store = ctx.local in
     match fundec.svar.vname with
     | "__goblint_dummy_init" ->
@@ -1814,11 +1830,11 @@ struct
       publish_all ctx `Init;
       (* otherfun uses __goblint_dummy_init, where we can properly side effect global initialization *)
       (* TODO: move into sync `Init *)
-      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
+      Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | _ ->
       let locals = List.filter (fun v -> not (WeakUpdates.mem v st.weak)) (fundec.sformals @ fundec.slocals) in
-      let nst_part = rem_many_partitioning (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) ctx.local locals in
-      let nst: store = rem_many (Analyses.ask_of_ctx ctx) nst_part locals in
+      let nst_part = rem_many_partitioning (Queries.to_value_domain_ask ask) ctx.local locals in
+      let nst: store = rem_many ask nst_part locals in
       match exp with
       | None -> nst
       | Some exp ->
@@ -1826,64 +1842,65 @@ struct
           | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
           | ret -> ret
         in
-        let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
-        let st' = set ~ctx ~t_override (Analyses.ask_of_ctx ctx) ctx.global nst (return_var ()) t_override rv in
-        match ThreadId.get_current (Analyses.ask_of_ctx ctx) with
-        | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) ->
+        let rv = eval_rv ~ctx ctx.local exp in
+        let st' = set ~ctx ~t_override nst (return_var ()) t_override rv in
+        match ThreadId.get_current ask with
+        | `Lifted tid when ThreadReturn.is_current ask ->
           (* Evaluate exp and cast the resulting value to the void-pointer-type.
               Casting to the right type here avoids precision loss on joins. *)
           let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in
           ctx.sideg (V.thread tid) (G.create_thread rv);
-          Priv.thread_return (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st'
+          Priv.thread_return ask (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st'
         | _ -> st'
 
   let vdecl ctx (v:varinfo) =
     if not (Cil.isArrayType v.vtype) then
       ctx.local
     else
-      let lval = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Var v, NoOffset) in
-      let current_value = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Lval (Var v, NoOffset)) in
-      let new_value = VD.update_array_lengths (eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local) current_value v.vtype in
-      set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval v.vtype new_value
+      let lval = eval_lv ~ctx ctx.local (Var v, NoOffset) in
+      let current_value = eval_rv ~ctx ctx.local (Lval (Var v, NoOffset)) in
+      let new_value = VD.update_array_lengths (eval_rv ~ctx ctx.local) current_value v.vtype in
+      set ~ctx ctx.local lval v.vtype new_value
 
   (**************************************************************************
    * Function calls
    **************************************************************************)
 
   (** From a list of expressions, collect a list of addresses that they might point to, or contain pointers to. *)
-  let collect_funargs ask ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) =
+  let collect_funargs ~ctx ?(warn=false) (st:store) (exps: exp list) =
+    let ask = Analyses.ask_of_ctx ctx in
     let do_exp e =
-      let immediately_reachable = reachable_from_value ask gs st (eval_rv ask gs st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
-      reachable_vars ask [immediately_reachable] gs st
+      let immediately_reachable = reachable_from_value ask (eval_rv ~ctx st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
+      reachable_vars ~ctx st [immediately_reachable]
     in
     List.concat_map do_exp exps
 
-  let collect_invalidate ~deep ask ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) =
+  let collect_invalidate ~deep ~ctx ?(warn=false) (st:store) (exps: exp list) =
     if deep then
-      collect_funargs ask ~warn gs st exps
+      collect_funargs ~ctx ~warn st exps
     else (
-      let mpt e = match eval_rv_address ask gs st e with
+      let mpt e = match eval_rv_address ~ctx st e with
         | Address a -> AD.remove NullPtr a
         | _ -> AD.empty ()
       in
       List.map mpt exps
     )
 
-  let invalidate ?(deep=true) ~ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
+  let invalidate ?(deep=true) ~ctx (st:store) (exps: exp list): store =
     if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]\n" (d_list ", " d_plainexp) exps;
     if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps;
     (* To invalidate a single address, we create a pair with its corresponding
      * top value. *)
     let invalidate_address st a =
       let t = AD.type_of a in
-      let v = get ask gs st a None in (* None here is ok, just causes us to be a bit less precise *)
-      let nv =  VD.invalidate_value (Queries.to_value_domain_ask ask) t v in
+      let v = get ~ctx st a None in (* None here is ok, just causes us to be a bit less precise *)
+      let nv =  VD.invalidate_value (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) t v in
       (a, t, nv)
     in
     (* We define the function that invalidates all the values that an address
      * expression e may point to *)
     let invalidate_exp exps =
-      let args = collect_invalidate ~deep ~warn:true ask gs st exps in
+      let args = collect_invalidate ~deep ~ctx ~warn:true st exps in
       List.map (invalidate_address st) args
     in
     let invalids = invalidate_exp exps in
@@ -1896,13 +1913,14 @@ struct
       let vs = List.map (Tuple3.third) invalids' in
       M.tracel "invalidate" "Setting addresses [%a] to values [%a]\n" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs
     );
-    set_many ~ctx ask gs st invalids'
+    set_many ~ctx st invalids'
 
 
   let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t =
+    let ask = Analyses.ask_of_ctx ctx in
     let st: store = ctx.local in
     (* Evaluate the arguments. *)
-    let vals = List.map (eval_rv (Analyses.ask_of_ctx ctx) ctx.global st) args in
+    let vals = List.map (eval_rv ~ctx st) args in
     (* generate the entry states *)
     (* If we need the globals, add them *)
     (* TODO: make this is_private PrivParam dependent? PerMutexOplusPriv should keep *)
@@ -1912,12 +1930,12 @@ struct
            Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
            sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
            EnterMultithreaded events only execute after threadenter and threadspawn. *)
-        if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
-          ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st);
-        Priv.threadenter (Analyses.ask_of_ctx ctx) st
+        if not (ThreadFlag.has_ever_been_multi ask) then
+          ignore (Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st);
+        Priv.threadenter ask st
       ) else
         (* use is_global to account for values that became globals because they were saved into global variables *)
-        let globals = CPA.filter (fun k v -> is_global (Analyses.ask_of_ctx ctx) k) st.cpa in
+        let globals = CPA.filter (fun k v -> is_global ask k) st.cpa in
         (* let new_cpa = if !earlyglobs || ThreadFlag.is_multi ctx.ask then CPA.filter (fun k v -> is_private ctx.ask ctx.local k) globals else globals in *)
         let new_cpa = globals in
         {st with cpa = new_cpa}
@@ -1927,13 +1945,13 @@ struct
     add_to_array_map fundec pa;
     let new_cpa = CPA.add_list pa st'.cpa in
     (* List of reachable variables *)
-    let reachable = List.concat_map AD.to_var_may (reachable_vars (Analyses.ask_of_ctx ctx) (get_ptrs vals) ctx.global st) in
+    let reachable = List.concat_map AD.to_var_may (reachable_vars ~ctx st (get_ptrs vals)) in
     let reachable = List.filter (fun v -> CPA.mem v st.cpa) reachable in
     let new_cpa = CPA.add_list_fun reachable (fun v -> CPA.find v st.cpa) new_cpa in
 
     (* Projection to Precision of the Callee *)
     let p = PU.int_precision_from_fundec fundec in
-    let new_cpa = project (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) (Some p) new_cpa fundec in
+    let new_cpa = project (Queries.to_value_domain_ask ask) (Some p) new_cpa fundec in
 
     (* Identify locals of this fundec for which an outer copy (from a call down the callstack) is reachable *)
     let reachable_other_copies = List.filter (fun v -> match Cilfacade.find_scope_fundec v with Some scope -> CilType.Fundec.equal scope fundec | None -> false) reachable in
@@ -1979,7 +1997,7 @@ struct
         (* extra sync so that we do not analyze new threads with bottom global invariant *)
         publish_all ctx `Thread;
         (* Collect the threads. *)
-        let start_addr = eval_tv (Analyses.ask_of_ctx ctx) ctx.global ctx.local start in
+        let start_addr = eval_tv ~ctx ctx.local start in
         let start_funvars = AD.to_var_may start_addr in
         let start_funvars_with_unknown =
           if AD.mem Addr.UnknownPtr start_addr then
@@ -1996,8 +2014,8 @@ struct
          Need this to not have memmove spawn in SV-COMP. *)
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
-      let shallow_flist = collect_invalidate ~deep:false (Analyses.ask_of_ctx ctx) ctx.global ctx.local shallow_args in
-      let deep_flist = collect_invalidate ~deep:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local deep_args in
+      let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in
+      let deep_flist = collect_invalidate ~deep:true ~ctx ctx.local deep_args in
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
@@ -2007,13 +2025,13 @@ struct
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
     if not refine then ctx.local else begin
-      let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in
+      let newst = invariant ctx ctx.local e true in
       (* if check_assert e newst <> `Lifted true then
           M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *)
       newst
     end
 
-  let special_unknown_invalidate ctx ask gs st f args =
+  let special_unknown_invalidate ctx f args =
     (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called");
     let desc = LF.find f in
     let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
@@ -2034,8 +2052,8 @@ struct
     in
     (* TODO: what about escaped local variables? *)
     (* invalidate arguments and non-static globals for unknown functions *)
-    let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in
-    invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
+    let st' = invalidate ~deep:false ~ctx ctx.local shallow_addrs in
+    invalidate ~deep:true ~ctx st' deep_addrs
 
   let check_invalid_mem_dealloc ctx special_fn ptr =
     let has_non_heap_var = AD.exists (function
@@ -2046,7 +2064,7 @@ struct
         | Addr (_,o) -> Offs.cmp_zero_offset o <> `MustZero
         | _ -> false)
     in
-    match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
+    match eval_rv_address ~ctx ctx.local ptr with
     | Address a ->
       if AD.is_top a then (
         AnalysisStateUtil.set_mem_safety_flag InvalidFree;
@@ -2125,19 +2143,18 @@ struct
     let invalidate_ret_lv st = match lv with
       | Some lv ->
         if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname;
-        invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
+        invalidate ~deep:false ~ctx st [Cil.mkAddrOrStartOf lv]
       | None -> st
     in
     let addr_type_of_exp exp =
       let lval = mkMem ~addr:(Cil.stripCasts exp) ~off:NoOffset in
-      let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
+      let addr = eval_lv ~ctx ctx.local lval in
       (addr, AD.type_of addr)
     in
     let forks = forkfun ctx lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
     List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks;
     let st: store = ctx.local in
-    let gs = ctx.global in
     let desc = LF.find f in
     let memory_copying dst src n =
       let dest_size = get_size_of_ptr_target ctx dst in
@@ -2157,21 +2174,21 @@ struct
       in
       let dest_a, dest_typ = addr_type_of_exp dst in
       let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in
-      let src_typ = eval_lv (Analyses.ask_of_ctx ctx) gs st src_lval
+      let src_typ = eval_lv ~ctx ctx.local src_lval
                     |> AD.type_of in
       (* when src and destination type coincide, take value from the source, otherwise use top *)
       let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
           let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
-          eval_rv (Analyses.ask_of_ctx ctx) gs st (Lval src_cast_lval)
+          eval_rv ~ctx st (Lval src_cast_lval)
         else
           VD.top_value (unrollType dest_typ)
       in
-      set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value in
+      set ~ctx st dest_a dest_typ value in
     (* for string functions *)
     let eval_n = function
       (* if only n characters of a given string are needed, evaluate expression n to an integer option *)
       | Some n ->
-        begin match eval_rv (Analyses.ask_of_ctx ctx) gs st n with
+        begin match eval_rv ~ctx st n with
           | Int i ->
             begin match ID.to_int i with
               | Some x -> Some (Z.to_int x)
@@ -2197,10 +2214,10 @@ struct
       | _ -> raise (Failure "String function: not an address")
     in
     let string_manipulation s1 s2 lv all op_addr op_array =
-      let s1_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s1 in
+      let s1_v = eval_rv ~ctx st s1 in
       let s1_a = address_from_value s1_v in
       let s1_typ = AD.type_of s1_a in
-      let s2_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s2 in
+      let s2_v = eval_rv ~ctx st s2 in
       let s2_a = address_from_value s2_v in
       let s2_typ = AD.type_of s2_a in
       (* compute value in string literals domain if s1 and s2 are both string literals *)
@@ -2209,30 +2226,30 @@ struct
         begin match lv, op_addr with
           | Some lv_val, Some f ->
             (* when whished types coincide, compute result of operation op_addr, otherwise use top *)
-            let lv_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in
+            let lv_a = eval_lv ~ctx st lv_val in
             let lv_typ = Cilfacade.typeOfLval lv_val in
             if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *)
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
+              set ~ctx st lv_a lv_typ (f s1_a s2_a)
             else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *)
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a)
+              set ~ctx st lv_a lv_typ (f s1_a s2_a)
             else
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ))
+              set ~ctx st lv_a lv_typ (VD.top_value (unrollType lv_typ))
           | _ ->
             (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *)
             let _ = AD.string_writing_defined s1_a in
-            set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ))
+            set ~ctx st s1_a s1_typ (VD.top_value (unrollType s1_typ))
         end
         (* else compute value in array domain *)
       else
         let lv_a, lv_typ = match lv with
-          | Some lv_val -> eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val, Cilfacade.typeOfLval lv_val
+          | Some lv_val -> eval_lv ~ctx st lv_val, Cilfacade.typeOfLval lv_val
           | None -> s1_a, s1_typ in
-        begin match (get (Analyses.ask_of_ctx ctx) gs st s1_a None), get (Analyses.ask_of_ctx ctx) gs st s2_a None with
-          | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
+        begin match (get ~ctx st s1_a None), get ~ctx st s2_a None with
+          | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
           | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType ->
             let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
             let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
-            set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
+            set ~ctx ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
           | Bot, Array array_s2 ->
             (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
             let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
@@ -2241,7 +2258,7 @@ struct
               try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
               with Failure _ -> ID.top_of ptrdiff_ik in
             let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
-            set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2)
+            set ~ctx st lv_a lv_typ (op_array empty_array array_s2)
           | Bot , _ when CilType.Typ.equal s2_typ charPtrType ->
             (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
             let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
@@ -2252,25 +2269,25 @@ struct
             let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
             let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
             let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
-            set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2)
+            set ~ctx st lv_a lv_typ (op_array empty_array array_s2)
           | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType ->
             (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *)
             if op_addr = None then
               (* triggers warning, function only evaluated for side-effects *)
               let _ = AD.string_writing_defined s1_a in
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ))
+              set ~ctx st s1_a s1_typ (VD.top_value (unrollType s1_typ))
             else
               let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in
               let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
+              set ~ctx st lv_a lv_typ (op_array array_s1 array_s2)
           | _ ->
-            set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ))
+            set ~ctx st lv_a lv_typ (VD.top_value (unrollType lv_typ))
         end
     in
     let st = match desc.special args, f.vname with
     | Memset { dest; ch; count; }, _ ->
       (* TODO: check count *)
-      let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in
+      let eval_ch = eval_rv ~ctx st ch in
       let dest_a, dest_typ = addr_type_of_exp dest in
       let value =
         match eval_ch with
@@ -2279,13 +2296,13 @@ struct
         | _ ->
           VD.top_value dest_typ
       in
-      set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
+      set ~ctx st dest_a dest_typ value
     | Bzero { dest; count; }, _ ->
       (* TODO: share something with memset special case? *)
       (* TODO: check count *)
       let dest_a, dest_typ = addr_type_of_exp dest in
       let value = VD.zero_init_value dest_typ in
-      set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
+      set ~ctx st dest_a dest_typ value
     | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *)
       memory_copying dst src (Some n)
     | Strcpy { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_copy ar1 ar2 (eval_n n)))
@@ -2293,9 +2310,9 @@ struct
     | Strlen s, _ ->
       begin match lv with
         | Some lv_val ->
-          let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in
+          let dest_a = eval_lv ~ctx st lv_val in
           let dest_typ = Cilfacade.typeOfLval lv_val in
-          let v = eval_rv (Analyses.ask_of_ctx ctx) gs st s in
+          let v = eval_rv ~ctx st s in
           let a = address_from_value v in
           let value:value =
             (* if s string literal, compute strlen in string literals domain *)
@@ -2304,11 +2321,11 @@ struct
               Int (AD.to_string_length a)
               (* else compute strlen in array domain *)
             else
-              begin match get (Analyses.ask_of_ctx ctx) gs st a None with
+              begin match get ~ctx st a None with
                 | Array array_s -> Int (CArrays.to_string_length array_s)
                 | _ -> VD.top_value (unrollType dest_typ)
               end in
-          set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
+          set ~ctx st dest_a dest_typ value
         | None -> st
       end
     | Strstr { haystack; needle }, _ ->
@@ -2321,8 +2338,8 @@ struct
           string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD.substring_extraction h_a n_a)))
             (fun h_ar n_ar -> match CArrays.substring_extraction h_ar n_ar with
                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
-               | CArrays.IsSubstrAtIndex0 -> Address (eval_lv (Analyses.ask_of_ctx ctx) gs st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
-               | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv (Analyses.ask_of_ctx ctx) gs st
+               | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
+               | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx st
                                                               (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
         | None -> st
       end
@@ -2340,14 +2357,15 @@ struct
       begin match ThreadId.get_current (Analyses.ask_of_ctx ctx) with
         | `Lifted tid ->
           (
-            let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
+            let rv = eval_rv ~ctx ctx.local exp in
             ctx.sideg (V.thread tid) (G.create_thread rv);
             (* TODO: emit thread return event so other analyses are aware? *)
             (* TODO: publish still needed? *)
             publish_all ctx `Return; (* like normal return *)
-            match ThreadId.get_current (Analyses.ask_of_ctx ctx) with
-            | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) ->
-              ignore @@ Priv.thread_return (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st
+            let ask = Analyses.ask_of_ctx ctx in
+            match ThreadId.get_current ask with
+            | `Lifted tid when ThreadReturn.is_current ask ->
+              ignore @@ Priv.thread_return ask (priv_getg ctx.global) (priv_sideg ctx.sideg) tid st
             | _ -> ())
         | _ -> ()
       end;
@@ -2355,22 +2373,22 @@ struct
     | MutexAttrSetType {attr = attr; typ = mtyp}, _ ->
       begin
         let get_type lval =
-          let address = eval_lv (Analyses.ask_of_ctx ctx) gs st lval in
+          let address = eval_lv ~ctx st lval in
           AD.type_of address
         in
         let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in
         let dest_typ = get_type dst_lval in
-        let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dst_lval in
-        match eval_rv (Analyses.ask_of_ctx ctx) gs st mtyp with
+        let dest_a = eval_lv ~ctx st dst_lval in
+        match eval_rv ~ctx st mtyp with
         | Int x ->
           begin
             match ID.to_int x with
             | Some z ->
               if M.tracing then M.tracel "attr" "setting\n";
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z))
-            | None -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
+              set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z))
+            | None -> set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
           end
-        | _ -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
+        | _ -> set ~ctx st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
       end
     | Identity e, _ ->
       begin match lv with
@@ -2380,22 +2398,22 @@ struct
     (**Floating point classification and trigonometric functions defined in c99*)
     | Math { fun_args; }, _ ->
       let apply_unary fk float_fun x =
-        let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
+        let eval_x = eval_rv ~ctx st x in
         begin match eval_x with
           | Float float_x -> float_fun (FD.cast_to fk float_x)
           | _ -> failwith ("non-floating-point argument in call to function "^f.vname)
         end
       in
       let apply_binary fk float_fun x y =
-        let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
-        let eval_y = eval_rv (Analyses.ask_of_ctx ctx) gs st y in
+        let eval_x = eval_rv ~ctx st x in
+        let eval_y = eval_rv ~ctx st y in
         begin match eval_x, eval_y with
           | Float float_x, Float float_y -> float_fun (FD.cast_to fk float_x) (FD.cast_to fk float_y)
           | _ -> failwith ("non-floating-point argument in call to function "^f.vname)
         end
       in
       let apply_abs ik x =
-        let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
+        let eval_x = eval_rv ~ctx st x in
         begin match eval_x with
           | Int int_x ->
             let xcast = ID.cast_to ik int_x in
@@ -2445,7 +2463,7 @@ struct
         end
       in
       begin match lv with
-        | Some lv_val -> set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv_val) (Cilfacade.typeOfLval lv_val) result
+        | Some lv_val -> set ~ctx st (eval_lv ~ctx st lv_val) (Cilfacade.typeOfLval lv_val) result
         | None -> st
       end
     (* handling thread creations *)
@@ -2455,18 +2473,18 @@ struct
     | ThreadJoin { thread = id; ret_var }, _ ->
       let st' =
         (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
-        match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with
+        match eval_rv ~ctx st ret_var with
         | Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
         | Address ret_a ->
-          begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
-            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
+          begin match eval_rv ~ctx st id with
+            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx st [ret_var]
             | Thread a ->
               let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
               (* TODO: is this type right? *)
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v
-            | _      -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
+              set ~ctx st ret_a (Cilfacade.typeOf ret_var) v
+            | _      -> invalidate ~ctx st [ret_var]
           end
-        | _      -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
+        | _      -> invalidate ~ctx st [ret_var]
       in
       let st' = invalidate_ret_lv st' in
       Priv.thread_join (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st'
@@ -2477,9 +2495,9 @@ struct
         match lv with
         | Some lv ->
           let heap_var = AD.of_var (heap_var true ctx) in
-          (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ctx.ask gs st size); *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(heap_var, TVoid [], Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, true));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address heap_var)]
+          (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *)
+          set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true));
+                            (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)]
         | _ -> st
       end
     | Malloc size, _ -> begin
@@ -2490,9 +2508,9 @@ struct
             then AD.join (AD.of_var (heap_var false ctx)) AD.null_ptr
             else AD.of_var (heap_var false ctx)
           in
-          (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ctx.ask gs st size); *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(heap_var, TVoid [], Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, true));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address heap_var)]
+          (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *)
+          set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true));
+                            (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)]
         | _ -> st
       end
     | Calloc { count = n; size }, _ ->
@@ -2504,20 +2522,20 @@ struct
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
           let ik = Cilfacade.ptrdiff_ikind () in
-          let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
-          let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
+          let sizeval = eval_int ~ctx st size in
+          let countval = eval_int ~ctx st n in
           if ID.to_int countval = Some Z.one then (
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+            set_many ~ctx st [
               (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
-              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))
+              (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))
             ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
             (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+            set_many ~ctx st [
               (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, false))));
-              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset)))))
+              (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset)))))
             ]
           )
         | _ -> st
@@ -2527,8 +2545,7 @@ struct
       check_invalid_mem_dealloc ctx f p;
       begin match lv with
         | Some lv ->
-          let ask = Analyses.ask_of_ctx ctx in
-          let p_rv = eval_rv ask gs st p in
+          let p_rv = eval_rv ~ctx st p in
           let p_addr =
             match p_rv with
             | Address a -> a
@@ -2538,8 +2555,8 @@ struct
             | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
           in
           let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)
-          let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)
-          let size_int = eval_int ask gs st size in
+          let p_addr_get = get ~ctx st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)
+          let size_int = eval_int ~ctx st size in
           let heap_val:value = Blob (p_addr_get, size_int, true) in (* copy old contents with new size *)
           let heap_addr = AD.of_var (heap_var false ctx) in
           let heap_addr' =
@@ -2548,8 +2565,8 @@ struct
             else
               heap_addr
           in
-          let lv_addr = eval_lv ask gs st lv in
-          set_many ~ctx ask gs st [
+          let lv_addr = eval_lv ~ctx st lv in
+          set_many ~ctx st [
             (heap_addr, TVoid [], heap_val);
             (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr');
           ] (* TODO: free (i.e. invalidate) old blob if successful? *)
@@ -2562,22 +2579,20 @@ struct
       st
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | Setjmp { env }, _ ->
-      let ask = Analyses.ask_of_ctx ctx in
-      let st' = match eval_rv ask gs st env with
+      let st' = match eval_rv ~ctx st env with
         | Address jmp_buf ->
           let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
-          let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in
+          let r = set ~ctx st jmp_buf (Cilfacade.typeOf env) value in
           if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
           r
         | _ -> failwith "problem?!"
       in
       begin match lv with
         | Some lv ->
-          set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
+          set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
         | None -> st'
       end
     | Longjmp {env; value}, _ ->
-      let ask = Analyses.ask_of_ctx ctx in
       let ensure_not_zero (rv:value) = match rv with
         | Int i ->
           begin match ID.to_bool i with
@@ -2594,19 +2609,19 @@ struct
           M.warn ~category:Program "Arguments to longjmp are strange!";
           rv
       in
-      let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
+      let rv = ensure_not_zero @@ eval_rv ~ctx ctx.local value in
       let t = Cilfacade.typeOf value in
-      set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
+      set ~ctx ~t_override:t ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
     | Rand, _ ->
       begin match lv with
         | Some x ->
           let result:value = (Int (ID.starting IInt Z.zero)) in
-          set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
+          set ~ctx st (eval_lv ~ctx st x) (Cilfacade.typeOfLval x) result
         | None -> st
       end
     | _, _ ->
       let st =
-        special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args
+        special_unknown_invalidate ctx f args
         (*
           *  TODO: invalidate vars reachable via args
           *  publish globals
@@ -2620,27 +2635,25 @@ struct
     if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st
 
   let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store =
-    let ask = (Analyses.ask_of_ctx ctx) in
-    AD.fold (fun addr st ->
+    AD.fold (fun addr (st: store) ->
         match addr with
-        | Addr.Addr (v,o) ->
-          if CPA.mem v fun_st.cpa then
-            let lval = Addr.Mval.to_cil (v,o) in
-            let address = eval_lv ask ctx.global st lval in
+        | Addr.Addr (v,o) when CPA.mem v fun_st.cpa ->
+          begin
             let lval_type = Addr.type_of addr in
             if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type;
-            match (CPA.find_opt v (fun_st.cpa)), lval_type with
-            | None, _ -> st
+            match CPA.find_opt v (fun_st.cpa) with
+            | None -> st
             (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
-            | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
+            | Some (Array a) when CArrays.domain_of_t a = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
             (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
-            | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
-            | _, _ -> begin
-                let new_val = get ask ctx.global fun_st address None in
+            | Some voidVal when Addr.type_of addr = voidType -> {st with cpa = CPA.add v voidVal st.cpa}
+            | _ ->
+              begin
+                let address = AD.singleton addr in
+                let new_val = get ~ctx fun_st address None in
                 if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
-                let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
-                let partDep = Dep.find_opt v fun_st.deps in
-                match partDep with
+                let st' = set_savetop ~ctx st address lval_type new_val in
+                match Dep.find_opt v fun_st.deps with
                 | None -> st'
                 (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
                 | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
@@ -2648,7 +2661,7 @@ struct
                                                                   | None -> accCPA
                                                                   | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
               end
-          else st
+          end
         | _ -> st
       ) tainted_lvs local_st
 
@@ -2663,7 +2676,7 @@ struct
       let add_globals (st: store) (fun_st: store) =
         (* Remove the return value as this is dealt with separately. *)
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
-        let ask = (Analyses.ask_of_ctx ctx) in
+        let ask = Analyses.ask_of_ctx ctx in
         let tainted = f_ask.f Q.MayBeTainted in
         if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
@@ -2711,7 +2724,7 @@ struct
       let return_var = return_var () in
       let return_val =
         if CPA.mem (return_varinfo ()) fun_st.cpa
-        then get (Analyses.ask_of_ctx ctx) ctx.global fun_st return_var None
+        then get ~ctx fun_st return_var None
         else VD.top ()
       in
 
@@ -2725,7 +2738,7 @@ struct
 
       match lval with
       | None      -> st
-      | Some lval -> set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lval) (Cilfacade.typeOfLval lval) return_val
+      | Some lval -> set_savetop ~ctx st (eval_lv ~ctx st lval) (Cilfacade.typeOfLval lval) return_val
     in
     combine_one ctx.local after
 
@@ -2735,8 +2748,7 @@ struct
       [make_entry ~thread:true ctx fd args]
     | exception Not_found ->
       (* Unknown functions *)
-      let st = ctx.local in
-      let st = special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) ctx.global st f args in
+      let st = special_unknown_invalidate ctx f args in
       [st]
 
   let threadspawn ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
@@ -2824,26 +2836,25 @@ struct
           module V = V
           module G = G
 
-          let oa = Analyses.ask_of_ctx octx
           let ost = octx.local
 
           (* all evals happen in octx with non-top values *)
-          let eval_rv a gs st e = eval_rv oa gs ost e
-          let eval_rv_address a gs st e = eval_rv_address oa gs ost e
-          let eval_lv a gs st lv = eval_lv oa gs ost lv
-          let convert_offset a gs st o = convert_offset oa gs ost o
+          let eval_rv ~ctx st e = eval_rv ~ctx:octx ost e
+          let eval_rv_address ~ctx st e = eval_rv_address ~ctx:octx ost e
+          let eval_lv ~ctx st lv = eval_lv ~ctx:octx ost lv
+          let convert_offset ~ctx st o = convert_offset ~ctx:octx ost o
 
           (* all updates happen in ctx with top values *)
           let get_var = get_var
-          let get a gs st addrs exp = get a gs st addrs exp
-          let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:false gs st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
+          let get ~ctx st addrs exp = get ~ctx st addrs exp
+          let set ~ctx st lval lval_type ?lval_raw value = set ~ctx ~invariant:false st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
 
           let refine_entire_var = false
           let map_oldval oldval t_lval =
             if VD.is_bot oldval then VD.top_value t_lval else oldval
-          let eval_rv_lval_refine a gs st exp lv =
+          let eval_rv_lval_refine ~ctx st exp lv =
             (* new, use different ctx for eval_lv (for Mem): *)
-            eval_rv_base_lval ~eval_lv a gs st exp lv
+            eval_rv_base_lval ~eval_lv ~ctx st exp lv
 
           (* don't meet with current octx values when propagating inverse operands down *)
           let id_meet_down ~old ~c = c
@@ -2854,7 +2865,7 @@ struct
         in
         let module Unassume = BaseInvariant.Make (UnassumeEval) in
         try
-          Unassume.invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true
+          Unassume.invariant ctx ctx.local e true
         with Deadcode -> (* contradiction in unassume *)
           D.bot ()
       in
@@ -2880,31 +2891,32 @@ struct
       WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
           CPA.fold (fun x v acc ->
               let addr: AD.t = AD.of_mval (x, `NoOffset) in
-              set (Analyses.ask_of_ctx ctx) ~ctx ~invariant:false ctx.global acc addr x.vtype v
+              set ~ctx ~invariant:false acc addr x.vtype v
             ) e_d.cpa ctx.local
         )
     in
     D.join ctx.local e_d'
 
   let event ctx e octx =
+    let ask = Analyses.ask_of_ctx ctx in
     let st: store = ctx.local in
     match e with
-    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr;
-      Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr
-    | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+      Priv.lock ask (priv_getg ctx.global) st addr
+    | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       if addr = UnknownPtr then
         M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
+          Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
         )
     | Events.Escape escaped ->
-      Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
+      Priv.escape ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
     | Events.EnterMultiThreaded ->
-      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
+      Priv.enter_multithreaded ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
-      set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
+      set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
     | Events.Assert exp ->
       assert_fn ctx exp true
     | Events.Unassume {exp; uuids} ->
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 003ac06b92..de21aabb91 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -14,18 +14,18 @@ sig
   module V: Analyses.SpecSysVar
   module G: Lattice.S
 
-  val eval_rv: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> VD.t
-  val eval_rv_address: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> VD.t
-  val eval_lv: Queries.ask -> (V.t -> G.t) -> D.t -> lval -> AD.t
-  val convert_offset: Queries.ask -> (V.t -> G.t) -> D.t -> offset -> ID.t Offset.t
+  val eval_rv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
+  val eval_rv_address: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
+  val eval_lv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> lval -> AD.t
+  val convert_offset: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> offset -> ID.t Offset.t
 
-  val get_var: Queries.ask -> (V.t -> G.t) -> D.t -> varinfo -> VD.t
-  val get: Queries.ask -> (V.t -> G.t) -> D.t -> AD.t -> exp option -> VD.t
-  val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t
+  val get_var: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> varinfo -> VD.t
+  val get: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> AD.t -> exp option -> VD.t
+  val set: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t
 
   val refine_entire_var: bool
   val map_oldval: VD.t -> typ -> VD.t
-  val eval_rv_lval_refine: Queries.ask -> (V.t -> G.t) -> D.t -> exp -> lval -> VD.t
+  val eval_rv_lval_refine: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> lval -> VD.t
 
   val id_meet_down: old:ID.t -> c:ID.t -> ID.t
   val fd_meet_down: old:FD.t -> c:FD.t -> FD.t
@@ -61,12 +61,12 @@ struct
       VD.meet old_val new_val
     with Lattice.Uncomparable -> old_val
 
-  let refine_lv_fallback ctx a gs st lval value tv =
+  let refine_lv_fallback ctx st lval value tv =
     if M.tracing then M.tracec "invariant" "Restricting %a with %a\n" d_lval lval VD.pretty value;
-    let addr = eval_lv a gs st lval in
+    let addr = eval_lv ~ctx st lval in
     if (AD.is_top addr) then st
     else
-      let old_val = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
+      let old_val = get ~ctx st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
       let t_lval = Cilfacade.typeOfLval lval in
       let old_val = map_oldval old_val t_lval in
       let old_val =
@@ -77,8 +77,8 @@ struct
         else
           old_val
       in
-      let state_with_excluded = set a gs st addr t_lval value ~ctx in
-      let value =  get a gs state_with_excluded addr None in
+      let state_with_excluded = set st addr t_lval value ~ctx in
+      let value =  get ~ctx state_with_excluded addr None in
       let new_val = apply_invariant ~old_val ~new_val:value in
       if M.tracing then M.traceu "invariant" "New value is %a\n" VD.pretty new_val;
       (* make that address meet the invariant, i.e exclusion sets will be joined *)
@@ -87,18 +87,18 @@ struct
         contra st
       )
       else if VD.is_bot new_val
-      then set a gs st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *)
-      else set a gs st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *)
+      then set st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *)
+      else set st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *)
 
-  let refine_lv ctx a gs st c x c' pretty exp =
-    let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in
+  let refine_lv ctx st c x c' pretty exp =
+    let set' lval v st = set st (eval_lv ~ctx st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in
     match x with
     | Var var, o when refine_entire_var ->
       (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *)
-      let old_val = get_var a gs st var in
+      let old_val = get_var ~ctx st var in
       let old_val = map_oldval old_val var.vtype in
-      let offs = convert_offset a gs st o in
-      let new_val = VD.update_offset (Queries.to_value_domain_ask a) old_val offs c' (Some exp) x (var.vtype) in
+      let offs = convert_offset ~ctx st o in
+      let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) old_val offs c' (Some exp) x (var.vtype) in
       let v = apply_invariant ~old_val ~new_val in
       if is_some_bot v then contra st
       else (
@@ -110,7 +110,7 @@ struct
     | Var _, _
     | Mem _, _ ->
       (* For accesses via pointers, not yet *)
-      let old_val = eval_rv_lval_refine a gs st exp x in
+      let old_val = eval_rv_lval_refine ~ctx st exp x in
       let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
       let v = apply_invariant ~old_val ~new_val:c' in
       if is_some_bot v then contra st
@@ -119,7 +119,7 @@ struct
         set' x v st
       )
 
-  let invariant_fallback ctx a (gs:V.t -> G.t) st exp tv =
+  let invariant_fallback ctx st exp tv =
     (* We use a recursive helper function so that x != 0 is false can be handled
      * as x == 0 is true etc *)
     let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): (lval * VD.t) option =
@@ -146,7 +146,7 @@ struct
             end
           | Address n -> begin
               if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x AD.pretty n;
-              match eval_rv_address a gs st (Lval x) with
+              match eval_rv_address ~ctx st (Lval x) with
               | Address a when AD.is_definite n ->
                 Some (x, Address (AD.diff a n))
               | Top when AD.is_null n ->
@@ -210,12 +210,12 @@ struct
       let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *)
       match exp with
       (* Since we handle not only equalities, the order is important *)
-      | BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv a gs st rval)) tv
+      | BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv ~ctx st rval)) tv
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
       | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
       | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) ->
-        (match eval_rv a gs st (Lval x) with
+        (match eval_rv ~ctx st (Lval x) with
          | Int v ->
            (* This is tricky: It it is not sufficient to check that ID.cast_to_ik v = v
              * If there is one domain that knows this to be true and the other does not, we
@@ -239,16 +239,16 @@ struct
     in
     match derived_invariant exp tv with
     | Some (lval, value) ->
-      refine_lv_fallback ctx a gs st lval value tv
+      refine_lv_fallback ctx st lval value tv
     | None ->
       if M.tracing then M.traceu "invariant" "Doing nothing.\n";
       M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp;
       st
 
-  let invariant ctx a gs st exp tv: D.t =
+  let invariant ctx st exp tv: D.t =
     let fallback reason st =
       if M.tracing then M.tracel "inv" "Can't handle %a.\n%t\n" d_plainexp exp reason;
-      invariant_fallback ctx a gs st exp tv
+      invariant_fallback ctx st exp tv
     in
     (* inverse values for binary operation a `op` b == c *)
     (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
@@ -552,7 +552,7 @@ struct
           a, b
       with FloatDomain.ArithmeticOnFloatBot _ -> raise Analyses.Deadcode
     in
-    let eval e st = eval_rv a gs st e in
+    let eval e st = eval_rv ~ctx st e in
     let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in
     let unroll_fk_of_exp e =
       match unrollType (Cilfacade.typeOf e) with
@@ -693,7 +693,7 @@ struct
               | Float c -> invert_binary_op c FD.pretty (fun ik -> FD.to_int ik c) (fun fk -> FD.cast_to fk c)
               | _ -> failwith "unreachable")
         | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *)
-          let update_lval c x c' pretty = refine_lv ctx a gs st c x c' pretty exp in
+          let update_lval c x c' pretty = refine_lv ctx st c x c' pretty exp in
           let t = Cil.unrollType (Cilfacade.typeOfLval x) in  (* unroll type to deal with TNamed *)
           if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a\n" d_lval x VD.pretty c_typed d_type t;
           begin match c_typed with
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 865cb928aa..7100534fab 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -82,8 +82,6 @@ struct
             M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, potentially all locals were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node
           else if not (Queries.VS.is_empty modified_locals) then
             M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, locals %a were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node Queries.VS.pretty modified_locals
-          else
-            ()
         ) longjmp_nodes;
       D.join modified_locals ctx.local
     | Access {ad; kind = Read; _} ->
diff --git a/src/analyses/ptranalAnalysis.ml b/src/analyses/ptranalAnalysis.ml
new file mode 100644
index 0000000000..6991b5ea22
--- /dev/null
+++ b/src/analyses/ptranalAnalysis.ml
@@ -0,0 +1,31 @@
+(** CIL's {!GoblintCil.Ptranal} for function pointer evaluation ([ptranal]).
+
+    Useful for sound analysis of function pointers without base. *)
+
+(* TODO: fix unsoundness on some bench repo examples: https://github.com/goblint/analyzer/pull/1063 *)
+
+open GoblintCil
+open Analyses
+
+module Spec =
+struct
+  include UnitAnalysis.Spec
+
+  let name () = "ptranal"
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.EvalFunvar (Lval (Mem e, _)) ->
+      let funs = Ptranal.resolve_exp e in
+      (* TODO: filter compatible function pointers by type? *)
+      List.fold_left (fun xs f -> Queries.AD.add (Queries.AD.Addr.of_var f) xs) (Queries.AD.empty ()) funs
+    | _ -> Queries.Result.top q
+
+  let init _: unit =
+    Ptranal.analyze_file !Cilfacade.current_file;
+    Ptranal.compute_results false
+
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 6b7217147e..7dae319d6f 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -349,7 +349,7 @@ struct
             | ts when Queries.TS.is_top ts ->
               includes_uk := true
             | ts ->
-              if Queries.TS.is_empty ts = false then
+              if not (Queries.TS.is_empty ts) then
                 includes_uk := true;
               let f = function
                 | TComp (ci, _) ->
diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml
index 55b1aceefc..263c1033bb 100644
--- a/src/cdomain/value/cdomains/addressDomain.ml
+++ b/src/cdomain/value/cdomains/addressDomain.ml
@@ -277,7 +277,7 @@ struct
     let compute_substring s1 s2 =
       try
         let i = Str.search_forward (Str.regexp_string s2) s1 0 in
-        Some (String.sub s1 i (String.length s1 - i))
+        Some (Str.string_after s1 i)
       with Not_found -> None in
 
     (* if any of the input address sets contains an element that isn't a StrPtr, return top *)
diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index ac9af3c5a4..1c06bff227 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -854,7 +854,6 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l)
     | _ ->
       AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.unknown "May access array out of bounds"
-  else ()
 
 
 module TrivialWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t =
diff --git a/src/cdomain/value/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml
index 0621f37eb6..2b968b0321 100644
--- a/src/cdomain/value/cdomains/stringDomain.ml
+++ b/src/cdomain/value/cdomains/stringDomain.ml
@@ -62,7 +62,7 @@ let to_n_c_string n x =
     else if n < 0 then
       None
     else
-      Some (String.sub x 0 n)
+      Some (Str.first_chars x n)
   | None -> None
 
 let to_string_length x =
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 0fd8fa79fb..bb3592ebb6 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -203,9 +203,8 @@ struct
     | TComp ({cstruct=false; _},_) -> Union (Unions.top ())
     | TArray (ai, length, _) ->
       let typAttr = typeAttrs ai in
-      let can_recover_from_top = ArrayDomain.can_recover_from_top (ArrayDomain.get_domain ~varAttr ~typAttr) in
       let len = array_length_idx (IndexDomain.top ()) length in
-      Array (CArrays.make ~varAttr ~typAttr len (if can_recover_from_top then (top_value ai) else (bot_value ai)))
+      Array (CArrays.make ~varAttr ~typAttr len (top_value ai))
     | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t
     | _ -> Top
 
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 661e220d69..ea8a350d3c 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -282,7 +282,7 @@ struct
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
                 ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in
       if String.starts_with res "+" then
-        String.sub res 1 (String.length res - 1)
+        Str.string_after res 1
       else
         res
     in
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 78aba17060..d47f1efde0 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -695,8 +695,6 @@ let getGlobalInits (file: file) : edges  =
         Hashtbl.add inits (assign lval) ()
       else if not (Hashtbl.mem inits (assign (any_index lval))) then
         Hashtbl.add inits (assign (any_index lval)) ()
-      else
-        ()
     | CompoundInit (typ, lst) ->
       let ntyp = match typ, lst with
         | TArray(t, None, attr), [] -> TArray(t, Some zero, attr) (* set initializer type to t[0] for flexible array members of structs that are intialized with {} *)
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 749ede4fc2..4057359d3d 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -84,8 +84,6 @@ let do_preprocess ast =
   let f fd visitor_fun = ignore @@ visitCilFunction (visitor_fun fd) fd in
   if active_visitors <> [] then
     iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) active_visitors | _ -> ())
-  else
-    ()
 
 (** @raise GoblintCil.FrontC.ParseError
     @raise GoblintCil.Errormsg.Error *)
diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml
index 24a1701ce6..16b5511717 100644
--- a/src/config/gobConfig.ml
+++ b/src/config/gobConfig.ml
@@ -140,7 +140,7 @@ struct
     let rec split' i =
       if i<l then begin
         if xs.[i]=c1 || xs.[i]=c2 then
-          (String.sub xs 0 i, String.sub xs i (l-i))
+          (Str.first_chars xs i, Str.string_after xs i)
         else
           split' (i+1)
       end else
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index f5c024c24f..84d7eff1ed 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1733,7 +1733,7 @@ struct
   let compare_locals h1 h2 =
     let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in
     let f k v1 =
-      if not (PP.mem h2 k) then () else
+      if PP.mem h2 k then
         let v2 = PP.find h2 k in
         let b1 = D.leq v1 v2 in
         let b2 = D.leq v2 v1 in
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 06c51b0c15..4b2eecb632 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -164,6 +164,7 @@ module TaintPartialContexts = TaintPartialContexts
 module UnassumeAnalysis = UnassumeAnalysis
 module ExpRelation = ExpRelation
 module AbortUnless = AbortUnless
+module PtranalAnalysis = PtranalAnalysis
 
 
 (** {1 Domains}
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 55b3fa8fc5..84b120b8e3 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -97,7 +97,7 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
          * case the edge is directly added to the diff set to avoid undetected ambiguities during the recursive
          * call. *)
         let testFalseEdge edge = match edge with
-          | Test (p,b) -> p = Cil.one && b = false
+          | Test (p,false) -> p = Cil.one
           | _ -> false in
         let posAmbigEdge edgeList = let findTestFalseEdge (ll,_) = testFalseEdge (snd (List.hd ll)) in
           let numDuplicates l = List.length (List.find_all findTestFalseEdge l) in
diff --git a/src/solver/generic.ml b/src/solver/generic.ml
index 636aed8831..1a866546a1 100644
--- a/src/solver/generic.ml
+++ b/src/solver/generic.ml
@@ -256,7 +256,7 @@ module SoundBoxSolverImpl =
           H.replace called x ();
           (* set the new value for [x] *)
           eval_rhs_event x;
-          let set_x d = if H.mem called x then set x d else () in
+          let set_x d = if H.mem called x then set x d in
           Option.may (fun f -> set_x (f (eval x) side)) (S.system x);
           (* remove [x] from called *)
           H.remove called x
diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml
index d05d87c4f3..8213fe8166 100644
--- a/src/solver/sLR.ml
+++ b/src/solver/sLR.ml
@@ -327,7 +327,7 @@ module Make0 =
           let k = X.get_key x in
           let _ = work := H.insert !work x in
           let _ = P.rem_item stable x in
-          if k >= sk then () else
+          if k < sk then
             let _ = X.set_value x (D.bot ()) in
             (* ignore @@ Pretty.printf " also restarting %d: %a\n" k S.Var.pretty_trace x; *)
             (* flush_all (); *)
@@ -348,7 +348,7 @@ module Make0 =
           let (i,nonfresh) = X.get_index y in
           let _ = if xi <= i then HM.replace wpoint y () in
           let _ = if (V.ver>2) && xi <= i then work := H.insert (!work) y in
-          let _ = if nonfresh then () else solve y in
+          let _ = if not nonfresh then solve y in
           let _ = L.add infl y x in
           X.get_value y
 
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 91bdb82ce1..eab06222ef 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -119,7 +119,7 @@ module EvalAssert = struct
           s
         | If (e, b1, b2, l,l2) ->
           let vars = Basetype.CilExp.get_vars e in
-          let asserts ~node loc vs = if full then make_assert ~node loc None else List.map (fun x -> make_assert ~node loc (Some (Var x,NoOffset))) vs |> List.concat in
+          let asserts ~node loc vs = if full then make_assert ~node loc None else List.concat_map (fun x -> make_assert ~node loc (Some (Var x,NoOffset))) vs in
           let add_asserts block =
             if block.bstmts <> [] then
               let with_asserts =
@@ -130,8 +130,6 @@ module EvalAssert = struct
                 [cStmt "{ %I:asserts %S:b }" (fun n t -> makeVarinfo true "unknown" (TVoid [])) b_loc [("asserts", FI b_assert_instr); ("b", FS block.bstmts)]]
               in
               block.bstmts <- with_asserts
-            else
-              ()
           in
           if emit_other then (add_asserts b1; add_asserts b2);
           s
diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml
index 923cf7600b..df766d5bdd 100644
--- a/src/util/cilCfg.ml
+++ b/src/util/cilCfg.ml
@@ -29,7 +29,7 @@ class countLoopsVisitor(count) = object
   inherit nopCilVisitor
 
   method! vstmt stmt = match stmt.skind with
-    | Loop _ -> count := !count + 1; DoChildren
+    | Loop _ -> incr count; DoChildren
     | _ -> DoChildren
 
 end
diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml
index 9023a68f8a..95fae95d26 100644
--- a/src/util/terminationPreprocessing.ml
+++ b/src/util/terminationPreprocessing.ml
@@ -59,8 +59,8 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
         s.skind <- Block nb;
         s
       | Goto (sref, l) ->
-        let goto_jmp_stmt = sref.contents.skind in
-        let loc_stmt = Cil.get_stmtLoc goto_jmp_stmt in
+        let goto_jmp_stmt = sref.contents in
+        let loc_stmt = Cilfacade.get_stmtLoc goto_jmp_stmt in
         if CilType.Location.compare l loc_stmt >= 0 then (
           (* is pos if first loc is greater -> below the second loc *)
           (* problem: the program might not terminate! *)
diff --git a/tests/regression/00-sanity/41-both_branches-2.c b/tests/regression/00-sanity/41-both_branches-2.c
new file mode 100644
index 0000000000..4bfd339b13
--- /dev/null
+++ b/tests/regression/00-sanity/41-both_branches-2.c
@@ -0,0 +1,17 @@
+// PARAM: --disable sem.unknown_function.invalidate.globals
+#include <goblint.h>
+struct S {
+  int *f[1];
+};
+
+int main() {
+  struct S* s;
+  s = magic();
+
+  int *p = s->f[0];
+  if (p)
+    __goblint_check(1); // reachable
+  else
+    __goblint_check(1); // reachable
+  return 0;
+}
diff --git a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
index 40e448eb22..c91c141446 100644
--- a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
+++ b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
@@ -22,8 +22,8 @@ int main() {
   ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool));
   cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx));
   if (!cctxPool->cctx[0]) // TODO NOWARN
-    __goblint_check(1); // TODO reachable
+    __goblint_check(1); // reachable
   else
-    __goblint_check(1); // TODO reachable
+    __goblint_check(1); // reachable
   return 0;
 }
diff --git a/tests/regression/33-constants/05-fun_ptranal.c b/tests/regression/33-constants/05-fun_ptranal.c
new file mode 100644
index 0000000000..5ebaf24e22
--- /dev/null
+++ b/tests/regression/33-constants/05-fun_ptranal.c
@@ -0,0 +1,14 @@
+//PARAM: --set ana.activated '["constants", "ptranal"]'
+// intentional explicit ana.activated to do tutorial in isolation
+int f(int a, int b){
+    int d = 3;
+    int z = a + d;
+    return z;
+}
+
+int main(){
+    int d = 0;
+    int (*fp)(int,int) = &f;
+    d = fp(2, 3);
+    return 0;
+}
diff --git a/tests/regression/46-apron2/58-issue-1249.c b/tests/regression/46-apron2/58-issue-1249.c
new file mode 100644
index 0000000000..862c539d15
--- /dev/null
+++ b/tests/regression/46-apron2/58-issue-1249.c
@@ -0,0 +1,10 @@
+// SKIP PARAM: --set ana.activated[+] apron
+int *a;
+int b;
+void c(int d) {
+    // *a is a null pointer here, so we should warn but maybe not crash
+    *a = d;
+}
+int main() {
+    c(b);
+}