From 3d99dec4ffca6e060ae4e61c54fcb2a309a44571 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 03:48:57 +0000
Subject: [PATCH 1/7] Initial plan


From 9a91271845cfeecbe8713a3b622fd73c96590e2f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 03:52:28 +0000
Subject: [PATCH 2/7] port tutorial analyses to simplified spec interface

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/04ac7a0b-b764-4f8a-b7c0-f96bcb75fc44

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
---
 src/analyses/tutorials/constants.ml           | 56 ++++++++--------
 src/analyses/tutorials/signs.ml               | 36 +++++-----
 .../tutorials/solution/signsExtendSol.ml      | 36 +++++-----
 src/analyses/tutorials/solution/signsSol.ml   | 36 +++++-----
 src/analyses/tutorials/solution/taintSol.ml   | 60 ++++++++---------
 src/analyses/tutorials/taint.ml               | 66 +++++++++----------
 src/analyses/tutorials/unitAnalysis.ml        | 55 ++++++++--------
 7 files changed, 176 insertions(+), 169 deletions(-)

diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index cd40d6ffe5..7d91ae21aa 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -2,13 +2,16 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 (** An analysis specification for didactic purposes.
  It only considers definite values of local variables.
  We do not pass information interprocedurally. *)
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "constants"
+  let name = "constants"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   module I = IntDomain.Flattened
 
@@ -16,7 +19,7 @@ struct
   module D = MapDomain.MapBot (Basetype.Variables) (I)
 
   (* No contexts *)
-  include Analyses.IdentityUnitContextsSpec
+  module C = Printable.Unit
 
   let get_local = function
     | Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
@@ -44,29 +47,31 @@ struct
     | _ -> I.top ()
 
   (* transfer functions *)
-  let assign man (lval:lval) (rval:exp) : D.t =
+  let query _ _ (type a) (q: a Queries.t): a Queries.result =
+    Queries.Result.top q
+
+  let assign _ state (lval:lval) (rval:exp) : D.t =
     match get_local lval with
-    | Some loc -> D.add loc (eval man.local rval) man.local
-    | None -> man.local
+    | Some loc -> D.add loc (eval state rval) state
+    | None -> state
 
-  let branch man (exp:exp) (tv:bool) : D.t =
-    let v = eval man.local exp in
+  let branch _ state (exp:exp) (tv:bool) : D.t =
+    let v = eval state exp in
     match I.to_bool v with
       | Some b when b <> tv -> raise Deadcode (* if the expression evaluates to not tv, the tv branch is not reachable *)
-      | _ -> man.local
+      | _ -> state
 
-  let body man (f:fundec) : D.t =
+  let body _ state (f:fundec) : D.t =
     (* Initialize locals to top *)
-    List.fold_left (fun m l -> D.add l (I.top ()) m) man.local f.slocals
+    List.fold_left (fun m l -> D.add l (I.top ()) m) state f.slocals
 
-  let return man (exp:exp option) (f:fundec) : D.t =
+  let return _ state (exp:exp option) (f:fundec) : D.t =
     (* Do nothing, as we are not interested in return values for now. *)
-    man.local
+    state
 
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+  let enter _ (_: D.t) (_: lval option) (f:fundec) (_: exp list) : D.t =
     (* Set the formal int arguments to top *)
-    let callee_state = List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals in
-    [(man.local, callee_state)]
+    List.fold_left (fun m l -> D.add l (I.top ()) m) (D.bot ()) f.sformals
 
   let set_local_int_lval_top (state: D.t) (lval: lval option) =
     match lval with
@@ -77,22 +82,21 @@ struct
         )
       |_ -> state
 
