Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class CAppE {
	CAppE next;

	public static void main(String[] args) {
		Random.args = args;
		CAppE list = createList();
		cappE(Random.random());
	}

	public static void cappE(int j) {
		CAppE a = new CAppE();
		if (j > 0) {
			a.appE(j);
			while (a.next == null) {}
		}
	}

	public void appE(int i) {
		if (next == null) {
			if (i <= 0) {
				return;
			} else {
				next = new CAppE();
			}
			i--;
	 	}
		next.appE(i);
	}

	public static CAppE createList() {
		CAppE result = null;
		int length = Random.random();
		while (length > 0) {
			result = new CAppE(result);
			length--;
		}
		return result;
	}

	public CAppE() {
		this.next = null;
	}

	public CAppE(CAppE n) {
		this.next = n;
	}
}

class Random {
	static String[] args;
	static int index = 0;

	public static int random() {
		String string = args[index];
		index++;
		return string.length();
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

CAppE.createList()LCAppE;: Graph of 91 nodes with 1 SCC.

CAppE.appE(I)V: Graph of 35 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CAppE.appE(I)V
SCC calls the following helper methods: CAppE.appE(I)V
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
  • CAppE: [next]
• Marker field analysis yielded the following relations that could be markers:
  

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f769_0_appE_FieldAccess(EOS, i99, i99) → f771_0_appE_NONNULL(EOS, i99, i99)
f771_0_appE_NONNULL(EOS, i99, i99) → f773_0_appE_Load(EOS, i99, i99)
f773_0_appE_Load(EOS, i99, i99) → f774_0_appE_GT(EOS, i99, i99, i99)
f774_0_appE_GT(EOS, i101, i101, i101) → f776_0_appE_GT(EOS, i101, i101, i101)
f776_0_appE_GT(EOS, i101, i101, i101) → f779_0_appE_Load(EOS, i101, i101) | >(i101, 0)
f779_0_appE_Load(EOS, i101, i101) → f783_0_appE_New(EOS, i101, i101)
f783_0_appE_New(EOS, i101, i101) → f794_0_appE_Duplicate(EOS, i101, i101)
f794_0_appE_Duplicate(EOS, i101, i101) → f797_0_appE_InvokeMethod(EOS, i101, i101)
f797_0_appE_InvokeMethod(EOS, i101, i101) → f799_0__init__Load(EOS, i101, i101)
f799_0__init__Load(EOS, i101, i101) → f801_0__init__InvokeMethod(EOS, i101, i101)
f801_0__init__InvokeMethod(EOS, i101, i101) → f803_0__init__Load(EOS, i101, i101)
f803_0__init__Load(EOS, i101, i101) → f805_0__init__ConstantStackPush(EOS, i101, i101)
f805_0__init__ConstantStackPush(EOS, i101, i101) → f807_0__init__FieldAccess(EOS, i101, i101)
f807_0__init__FieldAccess(EOS, i101, i101) → f809_0__init__Return(EOS, i101, i101)
f809_0__init__Return(EOS, i101, i101) → f811_0_appE_FieldAccess(EOS, i101, i101)
f811_0_appE_FieldAccess(EOS, i101, i101) → f815_0_appE_Inc(EOS, i101, i101)
f815_0_appE_Inc(EOS, i101, i101) → f817_0_appE_Load(EOS, i101, +(i101, -1)) | >(i101, 0)
f817_0_appE_Load(EOS, i101, i106) → f819_0_appE_FieldAccess(EOS, i101, i106)
f819_0_appE_FieldAccess(EOS, i101, i106) → f821_0_appE_Load(EOS, i101, i106)
f821_0_appE_Load(EOS, i101, i106) → f823_0_appE_InvokeMethod(EOS, i101, i106)
f823_0_appE_InvokeMethod(EOS, i101, i106) → f825_0_appE_Load(EOS, i106, i106)
f823_0_appE_InvokeMethod(EOS, i101, i106) → f825_1_appE_Load(EOS, i101, i106, i106)
f825_0_appE_Load(EOS, i106, i106) → f828_0_appE_Load(EOS, i106, i106)
f828_0_appE_Load(EOS, i106, i106) → f766_0_appE_Load(EOS, i106, i106)
f766_0_appE_Load(EOS, i99, i99) → f769_0_appE_FieldAccess(EOS, i99, i99)

Combined rules. Obtained 2 IRules

P rules:
f769_0_appE_FieldAccess(EOS, x0, x0) → f825_1_appE_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f769_0_appE_FieldAccess(EOS, x0, x0) → f769_0_appE_FieldAccess(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f769_0_appE_FieldAccess(x1, x2, x3) → f769_0_appE_FieldAccess(x2, x3)
Cond_f769_0_appE_FieldAccess(x1, x2, x3, x4) → Cond_f769_0_appE_FieldAccess(x1, x3, x4)
f825_1_appE_Load(x1, x2, x3, x4) → f825_1_appE_Load(x2, x3, x4)
Cond_f769_0_appE_FieldAccess1(x1, x2, x3, x4) → Cond_f769_0_appE_FieldAccess1(x1, x3, x4)

Filtered duplicate terms:

f769_0_appE_FieldAccess(x1, x2) → f769_0_appE_FieldAccess(x2)
Cond_f769_0_appE_FieldAccess(x1, x2, x3) → Cond_f769_0_appE_FieldAccess(x1, x3)
f825_1_appE_Load(x1, x2, x3) → f825_1_appE_Load(x3)
Cond_f769_0_appE_FieldAccess1(x1, x2, x3) → Cond_f769_0_appE_FieldAccess1(x1, x3)

Filtered unneeded terms:

Cond_f769_0_appE_FieldAccess(x1, x2) → Cond_f769_0_appE_FieldAccess(x1)

Prepared 2 rules for path length conversion:

P rules:
f769_0_appE_FieldAccess(x0) → f825_1_appE_Load(-(x0, 1)) | >(x0, 0)
f769_0_appE_FieldAccess(x0) → f769_0_appE_FieldAccess(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f769_0_appE_FieldAccess(x1) → f769_0_appE_FieldAccess(-(x1, 1)) | >(x1, 0)

(7) Obligation:

Rules:
f769_0_appE_FieldAccess(x1) → f769_0_appE_FieldAccess(-(x1, 1)) | >(x1, 0)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f769_0_appE_FieldAccess(x2)] = x2

Therefore the following rule(s) have been dropped:

f769_0_appE_FieldAccess(x0) → f769_0_appE_FieldAccess(-(x0, 1)) | >(x0, 0)

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CAppE.createList()LCAppE;
SCC calls the following helper methods:
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
• Marker field analysis yielded the following relations that could be markers:
  

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f381_0_createList_LE(EOS, i43, i43) → f389_0_createList_LE(EOS, i43, i43)
f389_0_createList_LE(EOS, i43, i43) → f416_0_createList_New(EOS, i43) | >(i43, 0)
f416_0_createList_New(EOS, i43) → f439_0_createList_Duplicate(EOS, i43)
f439_0_createList_Duplicate(EOS, i43) → f448_0_createList_Load(EOS, i43)
f448_0_createList_Load(EOS, i43) → f464_0_createList_InvokeMethod(EOS, i43)
f464_0_createList_InvokeMethod(EOS, i43) → f468_0__init__Load(EOS, i43)
f468_0__init__Load(EOS, i43) → f472_0__init__InvokeMethod(EOS, i43)
f472_0__init__InvokeMethod(EOS, i43) → f482_0__init__Load(EOS, i43)
f482_0__init__Load(EOS, i43) → f485_0__init__Load(EOS, i43)
f485_0__init__Load(EOS, i43) → f487_0__init__FieldAccess(EOS, i43)
f487_0__init__FieldAccess(EOS, i43) → f491_0__init__Return(EOS, i43)
f491_0__init__Return(EOS, i43) → f493_0_createList_Store(EOS, i43)
f493_0_createList_Store(EOS, i43) → f497_0_createList_Inc(EOS, i43)
f497_0_createList_Inc(EOS, i43) → f501_0_createList_JMP(EOS, +(i43, -1)) | >(i43, 0)
f501_0_createList_JMP(EOS, i71) → f509_0_createList_Load(EOS, i71)
f509_0_createList_Load(EOS, i71) → f373_0_createList_Load(EOS, i71)
f373_0_createList_Load(EOS, i38) → f381_0_createList_LE(EOS, i38, i38)

Combined rules. Obtained 1 IRules

P rules:
f381_0_createList_LE(EOS, x0, x0) → f381_0_createList_LE(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f381_0_createList_LE(x1, x2, x3) → f381_0_createList_LE(x2, x3)
Cond_f381_0_createList_LE(x1, x2, x3, x4) → Cond_f381_0_createList_LE(x1, x3, x4)

Filtered duplicate terms:

f381_0_createList_LE(x1, x2) → f381_0_createList_LE(x2)
Cond_f381_0_createList_LE(x1, x2, x3) → Cond_f381_0_createList_LE(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f381_0_createList_LE(x0) → f381_0_createList_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f381_0_createList_LE(x0) → f381_0_createList_LE(-(x0, 1)) | >(x0, 0)

(12) Obligation:

Rules:
f381_0_createList_LE(x0) → f381_0_createList_LE(-(x0, 1)) | >(x0, 0)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f381_0_createList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

f381_0_createList_LE(x0) → f381_0_createList_LE(-(x0, 1)) | >(x0, 0)

(14) YES