Predicate StackVariableReachability::bbSuccessorEntryReachesLoopInvariant

DEPRECATED: use the corresponding predicate in LocalScopeVariableReachability instead.

Loop invariant for bbSuccessorEntryReaches:

  • succ is a successor of pred.
  • predSkipsFirstLoopAlwaysTrueUponEntry: whether the path from pred (via succ) skips the first loop where the condition is provably true upon entry.
  • succSkipsFirstLoopAlwaysTrueUponEntry: whether the path from succ skips the first loop where the condition is provably true upon entry.
  • If pred contains the entry point of a loop where the condition is provably true upon entry, then succ is not allowed to skip that loop (succSkipsFirstLoopAlwaysTrueUponEntry = false).
predicate bbSuccessorEntryReachesLoopInvariant(BasicBlock pred, BasicBlock succ, boolean predSkipsFirstLoopAlwaysTrueUponEntry, boolean succSkipsFirstLoopAlwaysTrueUponEntry)