-  let combine_env man lval fexp f args fc au f_ask =
-    man.local (* keep local as opposed to IdentitySpec *)
-
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask): D.t =
+  let combine _ state (_: D.t) (lval:lval option) (_: fundec) (_: exp list): D.t =
     (* If we have a function call with assignment
         x = f (e1, ... , ek)
       with a local int variable x on the left, we set it to top *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special _ state (lval: lval option) (_:varinfo) (_:exp list) : D.t =
     (* When calling a special function, and assign the result to some local int variable, we also set it to top. *)
-    set_local_int_lval_top man.local lval
+    set_local_int_lval_top state lval
 
-  let startstate v = D.bot ()
-  let exitstate v = D.top () (* TODO: why is this different from startstate? *)
+  let startstate = D.bot ()
+  let startcontext = ()
+  let context _ (_, c) _ _ = c
+  let threadenter _ _ _ _ = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index 06412d6201..0a12322e99 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,18 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signs"
+  let name = "signs"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
-
-  let startstate v = D.bot ()
-  let exitstate = startstate
+  module C = D
 
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +68,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -79,17 +79,23 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let branch _ state (_: exp) (_: bool) = state
+  let body _ state (_: fundec) = state
+  let return _ state (_: exp option) (_: fundec) = state
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
+  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/signsExtendSol.ml b/src/analyses/tutorials/solution/signsExtendSol.ml
index 04ed920437..86ce6c58f3 100644
--- a/src/analyses/tutorials/solution/signsExtendSol.ml
+++ b/src/analyses/tutorials/solution/signsExtendSol.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -46,18 +47,18 @@ struct
     for_all (fun x -> for_all (fun y -> Signs.lt x y) y) x
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsExtendSol"
+  let name = "signsExtendSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
+  module C = D
 
-  let startstate v = D.bot ()
-  let exitstate = startstate
-
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -69,8 +70,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -81,17 +81,23 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let branch _ state (_: exp) (_: bool) = state
+  let body _ state (_: fundec) = state
+  let return _ state (_: exp option) (_: fundec) = state
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
+  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/signsSol.ml b/src/analyses/tutorials/solution/signsSol.ml
index d757e308d3..f209a68176 100644
--- a/src/analyses/tutorials/solution/signsSol.ml
+++ b/src/analyses/tutorials/solution/signsSol.ml
@@ -4,6 +4,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module Signs =
 struct
@@ -44,18 +45,18 @@ struct
     | _ -> false
 end
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  let name () = "signsSol"
+  let name = "signsSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
 
   (* Map of integers variables to our signs lattice. *)
   module D = MapDomain.MapBot (Basetype.Variables) (SL)
-  include Analyses.ValueContexts(D)
+  module C = D
 
-  let startstate v = D.bot ()
-  let exitstate = startstate
-
-  include Analyses.IdentitySpec
+  let startstate = D.bot ()
+  let startcontext = D.bot ()
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
@@ -67,8 +68,7 @@ struct
 
   (* Transfer functions: we only implement assignments here.
    * You can leave this code alone... *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let d = man.local in
+  let assign _ d (lval:lval) (rval:exp) : D.t =
     match lval with
     | (Var x, NoOffset) when not x.vaddrof -> D.add x (eval d rval) d
     | _ -> D.top ()
@@ -79,17 +79,23 @@ struct
     | BinOp (Lt, e1, e2, _) -> SL.lt (eval d e1) (eval d e2)
     | _ -> false
 
-  (* We should now provide this information to Goblint. Assertions are integer expressions,
-   * so we implement here a response to EvalInt queries.
-   * You should definitely leave this alone... *)
-  let query man (type a) (q: a Queries.t): a Queries.result =
+  let query _ state (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     match q with
-    | EvalInt e when assert_holds man.local e ->
+    | EvalInt e when assert_holds state e ->
       let ik = Cilfacade.get_ikind_exp e in
       ID.of_bool ik true
     | _ -> Result.top q
+
+  let branch _ state (_: exp) (_: bool) = state
+  let body _ state (_: fundec) = state
+  let return _ state (_: exp option) (_: fundec) = state
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
+  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
+  let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/solution/taintSol.ml b/src/analyses/tutorials/solution/taintSol.ml
index e2bb65d15d..b61ed81332 100644
--- a/src/analyses/tutorials/solution/taintSol.ml
+++ b/src/analyses/tutorials/solution/taintSol.ml
@@ -10,6 +10,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module VarinfoSet = SetDomain.Make(CilType.Varinfo)
 
@@ -21,17 +22,17 @@ let is_source varinfo = Cil.hasAttribute "taint_source" varinfo.vattr
 (** "Fake" variable to handle returning from a function *)
 let return_varinfo = dummyFunDec.svar
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  include Analyses.DefaultSpec
-
-  let name () = "taintSol"
+  let name = "taintSol"
+  module V = Printable.Unit
+  module G = Lattice.Unit
   module D = SetDomain.Make(CilType.Varinfo) (* TODO: Change such that you have a fitting local domain *)
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context man _ _ = ()
-  let startcontext () = ()
+  let context _ _ _ _ = ()
+  let startcontext = ()
 
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
@@ -60,8 +61,10 @@ struct
   (* transfer functions *)
 
   (** Handles assignment of [rval] to [lval]. *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let state = man.local in
+  let query _ _ (type a) (q: a Queries.t): a Queries.result =
+    Queries.Result.top q
+
+  let assign _ state (lval:lval) (rval:exp) : D.t =
     match lval with
     | Var v,_ ->
       (* TODO: Check whether rval is tainted, handle assignment to v accordingly *)
@@ -72,15 +75,15 @@ struct
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
-  let branch man (exp:exp) (tv:bool) : D.t =
+  let branch _ state (exp:exp) (tv:bool) : D.t =
     (* Nothing needs to be done *)
-    man.local
+    ignore (exp, tv);
+    state
 
   (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
       computes the caller state after the function call.
       For this analysis, source and sink functions will be considered _special_ and have to be treated here. *)
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    let caller_state = man.local in
+  let special _ caller_state (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     (* TODO: Check if f is a sink / source and handle it appropriately *)
     (* To warn about a potential issue in the code, use M.warn. *)
     if is_source f then
@@ -105,13 +108,13 @@ struct
 
   (** Handles going from start node of function [f] into the function body of [f].
       Meant to handle e.g. initialization of local variables. *)
-  let body man (f:fundec) : D.t =
+  let body _ state (f:fundec) : D.t =
     (* Nothing needs to be done here, as the (non-formals) locals are initally untainted *)
-    man.local
+    ignore f;
+    state
 
   (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
-  let return man (exp:exp option) (f:fundec) : D.t =
-    let state = man.local in
+  let return _ state (exp:exp option) (f:fundec) : D.t =
     match exp with
     | Some e when is_exp_tainted state e ->
       (* TODO: Record whether a tainted value was returned. *)
@@ -123,8 +126,7 @@ struct
       [enter] returns a caller state, and the initial state of the callee.
       In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
       will compute the caller state after the function call, given the return state of the callee. *)
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let caller_state = man.local in
+  let enter _ caller_state (lval: lval option) (f:fundec) (args:exp list) : D.t =
     (* Create list of (formal, actual_exp)*)
     let zipped = List.combine f.sformals args in
     (* TODO: For the initial callee_state, collect formal parameters where the actual is tainted. *)
@@ -134,21 +136,13 @@ struct
         else ts)
         (D.bot ())
         zipped in
-    (* first component is state of caller, second component is state of callee *)
-    [caller_state, callee_state]
+    ignore lval;
+    callee_state
 
   (** For a function call "lval = f(args)" or "f(args)",
       computes the global environment state of the caller after the call.
       Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    (* Nothing needs to be done *)
-    man.local
-
-  (** For a function call "lval = f(args)" or "f(args)",
-      computes the state of the caller after assigning the return value from the call.
-      Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    let caller_state = man.local in
+  let combine _ caller_state (callee_local:D.t) (lval:lval option) (_: fundec) (_: exp list): D.t =
     (* TODO: Record whether lval was tainted. *)
     match lval with
     | Some (Var v,_) ->
@@ -158,11 +152,9 @@ struct
     | _ -> caller_state
 
   (* You may leave these alone *)
-  let startstate v = D.bot ()
-  let threadenter man ~multiple lval f args = [D.top ()]
-  let threadspawn man ~multiple lval f args fman = man.local
-  let exitstate  v = D.top ()
+  let startstate = D.bot ()
+  let threadenter _ _ _ _ = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index aadc2f91ea..337997c53c 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -10,6 +10,7 @@
 
 open GoblintCil
 open Analyses
+open SimplifiedAnalysis
 
 module VarinfoSet = SetDomain.Make(CilType.Varinfo)
 
@@ -21,17 +22,17 @@ let is_source varinfo = Cil.hasAttribute "taint_source" varinfo.vattr
 (** "Fake" variable to handle returning from a function *)
 let return_varinfo = dummyFunDec.svar
 
-module Spec : Analyses.MCPSpec =
+module Spec : SimplifiedSpec =
 struct
-  include Analyses.DefaultSpec
-
-  let name () = "taint"
+  let name = "taint"
+  module V = Printable.Unit
+  module G = Lattice.Unit
   module D = Lattice.Unit (* TODO: Change such that you have a fitting local domain *)
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context man _ _ = ()
-  let startcontext () = ()
+  let context _ _ _ _ = ()
+  let startcontext = ()
 
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
@@ -60,8 +61,10 @@ struct
   (* transfer functions *)
 
   (** Handles assignment of [rval] to [lval]. *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    let state = man.local in
+  let query _ _ (type a) (q: a Queries.t): a Queries.result =
+    Queries.Result.top q
+
+  let assign _ (state: D.t) (lval:lval) (rval:exp) : D.t =
     match lval with
     | Var v,_ ->
       (* TODO: Check whether rval is tainted, handle assignment to v accordingly *)
@@ -69,41 +72,43 @@ struct
     | _ -> state
 
   (** Handles conditional branching yielding truth value [tv]. *)
-  let branch man (exp:exp) (tv:bool) : D.t =
+  let branch _ (state: D.t) (exp:exp) (tv:bool) : D.t =
     (* Nothing needs to be done *)
-    man.local
+    ignore (exp, tv);
+    state
 
   (** For a call to a _special_ function f "lval = f(args)" or "f(args)",
       computes the caller state after the function call.
       For this analysis, source and sink functions will be considered _special_ and have to be treated here. *)
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    let caller_state = man.local in
+  let special _ (caller_state: D.t) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     (* TODO: Check if f is a sink / source and handle it appropriately *)
     (* To warn about a potential issue in the code, use M.warn. *)
     caller_state
 
   (** Handles going from start node of function [f] into the function body of [f].
       Meant to handle e.g. initialization of local variables. *)
-  let body man (f:fundec) : D.t =
+  let body _ (state: D.t) (f:fundec) : D.t =
     (* Nothing needs to be done here, as the (non-formals) locals are initally untainted *)
-    man.local
+    ignore f;
+    state
 
   (** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
-  let return man (exp:exp option) (f:fundec) : D.t =
-    let state = man.local in
+  let return _ (state: D.t) (exp:exp option) (f:fundec) : D.t =
     match exp with
     | Some e ->
       (* TODO: Record whether a tainted value was returned. *)
       (* Hint: You may use return_varinfo in place of a variable. *)
+      ignore (e, f);
+      state
+    | None ->
+      ignore f;
       state
-    | None -> state
 
   (** For a function call "lval = f(args)" or "f(args)",
       [enter] returns a caller state, and the initial state of the callee.
       In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
       will compute the caller state after the function call, given the return state of the callee. *)
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let caller_state = man.local in
+  let enter _ (caller_state: D.t) (lval: lval option) (f:fundec) (args:exp list) : D.t =
     (* Create list of (formal, actual_exp)*)
     let zipped = List.combine f.sformals args in
     (* TODO: For the initial callee_state, collect formal parameters where the actual is tainted. *)
@@ -113,30 +118,21 @@ struct
         else ts)
         (D.bot ())
         zipped in
-    (* first component is state of caller, second component is state of callee *)
-    [caller_state, callee_state]
+    ignore lval;
+    callee_state
 
   (** For a function call "lval = f(args)" or "f(args)",
       computes the global environment state of the caller after the call.
       Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    (* Nothing needs to be done *)
-    man.local
-
-  (** For a function call "lval = f(args)" or "f(args)",
-      computes the state of the caller after assigning the return value from the call.
-      Argument [callee_local] is the state of [f] at its return node. *)
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    let caller_state = man.local in
+  let combine _ (caller_state: D.t) (callee_local:D.t) (lval:lval option) (_: fundec) (_: exp list): D.t =
     (* TODO: Record whether lval was tainted. *)
+    ignore callee_local;
     caller_state
 
   (* You may leave these alone *)
-  let startstate v = D.bot ()
-  let threadenter man ~multiple lval f args = [D.top ()]
-  let threadspawn man ~multiple lval f args fman = man.local
-  let exitstate  v = D.top ()
+  let startstate = D.bot ()
+  let threadenter _ _ _ _ = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 23c336bfa1..390c7dec78 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -1,49 +1,46 @@
 (** Simplest possible analysis with unit domain ([unit]). *)
 
 open GoblintCil
-open Analyses
+open SimplifiedAnalysis
 
-(* module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Printable.Unit and type marshal = unit = *)
-(* No signature so others can override module G *)
-module Spec =
+module Spec : SimplifiedSpec =
 struct
-  include Analyses.DefaultSpec
-
-  let name () = "unit"
+  let name = "unit"
+  module V = Printable.Unit
+  module G = Lattice.Unit
   module D = Lattice.Unit
   module C = Printable.Unit
 
   (* transfer functions *)
-  let assign man (lval:lval) (rval:exp) : D.t =
-    man.local
+  let query _ _ (type a) (q: a Queries.t) : a Queries.result =
+    Queries.Result.top q
 
-  let branch man (exp:exp) (tv:bool) : D.t =
-    man.local
+  let assign _ state (_: lval) (_: exp) : D.t =
+    state
 
-  let body man (f:fundec) : D.t =
-    man.local
+  let branch _ state (_: exp) (_: bool) : D.t =
+    state
 
-  let return man (exp:exp option) (f:fundec) : D.t =
-    man.local
+  let body _ state (_: fundec) : D.t =
+    state
 
-  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [man.local, man.local]
+  let return _ state (_: exp option) (_: fundec) : D.t =
+    state
 
-  let combine_env man lval fexp f args fc au f_ask =
-    au
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) : D.t =
+    state
 
-  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
-    man.local
+  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) : D.t =
+    state
 
-  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    man.local
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) : D.t =
+    state
 
-  let startcontext () = ()
-  let startstate v = D.bot ()
-  let threadenter man ~multiple lval f args = [D.top ()]
-  let threadspawn man ~multiple lval f args fman = man.local
-  let exitstate  v = D.top ()
+  let startcontext = ()
+  let startstate = D.bot ()
+  let context _ (_, c) _ _ = c
+  let threadenter _ _ _ _ = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)

From 54ce70197b96a8b5c182d412aa56ed77fc2a58d0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 05:53:44 +0000
Subject: [PATCH 3/7] restore unitAnalysis and add simplifiedUnitAnalysis

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/4163237d-68cb-41e2-ac46-468ac7eb3df5

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
---
 .../tutorials/simplifiedUnitAnalysis.ml       | 45 +++++++++++++++
 src/analyses/tutorials/unitAnalysis.ml        | 55 ++++++++++---------
 2 files changed, 74 insertions(+), 26 deletions(-)
 create mode 100644 src/analyses/tutorials/simplifiedUnitAnalysis.ml

diff --git a/src/analyses/tutorials/simplifiedUnitAnalysis.ml b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
new file mode 100644
index 0000000000..6cd9f2a40a
--- /dev/null
+++ b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
@@ -0,0 +1,45 @@
+(** Simplest possible analysis with unit domain ([simplifiedUnit]). *)
+
+open GoblintCil
+open SimplifiedAnalysis
+
+module Spec : SimplifiedSpec =
+struct
+  let name = "simplifiedUnit"
+  module V = Printable.Unit
+  module G = Lattice.Unit
+  module D = Lattice.Unit
+  module C = Printable.Unit
+
+  let query _ _ (type a) (q: a Queries.t) : a Queries.result =
+    Queries.Result.top q
+
+  let assign _ state (_: lval) (_: exp) : D.t =
+    state
+
+  let branch _ state (_: exp) (_: bool) : D.t =
+    state
+
+  let body _ state (_: fundec) : D.t =
+    state
+
+  let return _ state (_: exp option) (_: fundec) : D.t =
+    state
+
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) : D.t =
+    state
+
+  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) : D.t =
+    state
+
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) : D.t =
+    state
+
+  let startstate = D.bot ()
+  let startcontext = ()
+  let context _ (_, c) _ _ = c
+  let threadenter _ _ _ _ = D.top ()
+end
+
+let _ =
+  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 390c7dec78..23c336bfa1 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -1,46 +1,49 @@
 (** Simplest possible analysis with unit domain ([unit]). *)
 
 open GoblintCil
-open SimplifiedAnalysis
+open Analyses
 
-module Spec : SimplifiedSpec =
+(* module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Printable.Unit and type marshal = unit = *)
+(* No signature so others can override module G *)
+module Spec =
 struct
-  let name = "unit"
-  module V = Printable.Unit
-  module G = Lattice.Unit
+  include Analyses.DefaultSpec
+
+  let name () = "unit"
   module D = Lattice.Unit
   module C = Printable.Unit
 
   (* transfer functions *)
-  let query _ _ (type a) (q: a Queries.t) : a Queries.result =
-    Queries.Result.top q
+  let assign man (lval:lval) (rval:exp) : D.t =
+    man.local
 
-  let assign _ state (_: lval) (_: exp) : D.t =
-    state
+  let branch man (exp:exp) (tv:bool) : D.t =
+    man.local
 
-  let branch _ state (_: exp) (_: bool) : D.t =
-    state
+  let body man (f:fundec) : D.t =
+    man.local
 
-  let body _ state (_: fundec) : D.t =
-    state
+  let return man (exp:exp option) (f:fundec) : D.t =
+    man.local
 
-  let return _ state (_: exp option) (_: fundec) : D.t =
-    state
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [man.local, man.local]
 
-  let enter _ state (_: lval option) (_: fundec) (_: exp list) : D.t =
-    state
+  let combine_env man lval fexp f args fc au f_ask =
+    au
 
-  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) : D.t =
-    state
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+    man.local
 
