package j

func f(try func() int, shouldInc func() bool, N func(int) int) {
	var n int
loop: // we want to have 3 preds here, the function entry and both gotos
	if v := try(); v == 42 || v == 1337 { // the two || are to trick findIndVar
		if n < 30 { // this aims to be the matched block
			if shouldInc() {
				n++
				goto loop
			}
			n = N(n) // try to prevent some block joining
			goto loop
		}
	}

		inc = nxt.Args[1]
	} else if nxt.Args[1] == ind { // nxt = inc + ind
		inc = nxt.Args[0]
	} else {
		panic("unreachable") // one of the cases must be true from the above.
	}

	return
}

// findIndVar finds induction variables in a function.
//
// Look for variables and blocks that satisfy the following
//
//	 loop:
//	   ind = (Phi min nxt),
//	   if ind < max
//	     then goto enter_loop

	}
}

// addLocalInductiveFacts adds inductive facts when visiting b, where
// b is a join point in a loop. In contrast with findIndVar, this
// depends on facts established for b, which is why it happens when
// visiting b.
//
// TODO: It would be nice to combine this with findIndVar.
func addLocalInductiveFacts(ft *factsTable, b *Block) {
	// This looks for a specific pattern of induction:
	//

func constsuffix(s string) bool {
	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
}

// oforuntil tests the pattern created by OFORUNTIL blocks. These are
// handled by addLocalInductiveFacts rather than findIndVar.
func oforuntil(b []int) {
	i := 0
	if len(b) > i {
	top:
		println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
		i++
		if i < len(b) {
			goto top
		}