Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 1080 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 144 ms)
        ↳7 intTRS
        ↳8 LinearRankingProcessor (⇔, 19 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 64 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 0 ms)
        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:
package SharingAnalysis;

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

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


package SharingAnalysis;

public class SharingAnalysis {
	int val;
	SharingAnalysis field;

	public static void main(String[] args) {
		Random.args = args;
		SharingAnalysis t1 = new SharingAnalysis();
		SharingAnalysis t2 = t1.appendNewList(1);
		SharingAnalysis t3 = t2.appendNewList(Random.random());
		t2.field = null;
		copy(t1, t3);
	}

	public static void copy(SharingAnalysis source, SharingAnalysis target) {
		while (source != null) {
			SharingAnalysis newEle = new SharingAnalysis();
			newEle.val = source.val;
			target.field = newEle;
			source = source.field;
			target = target.field;
		}
	}

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private SharingAnalysis appendNewList(int i) {
		this.field = new SharingAnalysis();
		SharingAnalysis cur = this.field;
		while (i > 1) {
			i--;
			cur = cur.field = new SharingAnalysis();
		}
		return cur;
	}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
SharingAnalysis.SharingAnalysis.main([Ljava/lang/String;)V: Graph of 237 nodes with 2 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: SharingAnalysis.SharingAnalysis.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • SharingAnalysis.SharingAnalysis: [val, field]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 64 IRules

P rules:
f1432_0_copy_NULL(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1434_0_copy_NULL(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1434_0_copy_NULL(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1437_0_copy_New(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1437_0_copy_New(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1441_0_copy_Duplicate(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1441_0_copy_Duplicate(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1444_0_copy_InvokeMethod(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1444_0_copy_InvokeMethod(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1447_0__init__Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1447_0__init__Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1452_0__init__InvokeMethod(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1452_0__init__InvokeMethod(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1458_0__init__Return(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1458_0__init__Return(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1460_0_copy_Store(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1460_0_copy_Store(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1462_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1462_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1463_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1463_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1464_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1464_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766) → f1471_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(o780sub), java.lang.Object(o780sub), o767[SharingAnalysis.field]o766)
f1464_0_copy_FieldAccess(EOS, java.lang.Object(o794sub), java.lang.Object(o794sub), java.lang.Object(o794sub), o767[SharingAnalysis.field]o766) → f1472_0_copy_FieldAccess(EOS, java.lang.Object(o794sub), java.lang.Object(o794sub), java.lang.Object(o794sub), o767[SharingAnalysis.field]o766)
f1471_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1473_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1473_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1475_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1475_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1482_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1482_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1489_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1489_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1495_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1495_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1514_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) | >(o767[SharingAnalysis.field]o766, 0)
f1495_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1515_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)))
f1514_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1535_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1535_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1555_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766)
f1555_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)), o767[SharingAnalysis.field]o766) → f1572_0_copy_Store(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766)
f1572_0_copy_Store(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766) → f1578_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766)
f1578_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766) → f1595_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766)
f1595_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o766) → f1610_0_copy_Store(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781)
f1610_0_copy_Store(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781) → f1624_0_copy_JMP(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781)
f1624_0_copy_JMP(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781) → f1645_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781)
f1645_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781) → f1430_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o767[SharingAnalysis.field]o781)
f1430_0_copy_Load(EOS, java.lang.Object(o768sub), o765, o767[SharingAnalysis.field]o766) → f1432_0_copy_NULL(EOS, java.lang.Object(o768sub), o765, o765, o767[SharingAnalysis.field]o766)
f1515_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796))) → f1541_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)))
f1541_0_copy_Load(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796))) → f1559_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796)))
f1559_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i116, o796))) → f1573_0_copy_Store(EOS, java.lang.Object(o768sub), o796)
f1573_0_copy_Store(EOS, java.lang.Object(o768sub), o796) → f1582_0_copy_Load(EOS, java.lang.Object(o768sub), o796)
f1582_0_copy_Load(EOS, java.lang.Object(o768sub), o796) → f1599_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), o796)
f1599_0_copy_FieldAccess(EOS, java.lang.Object(o768sub), o796) → f1613_0_copy_Store(EOS, java.lang.Object(o768sub), o796)
f1613_0_copy_Store(EOS, java.lang.Object(o768sub), o796) → f1627_0_copy_JMP(EOS, java.lang.Object(o768sub), o796)
f1627_0_copy_JMP(EOS, java.lang.Object(o768sub), o796) → f1652_0_copy_Load(EOS, java.lang.Object(o768sub), o796)
f1652_0_copy_Load(EOS, java.lang.Object(o768sub), o796) → f1430_0_copy_Load(EOS, java.lang.Object(o768sub), o796, o837[SharingAnalysis.field]o781) | =(o837[SharingAnalysis.field]o781, 1)
f1472_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1474_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1474_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1479_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1479_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1487_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1487_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1493_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1493_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1501_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1501_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1529_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) | >(o767[SharingAnalysis.field]o766, 0)
f1501_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1530_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)))
f1529_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1545_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1545_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1564_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766)
f1564_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o767[SharingAnalysis.field]o766) → f1574_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766)
f1574_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766) → f1587_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766)
f1587_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766) → f1603_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766)
f1603_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o766) → f1617_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781)
f1617_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781) → f1631_0_copy_JMP(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781)
f1631_0_copy_JMP(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781) → f1660_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781)
f1660_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781) → f1430_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o767[SharingAnalysis.field]o781)
f1530_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798))) → f1553_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)))
f1553_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798))) → f1571_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)))
f1571_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798))) → f1576_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1576_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1593_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1593_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1608_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1608_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1622_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1622_0_copy_Store(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1637_0_copy_JMP(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1637_0_copy_JMP(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1669_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798)
f1669_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798) → f1430_0_copy_Load(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i117, o798)), o798, o840[SharingAnalysis.field]o781) | =(o840[SharingAnalysis.field]o781, 1)