-  let special _ state (_: lval option) (_: varinfo) (_: exp list) : D.t =
-    state
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    man.local
 
-  let startcontext = ()
-  let startstate = D.bot ()
-  let context _ (_, c) _ _ = c
-  let threadenter _ _ _ _ = D.top ()
+  let startcontext () = ()
+  let startstate v = D.bot ()
+  let threadenter man ~multiple lval f args = [D.top ()]
+  let threadspawn man ~multiple lval f args fman = man.local
+  let exitstate  v = D.top ()
 end
 
 let _ =
-  MCPRegistry.registered_simplified_analysis (module Spec : SimplifiedSpec)
+  MCP.register_analysis (module Spec : MCPSpec)

From 812244ed1aa3bedb51b666cae18fd8b38497aec2 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 06:14:52 +0000
Subject: [PATCH 4/7] export SimplifiedUnitAnalysis from goblint_lib

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/51579562-8e2a-4d5d-af08-de4f4244ecb5

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
---
 src/goblint_lib.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 2cbe47dad9..d79fa58141 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -154,6 +154,7 @@ module Constants = Constants
 module Signs = Signs
 module Taint = Taint
 module UnitAnalysis = UnitAnalysis
+module SimplifiedUnitAnalysis = SimplifiedUnitAnalysis
 
 module GStoreWidening = GStoreWidening
 module GStoreWideningHelper = GStoreWideningHelper

