Run dead code analysis with reanalyze

src/analyses/arinc.ml

@@ -625,11 +625,12 @@ struct
       | _ -> d
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
-    let d = ctx.local in
+    (* let d = ctx.local in *)
     match q with
-    | Queries.Priority _ ->
+    (* had this query but nobody asked for it *)
+    (* | Queries.Priority _ ->
       if Pri.is_int d.pri then Queries.ID.of_int IInt @@ BI.of_int64 @@ Option.get @@ Pri.to_int d.pri (* TODO: what ikind to use for priorities? *)
-      else if Pri.is_top d.pri then Queries.Result.top q else Queries.Result.bot q (* TODO: remove bot *)
+      else if Pri.is_top d.pri then Queries.Result.top q else Queries.Result.bot q (* TODO: remove bot *) *)
     (* | Queries.MayBePublic _ -> *)
     (*   `Bool ((PrE.to_int d.pre = Some 0L || PrE.to_int d.pre = None) && (not (mode_is_init d.pmo))) *)
     | _ -> Queries.Result.top q

src/analyses/base.ml

@@ -73,7 +73,6 @@ struct
 
   let name () = "base"
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
-  let otherstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
 
   (**************************************************************************

src/analyses/commonPriv.ml

@@ -61,9 +61,6 @@ struct
     let r = is_protected_by ask m x in
     if r then ProtectionLogging.record m x;
     r
-
-  let is_atomic ask: bool =
-    ask Q.MustBeAtomic
 end
 
 module MutexGlobals =

src/analyses/condVars.ml

@@ -1,4 +1,5 @@
 (** Must equality between variables and logical expressions. *)
+(* TODO: unused, what is this analysis? *)
 
 open Prelude.Ana
 open Analyses

src/analyses/fileUse.ml

@@ -39,14 +39,6 @@ struct
     | [(v,_)] -> Some v
     | _ -> None
 
-  let query_eq (ask: Queries.ask) exp =
-    match ask.f (Queries.EqualSet exp) with
-    | l when not (Queries.ES.is_top l) ->
-      Queries.ES.elements l
-    | _ -> []
-  let print_query_eq ?msg:(msg="") ask exp =
-    let xs = query_eq ask exp in (* EqualSet -> ExpSet *)
-    Messages.debug "%s EqualSet %a = [%a]" msg d_exp exp (Pretty.d_list ", " d_exp) xs
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =

src/analyses/mCP.ml

@@ -268,9 +268,6 @@ struct
           Result.meet a @@ S.query ctx' q
         in
         match q with
-        | Queries.PrintFullState ->
-          ignore (Pretty.printf "Current State:\n%a\n\n" D.pretty ctx.local);
-          ()
         | Queries.WarnGlobal g ->
           (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
           let (n, g): V.t = Obj.obj g in
@@ -331,7 +328,6 @@ struct
     { ctx with
       local  = obj d
     ; context = (fun () -> ctx.context () |> assoc n |> obj)
-    ; postsub= assoc_sub post_all
     ; global = (fun v      -> ctx.global (v_of n v) |> g_to n |> obj)
     ; split
     ; sideg  = (fun v g    -> ctx.sideg (v_of n v) (g_of n g))

src/analyses/malloc_null.ml

@@ -183,10 +183,6 @@ struct
 
   (* Function calls *)
 
-  let eval_funvar ctx (fv:exp) : varinfo list =
-    warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local fv;
-    []
-
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let nst = remove_unreachable (Analyses.ask_of_ctx ctx) args ctx.local in
     may (fun x -> warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval x)) lval;

src/analyses/mutexAnalysis.ml

@@ -143,13 +143,6 @@ struct
       event ctx e octx (* delegate to must lockset analysis *)
 end
 
-module MyParam =
-struct
-  module G = LockDomain.Simple
-  let effect_fun ?write:(w=false) ls = Lockset.export_locks ls
-  let check_fun = effect_fun
-end
-
 module WriteBased =
 struct
   module GReadWrite =

src/analyses/termination.ml

@@ -4,7 +4,6 @@ open Prelude.Ana
 open Analyses
 
 module M = Messages
-let (%?) = Option.bind
 let (||?) a b = match a,b with Some x,_ | _, Some x -> Some x | _ -> None
 
 module TermDomain = struct

src/analyses/uninit.ml

@@ -47,6 +47,7 @@ struct
     | _ ->
       M.warn "Access to unknown address could be global"; []
 
+  (* TODO: unused? remove? *)
   let rec access_one_byval a rw (exp:exp) =
     match exp with
     (* Integer literals *)

src/analyses/varEq.ml

@@ -119,6 +119,7 @@ struct
       | _ -> false
 
   (* kill predicate for must-equality kind of analyses*)
+  (* TODO: why unused? how different from below? *)
   let may_change_t (b:exp) (a:exp) : bool =
     let rec type_may_change_t a bt =
       let rec may_change_t_offset o =
@@ -151,6 +152,7 @@ struct
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
     type_may_change_t a bt
 
+  (* TODO: why unused? how different from below? *)
   let may_change_pt ask (b:exp) (a:exp) : bool =
     let pt e = ask (Queries.MayPointTo e) in
     let rec lval_may_change_pt a bl : bool =

src/cdomains/addressDomain.ml

@@ -1,7 +1,6 @@
 open Cil
 open Pretty
 open IntOps
-let fast_addr_sets = false (* unknown addresses for fast sets == top, for slow == {?}*)
 
 module GU = Goblintutil
 module M = Messages
@@ -41,7 +40,6 @@ struct
   let unknown_ptr    = singleton Addr.UnknownPtr
   let not_null       = unknown_ptr
   let top_ptr        = of_list Addr.([UnknownPtr; NullPtr])
-  let is_unknown x   = is_element Addr.UnknownPtr x
   let may_be_unknown x = exists (fun e -> e = Addr.UnknownPtr) x
   let is_null x      = is_element Addr.NullPtr x
   let is_not_null x  = for_all (fun e -> e <> Addr.NullPtr) x
@@ -117,6 +115,7 @@ struct
       | false, false -> join x y
   *)
 
+  (* TODO: overrides is_top, but not top? *)
   let is_top a = mem Addr.UnknownPtr a
 
   let merge uop cop x y =

src/cdomains/apron/apronDomain.apron.ml

@@ -1000,11 +1000,7 @@ sig
   include SLattice with type t = Man.mt A.t
 
 
-  val exp_is_cons : exp -> bool
-  val assert_cons : t -> exp -> bool -> t
   val assert_inv : t -> exp -> bool -> t
-  val check_assert : t -> exp -> [> `False | `Top | `True ]
-  val eval_interval_expr : t -> exp -> Z.t option * Z.t option
   val eval_int : t -> exp -> Queries.ID.t
 end
 
