(0) Obligation:
JBC Problem based on JBC Program:
Manifest-Version: 1.0
Created-By: 1.6.0_26 (Sun Microsystems Inc.)
Main-Class: simple/narrowing/Main
package simple.narrowing;
public class Main {
/**
* @param args
*/
public static void main(String[] args) {
Narrowing.loop(args.length);
}
}
package simple.narrowing;
public class Narrowing {
public static void loop(int i) {
int range = 20;
boolean up = false;
while (0 <= i && i <= range) {
if (i == 0) {
up = true;
}
if (i == range) {
up = false;
}
if (up) {
i++;
}
if (!up) {
i--;
}
if (i == range-2) {
range--;
}
}
}
}
(1) JBCNonTerm (EQUIVALENT transformation)
Reached a loop using the following run:
0:
<simple.narrowing.Main.main||0: load ADDR args||args: a266|| ->
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
1:
<simple.narrowing.Main.main||1: arraylength|| - ||a266>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
2:
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop(I)V|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
3:
<simple.narrowing.Narrowing.loop||0: push 20||i: 0|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
4:
<simple.narrowing.Narrowing.loop||2: store INT to range||i: 0||20>
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
5:
<simple.narrowing.Narrowing.loop||3: push 0||i: 0, range: 20|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
6:
<simple.narrowing.Narrowing.loop||4: store INT to up||i: 0, range: 20||0>
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
7:
<simple.narrowing.Narrowing.loop||5: push 0||i: 0, range: 20, up: 0|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a264
String.CASE_INSENSITIVE_ORDER: o133
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o133!: String$CaseInsensitiveComparator()
a264([java.io.ObjectStreamField|]): length 0
a266([java.lang.String...]): length 0
In the loop head node, references [i40, iconst_20, iconst_0, i41] were interesting.
By SMT, we could prove
((0 <= initial_i40 and 0 <= initial_i41 and initial_i41 <= 1 and 0 <= initial_i19) and ((((path1_i40 = path1_i64 and 1 = res_i40 and 1 = res_i41 and path1_i19 = res_i19 and path1_i40 = initial_i40 and path1_i41 = initial_i41 and path1_i19 = initial_i19) and (0 <= path1_i40 and path1_i64 <= 20 and path1_i64 = 0 and T and 1 > 0 and 1 > 0)) or ((path4_i40 = path4_i64 and path4_i64 = path4_i67 and path4_i67 = path4_i69 and path4_i71 = (path4_i69 + -1) and path4_i71 = path4_i79 and path4_i79 = res_i40 and 0 = res_i41 and path4_i19 = res_i19 and path4_i40 = initial_i40 and path4_i41 = initial_i41 and path4_i19 = initial_i19) and (0 <= path4_i40 and path4_i64 <= 20 and path4_i67 > 0 and path4_i69 != 20 and path4_i41 = 0 and T and T and path4_i79 != 18)) or ((path2_i40 = path2_i64 and path2_i64 = path2_i67 and path2_i67 = path2_i69 and path2_i70 = (path2_i69 + 1) and path2_i70 = path2_i77 and path2_i77 = res_i40 and 1 = res_i41 and path2_i19 = res_i19 and path2_i40 = initial_i40 and path2_i41 = initial_i41 and path2_i19 = initial_i19) and (0 <= path2_i40 and path2_i64 <= 20 and path2_i67 > 0 and path2_i41 = 1 and 1 > 0 and 1 > 0 and path2_i77 != 18 and path2_i69 > 20))) and ((res_i40 = res_i64 and !(0 <= res_i40 and res_i64 <= 20 and res_i64 = 0 and T and 1 > 0 and 1 > 0)) and ((res_i40 = res_i64 and res_i64 = res_i67 and res_i67 = res_i69 and res_i71 = (res_i69 + -1) and res_i71 = res_i79) and !(0 <= res_i40 and res_i64 <= 20 and res_i67 > 0 and res_i69 != 20 and res_i41 = 0 and T and T and res_i79 != 18)) and ((res_i40 = res_i64 and res_i64 = res_i67 and res_i67 = res_i69 and res_i70 = (res_i69 + 1) and res_i70 = res_i77) and !(0 <= res_i40 and res_i64 <= 20 and res_i67 > 0 and res_i69 != 20 and res_i41 = 1 and 1 > 0 and 1 > 0 and res_i77 != 18)))))
to be UNSAT. Consequently, the loop will not terminate.