From 7aa7b6a08d02b4bd29ddb09bea5a1c9f260a9d70 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 25 May 2026 02:38:16 +0000
Subject: [PATCH 5/7] Reuse SimplifiedUnitAnalysis defaults in signs tutorials

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c85e631b-65eb-4b46-9ad9-79625a27c3fb

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
---
 src/analyses/tutorials/signs.ml               |  9 +----
 .../tutorials/simplifiedUnitAnalysis.ml       | 37 +++++++++++--------
 .../tutorials/solution/signsExtendSol.ml      |  9 +----
 src/analyses/tutorials/solution/signsSol.ml   |  9 +----
 4 files changed, 28 insertions(+), 36 deletions(-)

diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index 0a12322e99..7f01ea4035 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -47,6 +47,8 @@ end
 
 module Spec : SimplifiedSpec =
 struct
+  include SimplifiedUnitAnalysis.DefaultSpec
+
   let name = "signs"
   module V = Printable.Unit
   module G = Lattice.Unit
@@ -87,14 +89,7 @@ struct
       ID.of_bool ik true
     | _ -> Result.top q
 
-  let branch _ state (_: exp) (_: bool) = state
-  let body _ state (_: fundec) = state
-  let return _ state (_: exp option) (_: fundec) = state
-  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
-  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
-  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
   let context _ ((state: D.t), _) _ _ = state
