The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 388).

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * A loop continously throwing and catching an exception.
 * The exception is thrown before the statement that makes the loop
 * progress, but the exception body contains another statement making the
 * loop progress.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate.
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class Exc3 {
    public static void main(String[] args) {
	int i = 0;

	while (i < 20) {
	    try {
		if (i > 10) throw null;
		i++;
	    }
	    catch (NullPointerException e) {
		i++;
	    }
	}
    }
}

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Exc3.main([Ljava/lang/String;)V: Graph of 78 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

Extracted set of 77 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 77 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  

Considered paths: nonterm paths and paths from start to sinks

(5) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

Extracted set of 76 edges for the analysis of TIME complexity. Dropped leaves.

(6) Obligation:

Set of 76 edges based on JBC Program.
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

(7) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(8) Obligation:

Termination Graph based on JBC Program:
Exc3.main([Ljava/lang/String;)V: Graph of 398 nodes with 0 SCCs.

(9) TerminationGraphToComplexityProof (EQUIVALENT transformation)

Proven constant complexity by absence of SCCs and edges with non-constant weight

(10) BOUNDS(CONSTANT, 388)