@@ -1020,7 +1016,6 @@ module ApronComponents (D2: S2) (PrivD: Lattice.S):
 sig
   module AD: S2 with type Man.mt = D2.Man.mt
   include Lattice.S with type t = (D2.t, PrivD.t) aproncomponents_t
-  val op_scheme: (D2.t -> D2.t -> D2.t) -> (PrivD.t -> PrivD.t -> PrivD.t) -> t -> t -> t
 end =
 struct
   module AD = D2

src/cdomains/arrayDomain.ml

@@ -25,7 +25,6 @@ sig
   val get_vars_in_e: t -> Cil.varinfo list
   val map: (value -> value) -> t -> t
   val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
-  val fold_left2: ('a -> value -> value -> 'a) -> 'a -> t -> t -> 'a
   val smart_join: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
   val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
   val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
@@ -60,7 +59,6 @@ struct
   let get_vars_in_e _ = []
   let map f x = f x
   let fold_left f a x = f a x
-  let fold_left2 f a x y = f a x y
 
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>Any</key>\n%a\n</map>\n</value>\n" Val.printXml x
   let smart_join _ _ = join
@@ -145,7 +143,6 @@ struct
   let get_vars_in_e _ = []
   let map f (xl, xr) = ((List.map f xl), f xr)
   let fold_left f a x = f a (join_of_all_parts x)
-  let fold_left2 f a x y = f a (join_of_all_parts x) (join_of_all_parts y)
   let printXml f (xl,xr) = BatPrintf.fprintf f "<value>\n<map>\n
   <key>unrolled array</key>\n
   <key>xl</key>\n%a\n\n
@@ -309,9 +306,6 @@ struct
   let fold_left f a (_, ((xl:value), (xm:value), (xr:value))) =
     f (f (f a xl) xm) xr
 
-  let fold_left2 f a (_, ((xl:value), (xm:value), (xr:value))) (_, ((yl:value), (ym:value), (yr:value))) =
-    f (f (f a xl yl) xm ym) xr yr
-
   let move_if_affected_with_length ?(replace_with_const=false) length (ask:Q.ask) ((e, (xl,xm, xr)) as x) (v:varinfo) movement_for_exp =
     normalize @@
     let move (i:int option) =
@@ -707,7 +701,6 @@ struct
   let move_if_affected ?(replace_with_const=false) _ x _ _ = x
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e _ = []
 
   let smart_join _ _ = join
@@ -748,7 +741,6 @@ struct
 
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e (x, _) = Base.get_vars_in_e x
 
   let smart_join x_eval_int y_eval_int (x,xl) (y,yl) =