-  let threadenter _ state _ _ = state
 end
 
 let _ =
diff --git a/src/analyses/tutorials/simplifiedUnitAnalysis.ml b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
index 6cd9f2a40a..488d1c6c83 100644
--- a/src/analyses/tutorials/simplifiedUnitAnalysis.ml
+++ b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
@@ -3,41 +3,48 @@
 open GoblintCil
 open SimplifiedAnalysis
 
-module Spec : SimplifiedSpec =
+module DefaultSpec =
 struct
-  let name = "simplifiedUnit"
-  module V = Printable.Unit
-  module G = Lattice.Unit
-  module D = Lattice.Unit
-  module C = Printable.Unit
-
   let query _ _ (type a) (q: a Queries.t) : a Queries.result =
     Queries.Result.top q
 
-  let assign _ state (_: lval) (_: exp) : D.t =
+  let assign _ state (_: lval) (_: exp) =
     state
 
-  let branch _ state (_: exp) (_: bool) : D.t =
+  let branch _ state (_: exp) (_: bool) =
     state
 
-  let body _ state (_: fundec) : D.t =
+  let body _ state (_: fundec) =
     state
 
-  let return _ state (_: exp option) (_: fundec) : D.t =
+  let return _ state (_: exp option) (_: fundec) =
     state
 
