Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package ClassAnalysis;

public class ClassAnalysis {
	A field;

	public static void main(String[] args) {
		Random.args = args;
		ClassAnalysis t = new ClassAnalysis();
		t.field = new A();
		t.field = new B();
		t.eval();
	}

	public void eval() {
		int x = Random.random() % 100;
		this.field.test(x);
	}
}

class A {
	public boolean test(int x) {
		while (x > 0) {
			if (x > 10) {
				x--;
			} else {
				x++;
			}
		}
		return true;
	}
}

class B extends A {
	public boolean test(int x) {
		while (x > 0) {
			x--;
		}
		return true;
	}
}


package ClassAnalysis;

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

ClassAnalysis.ClassAnalysis.eval()V: Graph of 86 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: ClassAnalysis.ClassAnalysis.eval()V
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:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f366_0_test_LE(EOS, i56, i56) → f419_0_test_LE(EOS, i56, i56)
f419_0_test_LE(EOS, i56, i56) → f433_0_test_Inc(EOS, i56) | >(i56, 0)
f433_0_test_Inc(EOS, i56) → f439_0_test_JMP(EOS, +(i56, -1)) | >(i56, 0)
f439_0_test_JMP(EOS, i58) → f452_0_test_Load(EOS, i58)
f452_0_test_Load(EOS, i58) → f353_0_test_Load(EOS, i58)
f353_0_test_Load(EOS, i35) → f366_0_test_LE(EOS, i35, i35)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f366_0_test_LE(x1, x2, x3) → f366_0_test_LE(x2, x3)
Cond_f366_0_test_LE(x1, x2, x3, x4) → Cond_f366_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f366_0_test_LE(x1, x2) → f366_0_test_LE(x2)
Cond_f366_0_test_LE(x1, x2, x3) → Cond_f366_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

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

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f366_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(8) YES