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

(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 Exc5 {
    public static void main() {
	int i = 0;

	while (i < 20) {
	    i--;

	    try {
		if (i > 10) throw null;
		i += 2;
	    }
	    catch (NullPointerException e) {
		i += 2;
	    }
	}
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Exc5.main()V: Graph of 69 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 68 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) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 68 jbc graph edges to a weighted ITS with 68 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 68 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_7(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_7(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_27(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_27(env, static) -{0,0}> langle_clinit_rangle_New_28(env, static) :|: 0 >= 0
langle_clinit_rangle_New_28(env, static) -{0,0}> langle_clinit_rangle_New_29(env, static) :|: 0 <= static
langle_clinit_rangle_New_29(env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_30(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_33(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, env, static) -{1,1}> langle_init_rangle_Load_35(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{0,0}> main_Load_165(iconst_0, env, static) :|: iconst_0 = 0
main_Load_165(i12, env, static) -{1,1}> main_ConstantStackPush_166(i12, env, static) :|: 0 >= 0
main_ConstantStackPush_166(i12, env, static) -{1,1}> main_GE_176(i12, iconst_20, env, static) :|: iconst_20 = 20
main_GE_176(i19, iconst_20, env, static) -{0,0}> main_GE_177(i19, iconst_20, env, static) :|: iconst_20 = 20 && i19 <= 19
main_GE_176(i20, iconst_20, env, static) -{0,0}> main_GE_178(i20, iconst_20, env, static) :|: iconst_20 = 20 && 20 <= i20
main_GE_177(i19, iconst_20, env, static) -{1,1}> main_Inc_182(i19, env, static) :|: iconst_20 = 20 && i19 < iconst_20 && i19 <= 19
main_Inc_182(i19, env, static) -{1,1}> main_Load_186(i21, env, static) :|: i19 + -1 = i21 && i19 <= 19 && i21 <= 18
main_Load_186(i21, env, static) -{1,1}> main_ConstantStackPush_188(i21, env, static) :|: i21 <= 18
main_ConstantStackPush_188(i21, env, static) -{1,1}> main_LE_193(i21, iconst_10, env, static) :|: iconst_10 = 10 && i21 <= 18
main_LE_193(i26, iconst_10, env, static) -{0,0}> main_LE_194(i26, iconst_10, env, static) :|: i26 <= 18 && i26 <= 10 && iconst_10 = 10
main_LE_193(i27, iconst_10, env, static) -{0,0}> main_LE_195(i27, iconst_10, env, static) :|: i27 <= 18 && iconst_10 = 10 && 11 <= i27
main_LE_194(i26, iconst_10, env, static) -{1,1}> main_Inc_199(i26, env, static) :|: i26 <= 10 && i26 <= iconst_10 && iconst_10 = 10
main_LE_195(i27, iconst_10, env, static) -{1,1}> main_ConstantStackPush_201(i27, env, static) :|: i27 <= 18 && iconst_10 < i27 && iconst_10 = 10 && 11 <= i27
main_Inc_199(i26, env, static) -{1,1}> main_JMP_203(i28, env, static) :|: i26 <= 10 && i28 <= 12 && i26 + 2 = i28
main_ConstantStackPush_201(i27, env, static) -{1,1}> main_AThrow_204(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_JMP_203(i28, env, static) -{1,1}> main_Load_208(i28, env, static) :|: i28 <= 12
main_AThrow_204(NULL, i27, env, static) -{1,1}> main_AThrow_210(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_Load_208(i28, env, static) -{0,0}> main_Load_165(i28, env, static) :|: i28 <= 12
main_AThrow_210(NULL, i27, env, static) -{0,0}> main_AThrow_211(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_AThrow_211(NULL, i27, env, static) -{1,1}> langle_init_rangle_Load_212(o50, i27, env, static) :|: NULL = 0 && 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_212(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_213(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_213(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_214(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_214(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_215(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_215(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_217(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_217(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_219(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_219(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_221(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_221(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_223(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_223(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_224(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_224(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_225(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_225(o50, i27, env, static) -{1,1}> langle_init_rangle_FieldAccess_226(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_FieldAccess_226(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_236(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_236(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_237(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_237(o50, i27, env, static) -{1,1}> langle_init_rangle_StackPop_240(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_StackPop_240(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_241(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_241(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_244(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_244(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_245(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_245(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_246(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_246(o50, i27, env, static) -{1,1}> main_AThrow_248(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_AThrow_248(o50, i27, env, static) -{1,1}> main_Store_249(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Store_249(o50, i27, env, static) -{1,1}> main_Inc_250(i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Inc_250(i27, env, static) -{1,1}> main_JMP_251(i30, env, static) :|: i30 <= 20 && i27 + 2 = i30 && 13 <= i30 && i27 <= 18 && 11 <= i27
main_JMP_251(i30, env, static) -{1,1}> main_Load_252(i30, env, static) :|: i30 <= 20 && 13 <= i30
main_Load_252(i30, env, static) -{0,0}> main_Load_165(i30, env, static) :|: i30 <= 20 && 13 <= i30

(7) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 68 jbc graph edges to a weighted ITS with 68 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(8) Obligation:

IntTrs with 68 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_7(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_7(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_27(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_27(env, static) -{0,0}> langle_clinit_rangle_New_28(env, static) :|: 0 >= 0
langle_clinit_rangle_New_28(env, static) -{0,0}> langle_clinit_rangle_New_29(env, static) :|: 0 <= static
langle_clinit_rangle_New_29(env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_30(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_33(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, env, static) -{1,1}> langle_init_rangle_Load_35(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{0,0}> main_Load_165(iconst_0, env, static) :|: iconst_0 = 0
main_Load_165(i12, env, static) -{1,1}> main_ConstantStackPush_166(i12, env, static) :|: 0 >= 0
main_ConstantStackPush_166(i12, env, static) -{1,1}> main_GE_176(i12, iconst_20, env, static) :|: iconst_20 = 20
main_GE_176(i19, iconst_20, env, static) -{0,0}> main_GE_177(i19, iconst_20, env, static) :|: iconst_20 = 20 && i19 <= 19
main_GE_176(i20, iconst_20, env, static) -{0,0}> main_GE_178(i20, iconst_20, env, static) :|: iconst_20 = 20 && 20 <= i20
main_GE_177(i19, iconst_20, env, static) -{1,1}> main_Inc_182(i19, env, static) :|: iconst_20 = 20 && i19 < iconst_20 && i19 <= 19
main_Inc_182(i19, env, static) -{1,1}> main_Load_186(i21, env, static) :|: i19 + -1 = i21 && i19 <= 19 && i21 <= 18
main_Load_186(i21, env, static) -{1,1}> main_ConstantStackPush_188(i21, env, static) :|: i21 <= 18
main_ConstantStackPush_188(i21, env, static) -{1,1}> main_LE_193(i21, iconst_10, env, static) :|: iconst_10 = 10 && i21 <= 18
main_LE_193(i26, iconst_10, env, static) -{0,0}> main_LE_194(i26, iconst_10, env, static) :|: i26 <= 18 && i26 <= 10 && iconst_10 = 10
main_LE_193(i27, iconst_10, env, static) -{0,0}> main_LE_195(i27, iconst_10, env, static) :|: i27 <= 18 && iconst_10 = 10 && 11 <= i27
main_LE_194(i26, iconst_10, env, static) -{1,1}> main_Inc_199(i26, env, static) :|: i26 <= 10 && i26 <= iconst_10 && iconst_10 = 10
main_LE_195(i27, iconst_10, env, static) -{1,1}> main_ConstantStackPush_201(i27, env, static) :|: i27 <= 18 && iconst_10 < i27 && iconst_10 = 10 && 11 <= i27
main_Inc_199(i26, env, static) -{1,1}> main_JMP_203(i28, env, static) :|: i26 <= 10 && i28 <= 12 && i26 + 2 = i28
main_ConstantStackPush_201(i27, env, static) -{1,1}> main_AThrow_204(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_JMP_203(i28, env, static) -{1,1}> main_Load_208(i28, env, static) :|: i28 <= 12
main_AThrow_204(NULL, i27, env, static) -{1,1}> main_AThrow_210(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_Load_208(i28, env, static) -{0,0}> main_Load_165(i28, env, static) :|: i28 <= 12
main_AThrow_210(NULL, i27, env, static) -{0,0}> main_AThrow_211(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_AThrow_211(NULL, i27, env, static) -{1,1}> langle_init_rangle_Load_212(o50, i27, env, static) :|: NULL = 0 && 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_212(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_213(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_213(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_214(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_214(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_215(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_215(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_217(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_217(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_219(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_219(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_221(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_221(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_223(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_223(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_224(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_224(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_225(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_225(o50, i27, env, static) -{1,1}> langle_init_rangle_FieldAccess_226(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_FieldAccess_226(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_236(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_236(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_237(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_237(o50, i27, env, static) -{1,1}> langle_init_rangle_StackPop_240(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_StackPop_240(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_241(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_241(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_244(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_244(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_245(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_245(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_246(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_246(o50, i27, env, static) -{1,1}> main_AThrow_248(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_AThrow_248(o50, i27, env, static) -{1,1}> main_Store_249(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Store_249(o50, i27, env, static) -{1,1}> main_Inc_250(i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Inc_250(i27, env, static) -{1,1}> main_JMP_251(i30, env, static) :|: i30 <= 20 && i27 + 2 = i30 && 13 <= i30 && i27 <= 18 && 11 <= i27
main_JMP_251(i30, env, static) -{1,1}> main_Load_252(i30, env, static) :|: i30 <= 20 && 13 <= i30
main_Load_252(i30, env, static) -{0,0}> main_Load_165(i30, env, static) :|: i30 <= 20 && 13 <= i30

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

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

(10) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

(11) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 67 jbc graph edges to a weighted ITS with 67 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(12) Obligation:

IntTrs with 67 rules
Start term: main_ConstantStackPush_2(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_7(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_7(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_25(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_27(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_27(env, static) -{0,0}> langle_clinit_rangle_New_28(env, static) :|: 0 >= 0
langle_clinit_rangle_New_28(env, static) -{0,0}> langle_clinit_rangle_New_29(env, static) :|: 0 <= static
langle_clinit_rangle_New_29(env, static) -{1,1}> langle_clinit_rangle_Duplicate_30(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_30(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_33(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_34(o2, env, static) -{1,1}> langle_init_rangle_Load_35(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_35(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, env, static) -{1,1}> langle_init_rangle_Return_38(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{0,0}> main_Load_165(iconst_0, env, static) :|: iconst_0 = 0
main_Load_165(i12, env, static) -{1,1}> main_ConstantStackPush_166(i12, env, static) :|: 0 >= 0
main_ConstantStackPush_166(i12, env, static) -{1,1}> main_GE_176(i12, iconst_20, env, static) :|: iconst_20 = 20
main_GE_176(i19, iconst_20, env, static) -{0,0}> main_GE_177(i19, iconst_20, env, static) :|: iconst_20 = 20 && i19 <= 19
main_GE_177(i19, iconst_20, env, static) -{1,1}> main_Inc_182(i19, env, static) :|: iconst_20 = 20 && i19 < iconst_20 && i19 <= 19
main_Inc_182(i19, env, static) -{1,1}> main_Load_186(i21, env, static) :|: i19 + -1 = i21 && i19 <= 19 && i21 <= 18
main_Load_186(i21, env, static) -{1,1}> main_ConstantStackPush_188(i21, env, static) :|: i21 <= 18
main_ConstantStackPush_188(i21, env, static) -{1,1}> main_LE_193(i21, iconst_10, env, static) :|: iconst_10 = 10 && i21 <= 18
main_LE_193(i26, iconst_10, env, static) -{0,0}> main_LE_194(i26, iconst_10, env, static) :|: i26 <= 18 && i26 <= 10 && iconst_10 = 10
main_LE_193(i27, iconst_10, env, static) -{0,0}> main_LE_195(i27, iconst_10, env, static) :|: i27 <= 18 && iconst_10 = 10 && 11 <= i27
main_LE_194(i26, iconst_10, env, static) -{1,1}> main_Inc_199(i26, env, static) :|: i26 <= 10 && i26 <= iconst_10 && iconst_10 = 10
main_LE_195(i27, iconst_10, env, static) -{1,1}> main_ConstantStackPush_201(i27, env, static) :|: i27 <= 18 && iconst_10 < i27 && iconst_10 = 10 && 11 <= i27
main_Inc_199(i26, env, static) -{1,1}> main_JMP_203(i28, env, static) :|: i26 <= 10 && i28 <= 12 && i26 + 2 = i28
main_ConstantStackPush_201(i27, env, static) -{1,1}> main_AThrow_204(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_JMP_203(i28, env, static) -{1,1}> main_Load_208(i28, env, static) :|: i28 <= 12
main_AThrow_204(NULL, i27, env, static) -{1,1}> main_AThrow_210(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_Load_208(i28, env, static) -{0,0}> main_Load_165(i28, env, static) :|: i28 <= 12
main_AThrow_210(NULL, i27, env, static) -{0,0}> main_AThrow_211(NULL, i27, env, static) :|: NULL = 0 && i27 <= 18 && 11 <= i27
main_AThrow_211(NULL, i27, env, static) -{1,1}> langle_init_rangle_Load_212(o50, i27, env, static) :|: NULL = 0 && 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_212(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_213(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_213(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_214(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_214(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_215(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_215(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_217(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_217(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_219(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_219(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_221(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_221(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_223(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_223(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_224(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_224(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_225(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_225(o50, i27, env, static) -{1,1}> langle_init_rangle_FieldAccess_226(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_FieldAccess_226(o50, i27, env, static) -{1,1}> langle_init_rangle_Load_236(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Load_236(o50, i27, env, static) -{1,1}> langle_init_rangle_InvokeMethod_237(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_InvokeMethod_237(o50, i27, env, static) -{1,1}> langle_init_rangle_StackPop_240(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_StackPop_240(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_241(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_241(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_244(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_244(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_245(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_245(o50, i27, env, static) -{1,1}> langle_init_rangle_Return_246(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
langle_init_rangle_Return_246(o50, i27, env, static) -{1,1}> main_AThrow_248(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_AThrow_248(o50, i27, env, static) -{1,1}> main_Store_249(o50, i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Store_249(o50, i27, env, static) -{1,1}> main_Inc_250(i27, env, static) :|: 0 < o50 && i27 <= 18 && 11 <= i27
main_Inc_250(i27, env, static) -{1,1}> main_JMP_251(i30, env, static) :|: i30 <= 20 && i27 + 2 = i30 && 13 <= i30 && i27 <= 18 && 11 <= i27
main_JMP_251(i30, env, static) -{1,1}> main_Load_252(i30, env, static) :|: i30 <= 20 && 13 <= i30
main_Load_252(i30, env, static) -{0,0}> main_Load_165(i30, env, static) :|: i30 <= 20 && 13 <= i30

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

Constructed TerminationGraph.

(14) Obligation:

Termination Graph based on JBC Program:
Exc5.main()V: Graph of 395 nodes with 0 SCCs.

(15) TerminationGraphToComplexityProof (EQUIVALENT transformation)

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

(16) BOUNDS(CONSTANT, 385)