Combined rules. Obtained 4 IRules

P rules:
f1432_0_copy_NULL(EOS, java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2)), x3) → f1432_0_copy_NULL(EOS, java.lang.Object(x0), x2, x2, x4) | >(x3, 0)
f1432_0_copy_NULL(EOS, java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2)), x3) → f1432_0_copy_NULL(EOS, java.lang.Object(x0), x2, x2, 1)
f1432_0_copy_NULL(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), x2) → f1432_0_copy_NULL(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), x1, x1, x3) | >(x2, 0)
f1432_0_copy_NULL(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), x2) → f1432_0_copy_NULL(EOS, java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), x1, x1, 1)

Filtered ground terms:


f1432_0_copy_NULL(x1, x2, x3, x4, x5) → f1432_0_copy_NULL(x2, x3, x4, x5)
Cond_f1432_0_copy_NULL(x1, x2, x3, x4, x5, x6, x7) → Cond_f1432_0_copy_NULL(x1, x3, x4, x5, x6, x7)
Cond_f1432_0_copy_NULL1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1432_0_copy_NULL1(x1, x3, x4, x5, x6, x7)
SharingAnalysis.SharingAnalysis(x1, x2, x3) → SharingAnalysis.SharingAnalysis(x2, x3)

Filtered duplicate terms:


f1432_0_copy_NULL(x1, x2, x3, x4) → f1432_0_copy_NULL(x1, x3, x4)
Cond_f1432_0_copy_NULL(x1, x2, x3, x4, x5, x6) → Cond_f1432_0_copy_NULL(x1, x2, x4, x5, x6)
Cond_f1432_0_copy_NULL1(x1, x2, x3, x4, x5, x6) → Cond_f1432_0_copy_NULL1(x1, x4, x5, x6)

Filtered unneeded terms:


Cond_f1432_0_copy_NULL(x1, x2, x3, x4, x5) → Cond_f1432_0_copy_NULL(x1, x2, x3, x5)
SharingAnalysis.SharingAnalysis(x1, x2) → SharingAnalysis.SharingAnalysis(x2)
Cond_f1432_0_copy_NULL1(x1, x2, x3, x4) → Cond_f1432_0_copy_NULL1(x1, x2, x4)

