infer_clone/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl

property SkipAfterRemove
  prefix "ArrayList"
  start -> start: *
  start -> removed: remove(Collection, Index)
  removed -> ok:    get(collection, index)
  removed -> error: get(collection, J) if j != index
[topl] Support side conditions for transitions. Summary: In addition to state1 -> state2: pattern one can now also write state1 -> state2: pattern if condition where "condition" is some conjunction of comparisons (==,<,>) that involve variables bound by "pattern", registers of the automaton, and constants. Reviewed By: ngorogiannis Differential Revision: D19035496 fbshipit-source-id: 6f6e6a9be 5 years ago			`property SkipAfterRemove`
			`prefix "ArrayList"`
			`start -> start: *`
			`start -> removed: remove(Collection, Index)`
			`removed -> ok: get(collection, index)`
			`removed -> error: get(collection, J) if j != index`