-  let enter _ state (_: lval option) (_: fundec) (_: exp list) : D.t =
+  let enter _ state (_: lval option) (_: fundec) (_: exp list) =
     state
 
-  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) : D.t =
+  let combine _ state _ (_: lval option) (_: fundec) (_: exp list) =
     state
 
-  let special _ state (_: lval option) (_: varinfo) (_: exp list) : D.t =
+  let special _ state (_: lval option) (_: varinfo) (_: exp list) =
     state
 
+  let context _ (_, c) _ _ = c
+  let threadenter _ state _ _ = state
+end
+
+module Spec : SimplifiedSpec =
+struct
+  include DefaultSpec
+
+  let name = "simplifiedUnit"
+  module V = Printable.Unit
+  module G = Lattice.Unit
+  module D = Lattice.Unit
+  module C = Printable.Unit
+
   let startstate = D.bot ()
   let startcontext = ()
-  let context _ (_, c) _ _ = c
   let threadenter _ _ _ _ = D.top ()
 end
 
diff --git a/src/analyses/tutorials/solution/signsExtendSol.ml b/src/analyses/tutorials/solution/signsExtendSol.ml
index 86ce6c58f3..d01f3e236d 100644
--- a/src/analyses/tutorials/solution/signsExtendSol.ml
+++ b/src/analyses/tutorials/solution/signsExtendSol.ml
@@ -49,6 +49,8 @@ end
 
 module Spec : SimplifiedSpec =
 struct
