(0) Obligation:
JBC Problem based on JBC Program:
Manifest-Version: 1.0
Created-By: 1.6.0_26 (Sun Microsystems Inc.)
Main-Class: simple/narrowKonv/Main
package simple.narrowKonv;
public class Main {
/**
* @param args
*/
public static void main(String[] args) {
NarrowKonv.loop(args.length);
}
}
package simple.narrowKonv;
public class NarrowKonv {
public static void loop(int i) {
int range = 20;
while (0 <= i && i <= range) {
if (!(0 == i && i == range)) {
if (i == range) {
i = 0;
range--;
} else {
i++;
}
}
}
}
}
(1) JBCNonTerm (EQUIVALENT transformation)
Reached a loop using the following run:
0:
<simple.narrowKonv.Main.main||0: load ADDR args||args: a538|| ->
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
1:
<simple.narrowKonv.Main.main||1: arraylength|| - ||a538>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
2:
<simple.narrowKonv.Main.main||2: simple.narrowKonv.NarrowKonv.loop(I)V|| - ||1>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
3:
<simple.narrowKonv.NarrowKonv.loop||0: push 20||i: 1|| ->
<simple.narrowKonv.Main.main||2: simple.narrowKonv.NarrowKonv.loop|| - ||1>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
4:
<simple.narrowKonv.NarrowKonv.loop||2: store INT to range||i: 1||20>
<simple.narrowKonv.Main.main||2: simple.narrowKonv.NarrowKonv.loop|| - ||1>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
5:
<simple.narrowKonv.NarrowKonv.loop||3: push 0||i: 1, range: 20|| ->
<simple.narrowKonv.Main.main||2: simple.narrowKonv.NarrowKonv.loop|| - ||1>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a536
String.CASE_INSENSITIVE_ORDER: o269
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o269!: String$CaseInsensitiveComparator()
a536([java.io.ObjectStreamField|]): length 0
a538([java.lang.String...]): length 1
In the loop head node, references [iconst_0, i241, i242] were interesting.
By SMT, we could prove
(0 <= initial_i16 and ((((path1_i241 = path1_i249 and 0 = res_i241 and 0 = res_i242 and path1_i16 = res_i16 and path1_i241 = initial_i241 and path1_i242 = initial_i242 and path1_i16 = initial_i16) and (0 <= path1_i249 and path1_i249 <= path1_i242 and path1_i249 = 0 and path1_i242 = 0)) or ((path2_i241 = path2_i249 and path2_i249 = path2_i251 and path2_i256 = (path2_i251 + 1) and path2_i256 = res_i241 and path2_i242 = res_i242 and path2_i16 = res_i16 and path2_i241 = initial_i241 and path2_i242 = initial_i242 and path2_i16 = initial_i16) and (0 <= path2_i249 and path2_i249 <= path2_i242 and 0 != path2_i251 and path2_i251 != path2_i242)) or ((path3_i241 = path3_i249 and path3_i249 = path3_i251 and path3_i378 = (path3_i242 + -1) and 0 = res_i241 and path3_i378 = res_i242 and path3_i16 = res_i16 and path3_i241 = initial_i241 and path3_i242 = initial_i242 and path3_i16 = initial_i16) and (0 <= path3_i249 and path3_i249 <= path3_i242 and 0 != path3_i251)) or ((path4_i241 = path4_i249 and path4_i242 = path4_i253 and 1 = res_i241 and path4_i253 = res_i242 and path4_i16 = res_i16 and path4_i241 = initial_i241 and path4_i242 = initial_i242 and path4_i16 = initial_i16) and (0 <= path4_i249 and path4_i249 <= path4_i242 and path4_i249 = 0 and 0 != path4_i253 and 0 != path4_i253)) or ((path2_i241 = path2_i249 and path2_i249 = path2_i251 and path2_i256 = (path2_i251 + 1) and path2_i256 = res_i241 and path2_i242 = res_i242 and path2_i16 = res_i16 and path2_i241 = initial_i241 and path2_i242 = initial_i242 and path2_i16 = initial_i16) and (0 <= path2_i249 and path2_i249 <= path2_i242 and path2_i251 != path2_i242 and 0 < path2_i251)) or ((path2_i241 = path2_i249 and path2_i249 = path2_i251 and path2_i256 = (path2_i251 + 1) and path2_i256 = res_i241 and path2_i242 = res_i242 and path2_i16 = res_i16 and path2_i241 = initial_i241 and path2_i242 = initial_i242 and path2_i16 = initial_i16) and (0 <= path2_i249 and path2_i249 <= path2_i242 and path2_i251 != path2_i242 and 0 > path2_i251)) or ((path2_i241 = path2_i249 and path2_i249 = path2_i251 and path2_i256 = (path2_i251 + 1) and path2_i256 = res_i241 and path2_i242 = res_i242 and path2_i16 = res_i16 and path2_i241 = initial_i241 and path2_i242 = initial_i242 and path2_i16 = initial_i16) and (0 <= path2_i249 and path2_i249 <= path2_i242 and 0 != path2_i251 and path2_i251 < path2_i242)) or ((path2_i241 = path2_i249 and path2_i249 = path2_i251 and path2_i256 = (path2_i251 + 1) and path2_i256 = res_i241 and path2_i242 = res_i242 and path2_i16 = res_i16 and path2_i241 = initial_i241 and path2_i242 = initial_i242 and path2_i16 = initial_i16) and (0 <= path2_i249 and path2_i249 <= path2_i242 and 0 != path2_i251 and path2_i251 > path2_i242))) and ((res_i241 = res_i249 and !(0 <= res_i249 and res_i249 <= res_i242 and res_i249 = 0 and res_i242 = 0)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i256 = (res_i251 + 1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251 and res_i251 != res_i242)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i378 = (res_i242 + -1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251)) and ((res_i241 = res_i249 and res_i242 = res_i253) and !(0 <= res_i249 and res_i249 <= res_i242 and res_i249 = 0 and 0 != res_i253 and 0 != res_i253)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i256 = (res_i251 + 1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251 and res_i251 != res_i242)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i256 = (res_i251 + 1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251 and res_i251 != res_i242)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i256 = (res_i251 + 1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251 and res_i251 != res_i242)) and ((res_i241 = res_i249 and res_i249 = res_i251 and res_i256 = (res_i251 + 1)) and !(0 <= res_i249 and res_i249 <= res_i242 and 0 != res_i251 and res_i251 != res_i242)))))
to be UNSAT. Consequently, the loop will not terminate.