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