@@ -794,7 +786,6 @@ struct
   let move_if_affected ?(replace_with_const=false) _ x _ _ = x
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e _ = []
 
   let smart_join _ _ = join
@@ -855,7 +846,6 @@ struct
   let length = unop' P.length T.length U.length
   let map f = unop_to_t' (P.map f) (T.map f) (U.map f)
   let fold_left f s = unop' (P.fold_left f s) (T.fold_left f s) (U.fold_left f s)
-  let fold_left2 f s = binop' (P.fold_left2 f s) (T.fold_left2 f s) (U.fold_left2 f s)
 
   let move_if_affected ?(replace_with_const=false) (ask:Q.ask) x v f = unop_to_t' (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> U.move_if_affected ~replace_with_const:replace_with_const ask x v f) x
   let get_vars_in_e = unop' P.get_vars_in_e T.get_vars_in_e U.get_vars_in_e

src/cdomains/arrayDomain.mli

@@ -38,9 +38,6 @@ sig
   val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
   (** Left fold (like List.fold_left) over the arrays elements *)
 
-  val fold_left2: ('a -> value -> value -> 'a) -> 'a -> t -> t -> 'a
-  (** Left fold over the elements of two arrays (like List.fold_left2 *)
-
   val smart_join: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t  -> t
   val smart_widen: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t
   val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t  -> bool

src/cdomains/basetype.ml

@@ -29,8 +29,6 @@ struct
       "(" ^ x.vname ^ ", " ^ description ^ ")"
     else x.vname
   let pretty () x = Pretty.text (show x)
-  let pretty_trace () x = Pretty.dprintf "%s on %a" x.vname CilType.Location.pretty x.vdecl
-  let get_location x = x.vdecl
   type group = Global | Local | Parameter | Temp [@@deriving show { with_path = false }]
   let (%) = Batteries.(%)
   let to_group = Option.some % function
@@ -40,8 +38,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-  let var_id _ = "globals"
-  let node _ = MyCFG.Function Cil.dummyFunDec
 
   let arbitrary () = MyCheck.Arbitrary.varinfo
 end

src/cdomains/exp.ml

@@ -59,6 +59,7 @@ struct
     in
     cv false e
 
+  (* TODO: unused *)
   let contains_field f e =
     let rec offs_contains o =
       match o with
@@ -159,6 +160,7 @@ struct
     | Question _ -> failwith "Logical operations should be compiled away by CIL."
     | _ -> failwith "Unmatched pattern."
 
+  (* TODO: unused *)
   let rec base_compinfo q exp =
     match exp with
     | SizeOf _
@@ -270,6 +272,7 @@ struct
 
   exception NotSimpleEnough
 
+  (* TODO: unused *)
   let rec ees_to_offs = function
     | [] 		-> `NoOffset
     (*	| Addr :: x ->
@@ -320,6 +323,7 @@ struct
     | EAddr::xs     , Lval lv   -> fromEl xs (AddrOf lv)
     | _            ,             _ -> raise (Invalid_argument "")
 
+  (* TODO: unused *)
   let strip_fields e =
     let rec sf e fs =
       match e with

src/cdomains/listDomain.ml

@@ -2,6 +2,8 @@ open Cil
 
 module GU = Goblintutil
 
+(* TODO: most operations unused *)
+
 module type S =
 sig
   include Lattice.S

src/cdomains/lockDomain.ml

@@ -78,7 +78,6 @@ struct
   let empty = ReverseAddrSet.empty
   let is_empty = ReverseAddrSet.is_empty
 
-  let map = ReverseAddrSet.map
   let filter = ReverseAddrSet.filter
   let fold = ReverseAddrSet.fold
   let singleton = ReverseAddrSet.singleton
@@ -106,9 +105,6 @@ struct
   module S = SetDomain.ToppedSet (Exp) (struct let topname = "All mutexes" end)
   include Lattice.Reverse (S)
 
-  let empty = S.empty
-  let is_empty = S.is_empty
-
   let rec eq_set (ask: Queries.ask) e =
     S.union
       (match ask.f (Queries.EqualSet e) with
@@ -145,6 +141,7 @@ struct
     S.diff st addrs
   let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st
 
+  (* TODO: unused *)
   let kill_lval (host,offset) st =
     let rec last_field os ls =
       match os with
@@ -160,10 +157,7 @@ struct
       | Mem (Lval (Var v, NoOffset)) -> remove_var v st
       | Mem _ ->  top ()
 
-  let elements = S.elements
-  let choose = S.choose
   let filter = S.filter
-  let union = S.union
   let fold = S.fold
 
 end