+  include SimplifiedUnitAnalysis.DefaultSpec
+
   let name = "signsExtendSol"
   module V = Printable.Unit
   module G = Lattice.Unit
@@ -89,14 +91,7 @@ struct
       ID.of_bool ik true
     | _ -> Result.top q
 
-  let branch _ state (_: exp) (_: bool) = state
-  let body _ state (_: fundec) = state
-  let return _ state (_: exp option) (_: fundec) = state
-  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
-  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
-  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
   let context _ ((state: D.t), _) _ _ = state
-  let threadenter _ state _ _ = state
 end
 
 let _ =
diff --git a/src/analyses/tutorials/solution/signsSol.ml b/src/analyses/tutorials/solution/signsSol.ml
index f209a68176..e59c332bc5 100644
--- a/src/analyses/tutorials/solution/signsSol.ml
+++ b/src/analyses/tutorials/solution/signsSol.ml
@@ -47,6 +47,8 @@ end
 
 module Spec : SimplifiedSpec =
 struct
+  include SimplifiedUnitAnalysis.DefaultSpec
+
   let name = "signsSol"
   module V = Printable.Unit
   module G = Lattice.Unit
@@ -87,14 +89,7 @@ struct
       ID.of_bool ik true
     | _ -> Result.top q
 
-  let branch _ state (_: exp) (_: bool) = state
-  let body _ state (_: fundec) = state
-  let return _ state (_: exp option) (_: fundec) = state
-  let enter _ state (_: lval option) (_: fundec) (_: exp list) = state
-  let combine _ state (_: D.t) (_: lval option) (_: fundec) (_: exp list) = state
-  let special _ state (_: lval option) (_: varinfo) (_: exp list) = state
   let context _ ((state: D.t), _) _ _ = state
