LoopInvariant (infer.Checkers.LoopInvariant)

module InvariantVars : sig ... end

module VarsInLoop : sig ... end

module LoopNodes : sig ... end

module VarSet : sig ... end

module LoopHeadToLoopNodes = IR.Procdesc.NodeMap

Map loop header node -> all nodes in the loop

module LoopHeadToInvVars = IR.Procdesc.NodeMap

Map loop head -> invariant vars in loop

type invariant_map = VarsInLoop.t IR.Procdesc.NodeMap.t

val get_inv_vars_in_loop : 
  IR.Tenv.t ->
  ReachingDefs.invariant_map ->
  is_pure_by_default:bool ->
  get_callee_purity:
    (IR.Procname.t ->
      PurityDomain.ModifiedParamIndices.t
        Absint.AbstractDomain.Types.top_lifted
        option) ->
  IR.Procdesc.Node.t ->
  LoopNodes.t ->
  VarSet.t

val get_loop_inv_var_map : 
  IR.Tenv.t ->
  (IR.Procname.t ->
    PurityDomain.ModifiedParamIndices.t Absint.AbstractDomain.Types.top_lifted
      option) ->
  ReachingDefs.invariant_map ->
  LoopNodes.t LoopHeadToInvVars.t ->
  invariant_map