Remove some usages of MyCFG.current_node

src/analyses/base.ml

@@ -2908,11 +2908,8 @@ struct
       let nst = add_globals st fun_st in
 
       (* Projection to Precision of the Caller *)
-      let p = PrecisionUtil.int_precision_from_node () in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
-      let callerFundec = match !MyCFG.current_node with
-        | Some n -> Node.find_fundec n
-        | None -> failwith "callerfundec not found"
-      in
+      let callerFundec = Node.find_fundec man.node in
+      let p:PrecisionUtil.int_precision = PrecisionUtil.int_precision_from_fundec callerFundec in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
       let cpa' = project (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (Some p) nst.cpa callerFundec in
 
       if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.svar.vattr then raise Deadcode;
@@ -2931,11 +2928,8 @@ struct
       in
 
       (* Projection to Precision of the Caller *)
-      let p = PrecisionUtil.int_precision_from_node () in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
-      let callerFundec = match !MyCFG.current_node with
-        | Some n -> Node.find_fundec n
-        | None -> failwith "callerfundec not found"
-      in
+      let callerFundec = Node.find_fundec man.node in
+      let p = PrecisionUtil.int_precision_from_fundec callerFundec in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
       let return_val = project_val (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (attributes_varinfo (return_varinfo ()) callerFundec) (Some p) return_val (is_privglob (return_varinfo ())) in
 
       match lval with

src/analyses/baseInvariant.ml

@@ -362,7 +362,8 @@ struct
         in
         let a,b = meet_bin a''' b' in
         (* Special handling for case a % 2 != c *)
-        let a = if PrecisionUtil.(is_congruence_active (int_precision_from_node_or_config ())) then
+        let callerFundec = Node.find_fundec man.node in
+        let a = if PrecisionUtil.(is_congruence_active (int_precision_from_fundec_or_config callerFundec)) then
             let two = Z.of_int 2 in
             match ID.to_int b, ID.to_excl_list c with
             | Some b, Some ([v], _) when Z.equal b two ->

src/analyses/extractPthread.ml

@@ -264,7 +264,7 @@ end = struct
 
   let get man =
     let d : PthreadDomain.D.t = man.local in
-    let node = Option.get !MyCFG.current_node in
+    let node = man.prev_node in
     let fundec = Node.find_fundec node in
     let thread_name =
       let cur_tid =
@@ -905,7 +905,7 @@ module Spec : Analyses.MCPSpec = struct
     let should_ignore_assigns = GobConfig.get_bool "ana.extract-pthread.ignore_assign" in
     if PthreadDomain.D.is_bot man.local || should_ignore_assigns
     then man.local
-    else if Option.is_none !MyCFG.current_node
+    else if !AnalysisState.global_initialization
     then (
       (* it is global var assignment *)
       let var_opt = Variable.make_from_lval lval in

src/analyses/raceAnalysis.ml

@@ -312,7 +312,7 @@ struct
         (*partitions & locks*)
         Obj.obj (oman.ask (PartAccess (Memory {exp; var_opt=vo; kind})))
       in
-      let node = Option.get !Node.current_node in
+      let node = man.prev_node in
       let add_access conf voffs =
         let acc = part_access (Option.map fst voffs) in
         Access.add ~side:(side_access oman {conf; kind; node; exp; acc}) ~side_empty:(side_access_empty oman) exp voffs;
@@ -374,7 +374,7 @@ struct
       let exp = Lval (Var f, NoOffset) in
       let conf = 110 in
       let kind = AccessKind.Call in
-      let node = Option.get !Node.current_node in
+      let node = man.prev_node in
       let vo = Some f in
       let acc = Obj.obj (man.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in
       side_access man {conf; kind; node; exp; acc} ((`Var f), `NoOffset) ;

src/cdomain/value/util/precisionUtil.ml

@@ -91,6 +91,12 @@ let int_precision_from_node_or_config (): int_precision =
   else
     (get_def_exc (), get_interval (), get_enums (), get_congruence (), get_interval_set (), get_bitfield ())
 
+let int_precision_from_fundec_or_config f: int_precision =
+  if get_annotation_int_enabled () then
+    int_precision_from_fundec f
+  else
+    (get_def_exc (), get_interval (), get_enums (), get_congruence (), get_interval_set (), get_bitfield ())
+
 let float_precision_from_node_or_config (): float_precision =
   if GobConfig.get_bool "annotation.float.enabled" then
     float_precision_from_node ()

src/cdomains/pthreadDomain.ml

@@ -15,8 +15,6 @@ module Pred = struct
 
   let of_node = singleton % Node.location
 
-  let of_current_node () = of_node @@ Option.get !MyCFG.current_node
-
   let string_of_elt (loc:Base.t) =
     let f i = (if i < 0 then "n" else "") ^ string_of_int (abs i) in
     f loc.line ^ "b" ^ f loc.byte

src/config/options.schema.json

@@ -2187,20 +2187,6 @@
           },
           "additionalProperties": false
         },
-        "limit": {
-          "title": "dbg.limit",
-          "type": "object",
-          "properties": {
-            "widen": {
-              "title": "dbg.limit.widen",
-              "description":
-                "Limit for number of widenings per node (0 = no limit).",
-              "type": "integer",
-              "default": 0
-            }
-          },
-          "additionalProperties": false
-        },
         "warn_with_context": {
           "title": "dbg.warn_with_context",
           "description":

src/framework/control.ml

@@ -36,7 +36,6 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
       |> lift true (module DeadCodeLifter)
       |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
-      |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
       |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
       |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.

src/lifters/specLifters.ml

@@ -445,34 +445,6 @@ struct
     | q -> query' man q
 end
 
-
-(** Limits the number of widenings per node. *)
-module LimitLifter (S:Spec) =
-struct
-  include (S : module type of S with module D := S.D and type marshal = S.marshal)
-
-  let name () = S.name ()^" limited"
-
-  let limit = ref 0
-
-  let init marshal =
-    limit := get_int "dbg.limit.widen";
-    S.init marshal
-
-  module H = MyCFG.NodeH
-  let h = H.create 13
-  let incr k =
-    H.modify_def 1 k (fun v ->
-        if v >= !limit then failwith (GobPretty.sprintf "LimitLifter: Reached limit (%d) for node %a" !limit Node.pretty_plain_short (Option.get !MyCFG.current_node));
-        v+1
-      ) h;
-  module D = struct
-    include S.D
-    let widen x y = Option.may incr !MyCFG.current_node; widen x y (* when is this None? *)
-  end
-end
-
-
 (* widening on contexts, keeps contexts for calls only in D *)
 module WidenContextLifterSide (S:Spec)
 =