-  let threadenter _ state _ _ = state
 end
 
 let _ =

From 2afea5169d993050d0dd0af7c8731001e790679c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 25 May 2026 02:39:05 +0000
Subject: [PATCH 6/7] Adjust SimplifiedUnitAnalysis defaults to safe shared
 subset

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c85e631b-65eb-4b46-9ad9-79625a27c3fb

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
---
 src/analyses/tutorials/signs.ml                   | 1 +
 src/analyses/tutorials/simplifiedUnitAnalysis.ml  | 4 +---
 src/analyses/tutorials/solution/signsExtendSol.ml | 1 +
 src/analyses/tutorials/solution/signsSol.ml       | 1 +
 4 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index 7f01ea4035..2ec00ad067 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -90,6 +90,7 @@ struct
     | _ -> Result.top q
 
   let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
diff --git a/src/analyses/tutorials/simplifiedUnitAnalysis.ml b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
index 488d1c6c83..4f0ee13b3a 100644
--- a/src/analyses/tutorials/simplifiedUnitAnalysis.ml
+++ b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
@@ -28,9 +28,6 @@ struct
 
   let special _ state (_: lval option) (_: varinfo) (_: exp list) =
     state
-
-  let context _ (_, c) _ _ = c
-  let threadenter _ state _ _ = state
 end
 
 module Spec : SimplifiedSpec =
@@ -45,6 +42,7 @@ struct
 
   let startstate = D.bot ()
   let startcontext = ()
+  let context _ (_, c) _ _ = c
   let threadenter _ _ _ _ = D.top ()
 end
 
diff --git a/src/analyses/tutorials/solution/signsExtendSol.ml b/src/analyses/tutorials/solution/signsExtendSol.ml
index d01f3e236d..738b5f7c25 100644
--- a/src/analyses/tutorials/solution/signsExtendSol.ml
+++ b/src/analyses/tutorials/solution/signsExtendSol.ml
@@ -92,6 +92,7 @@ struct
     | _ -> Result.top q
 
   let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =
diff --git a/src/analyses/tutorials/solution/signsSol.ml b/src/analyses/tutorials/solution/signsSol.ml
index e59c332bc5..3644bb1eb0 100644
--- a/src/analyses/tutorials/solution/signsSol.ml
+++ b/src/analyses/tutorials/solution/signsSol.ml
@@ -90,6 +90,7 @@ struct
     | _ -> Result.top q
 
   let context _ ((state: D.t), _) _ _ = state
+  let threadenter _ state _ _ = state
 end
 
 let _ =

From ae90222cb82739f43178329f9456f74ebe6d890a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 25 May 2026 11:23:22 +0800
Subject: [PATCH 7/7] Potential fix for pull request finding

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
---
 src/analyses/tutorials/simplifiedUnitAnalysis.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/tutorials/simplifiedUnitAnalysis.ml b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
index 4f0ee13b3a..ccf98fc87b 100644
--- a/src/analyses/tutorials/simplifiedUnitAnalysis.ml
+++ b/src/analyses/tutorials/simplifiedUnitAnalysis.ml
@@ -23,8 +23,8 @@ struct
   let enter _ state (_: lval option) (_: fundec) (_: exp list) =
     state
 
-  let combine _ state _ (_: lval option) (_: fundec) (_: exp list) =
-    state
+  let combine _ _ callee_local (_: lval option) (_: fundec) (_: exp list) =
+    callee_local
 
   let special _ state (_: lval option) (_: varinfo) (_: exp list) =
     state