Prepared 4 rules for path length conversion:

P rules:
f1432_0_copy_NULL(java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(x2)), x3) → f1432_0_copy_NULL(java.lang.Object(x0), x2, x4) | >(x3, 0)
f1432_0_copy_NULL(java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(x2)), x3) → f1432_0_copy_NULL(java.lang.Object(x0), x2, 1)
f1432_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x2) → f1432_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x1, x3) | >(x2, 0)
f1432_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x2) → f1432_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x1, 1)

Finished conversion. Obtained 4 rules.

P rules:
f1432_0_copy_NULL(v15, v16, x2) → f1432_0_copy_NULL(v17, v18, x3) | &&(&&(&&(&&(&&(&&(>(x2, 0), >(+(v18, 1), 0)), <=(+(v18, 1), v16)), >(+(v17, 1), 1)), <=(v17, v15)), >(+(v16, 1), 1)), >(+(v15, 1), 1))
f1432_0_copy_NULL(v19, v20, x6) → f1432_0_copy_NULL(v21, v22, 1) | &&(&&(&&(&&(&&(>(+(v22, 1), 0), <=(+(v22, 1), v20)), >(+(v21, 1), 1)), <=(v21, v19)), >(+(v20, 1), 1)), >(+(v19, 1), 1))
f1432_0_copy_NULL(v23, v24, x8) → f1432_0_copy_NULL(v25, v26, x9) | &&(&&(&&(&&(&&(&&(&&(&&(>(x8, 0), >(+(v26, 1), 0)), <=(+(v26, 1), v24)), <=(+(v26, 1), v23)), >(+(v25, 1), 1)), <=(v25, v24)), <=(v25, v23)), >(+(v24, 1), 1)), >(+(v23, 1), 1))
f1432_0_copy_NULL(v27, v28, x11) → f1432_0_copy_NULL(v29, v30, 1) | &&(&&(&&(&&(&&(&&(&&(>(+(v30, 1), 0), <=(+(v30, 1), v28)), <=(+(v30, 1), v27)), >(+(v29, 1), 1)), <=(v29, v28)), <=(v29, v27)), >(+(v28, 1), 1)), >(+(v27, 1), 1))

(7) Obligation:

Rules:
f1432_0_copy_NULL(v15, v16, x2) → f1432_0_copy_NULL(v17, v18, x3) | &&(&&(&&(&&(&&(&&(>(x2, 0), >(+(v18, 1), 0)), <=(+(v18, 1), v16)), >(+(v17, 1), 1)), <=(v17, v15)), >(+(v16, 1), 1)), >(+(v15, 1), 1))
f1432_0_copy_NULL(v19, v20, x6) → f1432_0_copy_NULL(v21, v22, 1) | &&(&&(&&(&&(&&(>(+(v22, 1), 0), <=(+(v22, 1), v20)), >(+(v21, 1), 1)), <=(v21, v19)), >(+(v20, 1), 1)), >(+(v19, 1), 1))
f1432_0_copy_NULL(v23, v24, x8) → f1432_0_copy_NULL(v25, v26, x9) | &&(&&(&&(&&(&&(&&(&&(&&(>(x8, 0), >(+(v26, 1), 0)), <=(+(v26, 1), v24)), <=(+(v26, 1), v23)), >(+(v25, 1), 1)), <=(v25, v24)), <=(v25, v23)), >(+(v24, 1), 1)), >(+(v23, 1), 1))
f1432_0_copy_NULL(v27, v28, x11) → f1432_0_copy_NULL(v29, v30, 1) | &&(&&(&&(&&(&&(&&(&&(>(+(v30, 1), 0), <=(+(v30, 1), v28)), <=(+(v30, 1), v27)), >(+(v29, 1), 1)), <=(v29, v28)), <=(v29, v27)), >(+(v28, 1), 1)), >(+(v27, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1432_0_copy_NULL(x)] = 1·x2

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


f1432_0_copy_NULL(x0, x1, x2) → f1432_0_copy_NULL(x3, x4, x5) | &&(&&(&&(&&(&&(&&(>(x2, 0), >(+(x4, 1), 0)), <=(+(x4, 1), x1)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 1))
f1432_0_copy_NULL(x6, x7, x8) → f1432_0_copy_NULL(x9, x10, 1) | &&(&&(&&(&&(&&(>(+(x10, 1), 0), <=(+(x10, 1), x7)), >(+(x9, 1), 1)), <=(x9, x6)), >(+(x7, 1), 1)), >(+(x6, 1), 1))
f1432_0_copy_NULL(x11, x12, x13) → f1432_0_copy_NULL(x14, x15, x16) | &&(&&(&&(&&(&&(&&(&&(&&(>(x13, 0), >(+(x15, 1), 0)), <=(+(x15, 1), x12)), <=(+(x15, 1), x11)), >(+(x14, 1), 1)), <=(x14, x12)), <=(x14, x11)), >(+(x12, 1), 1)), >(+(x11, 1), 1))
f1432_0_copy_NULL(x17, x18, x19) → f1432_0_copy_NULL(x20, x21, 1) | &&(&&(&&(&&(&&(&&(&&(>(+(x21, 1), 0), <=(+(x21, 1), x18)), <=(+(x21, 1), x17)), >(+(x20, 1), 1)), <=(x20, x18)), <=(x20, x17)), >(+(x18, 1), 1)), >(+(x17, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: SharingAnalysis.SharingAnalysis.main([Ljava/lang/String;)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:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f430_0_appendNewList_ConstantStackPush(EOS, i32, i32, o72[SharingAnalysis.field]o69) → f433_0_appendNewList_LE(EOS, i32, i32, 1, o72[SharingAnalysis.field]o69)
f433_0_appendNewList_LE(EOS, i47, i47, matching1, o72[SharingAnalysis.field]o69) → f438_0_appendNewList_LE(EOS, i47, i47, 1, o72[SharingAnalysis.field]o69) | =(matching1, 1)
f438_0_appendNewList_LE(EOS, i47, i47, matching1, o72[SharingAnalysis.field]o69) → f440_0_appendNewList_Inc(EOS, i47, o72[SharingAnalysis.field]o69) | &&(>(i47, 1), =(matching1, 1))
f440_0_appendNewList_Inc(EOS, i47, o72[SharingAnalysis.field]o69) → f444_0_appendNewList_Load(EOS, +(i47, -1), o72[SharingAnalysis.field]o69) | >(i47, 0)
f444_0_appendNewList_Load(EOS, i48, o72[SharingAnalysis.field]o69) → f449_0_appendNewList_New(EOS, i48, o72[SharingAnalysis.field]o69)
f449_0_appendNewList_New(EOS, i48, o72[SharingAnalysis.field]o69) → f454_0_appendNewList_Duplicate(EOS, i48, o72[SharingAnalysis.field]o69)
f454_0_appendNewList_Duplicate(EOS, i48, o72[SharingAnalysis.field]o69) → f458_0_appendNewList_InvokeMethod(EOS, i48, o72[SharingAnalysis.field]o69)
f458_0_appendNewList_InvokeMethod(EOS, i48, o72[SharingAnalysis.field]o69) → f463_0__init__Load(EOS, i48, o72[SharingAnalysis.field]o69)
f463_0__init__Load(EOS, i48, o72[SharingAnalysis.field]o69) → f474_0__init__InvokeMethod(EOS, i48, o72[SharingAnalysis.field]o69)
f474_0__init__InvokeMethod(EOS, i48, o72[SharingAnalysis.field]o69) → f482_0__init__Return(EOS, i48, o72[SharingAnalysis.field]o69)
f482_0__init__Return(EOS, i48, o72[SharingAnalysis.field]o69) → f486_0_appendNewList_Duplicate(EOS, i48, o72[SharingAnalysis.field]o69)
f486_0_appendNewList_Duplicate(EOS, i48, o72[SharingAnalysis.field]o69) → f488_0_appendNewList_FieldAccess(EOS, i48, o72[SharingAnalysis.field]o69)
f488_0_appendNewList_FieldAccess(EOS, i48, o72[SharingAnalysis.field]o69) → f526_0_appendNewList_FieldAccess(EOS, i48, o72[SharingAnalysis.field]o69) | >(o72[SharingAnalysis.field]o69, 0)
f488_0_appendNewList_FieldAccess(EOS, i48, o72[SharingAnalysis.field]o69) → f527_0_appendNewList_FieldAccess(EOS, i48)
f526_0_appendNewList_FieldAccess(EOS, i48, o72[SharingAnalysis.field]o69) → f534_0_appendNewList_Store(EOS, i48, o72[SharingAnalysis.field]o93) | =(o72[SharingAnalysis.field]o93, +(o72[SharingAnalysis.field]o69, 1))
f534_0_appendNewList_Store(EOS, i48, o72[SharingAnalysis.field]o93) → f543_0_appendNewList_JMP(EOS, i48, o72[SharingAnalysis.field]o93)
f543_0_appendNewList_JMP(EOS, i48, o72[SharingAnalysis.field]o93) → f577_0_appendNewList_Load(EOS, i48, o72[SharingAnalysis.field]o93)
f577_0_appendNewList_Load(EOS, i48, o72[SharingAnalysis.field]o93) → f423_0_appendNewList_Load(EOS, i48, o72[SharingAnalysis.field]o93)
f423_0_appendNewList_Load(EOS, i32, o72[SharingAnalysis.field]o69) → f430_0_appendNewList_ConstantStackPush(EOS, i32, i32, o72[SharingAnalysis.field]o69)
f527_0_appendNewList_FieldAccess(EOS, i48) → f541_0_appendNewList_Store(EOS, i48)
f541_0_appendNewList_Store(EOS, i48) → f547_0_appendNewList_JMP(EOS, i48)
f547_0_appendNewList_JMP(EOS, i48) → f599_0_appendNewList_Load(EOS, i48)
f599_0_appendNewList_Load(EOS, i48) → f423_0_appendNewList_Load(EOS, i48, o106[SharingAnalysis.field]o93) | =(o106[SharingAnalysis.field]o93, 1)

Combined rules. Obtained 2 IRules

P rules:
f430_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f430_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f430_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f430_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), 1) | >(x0, 1)

Filtered ground terms:


f430_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → f430_0_appendNewList_ConstantStackPush(x2, x3, x4)
Cond_f430_0_appendNewList_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f430_0_appendNewList_ConstantStackPush(x1, x3, x4, x5)
Cond_f430_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f430_0_appendNewList_ConstantStackPush1(x1, x3, x4, x5)

Filtered duplicate terms:


f430_0_appendNewList_ConstantStackPush(x1, x2, x3) → f430_0_appendNewList_ConstantStackPush(x2, x3)
Cond_f430_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → Cond_f430_0_appendNewList_ConstantStackPush(x1, x3, x4)
Cond_f430_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4) → Cond_f430_0_appendNewList_ConstantStackPush1(x1, x3, x4)

Filtered unneeded terms:


Cond_f430_0_appendNewList_ConstantStackPush1(x1, x2, x3) → Cond_f430_0_appendNewList_ConstantStackPush1(x1, x2)

Prepared 2 rules for path length conversion:

P rules:
f430_0_appendNewList_ConstantStackPush(x0, x1) → f430_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f430_0_appendNewList_ConstantStackPush(x0, x1) → f430_0_appendNewList_ConstantStackPush(-(x0, 1), 1) | >(x0, 1)

Finished conversion. Obtained 2 rules.

P rules:
f430_0_appendNewList_ConstantStackPush(x0, x1) → f430_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f430_0_appendNewList_ConstantStackPush(x2, x3) → f430_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(12) Obligation:

Rules:
f430_0_appendNewList_ConstantStackPush(x0, x1) → f430_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f430_0_appendNewList_ConstantStackPush(x2, x3) → f430_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f430_0_appendNewList_ConstantStackPush(x5, x7)] = x5

Therefore the following rule(s) have been dropped:


f430_0_appendNewList_ConstantStackPush(x0, x1) → f430_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f430_0_appendNewList_ConstantStackPush(x2, x3) → f430_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(14) YES