Problematic array store example for SPF cases - sohah/VeritestingTransformations GitHub Wiki
Here's an example that has a problem for an array store. The arrayLoad1 method is called with a concrete null array reference with fresh symbolic variables for index0 and length. The problem, as of now, is that we explore 3 choices apart from the static choice.
public boolean arrayLoad1(int x[], int index0, int length) {
int temp = 1;
boolean bug = false;
for (int index = 0; index < 2; index++) {
if (index0 == 1) {
x[index] = length;
}
}
return bug;
}Here's the log file:
symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 symbolic.min_byte=-128 symbolic.min_char=0 symbolic.max_int=2147483647 symbolic.max_long=9223372036854775807 symbolic.max_short=32767 symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=-100.0 symbolic.max_double=100.0
- running veritesting with SPFCases. JavaPathfinder core system v8.0 (rev 32) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test VeritestingPerf.main()
====================================================== search started: 10/2/18 1:58 PM iteration = 0 iteration = 1 Starting region analysis for fieldTest4(VeritestingPerf.fieldTest4(I)I) Subregion: if ((<= @w2 0 )) { if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; } } else { if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } } putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 11 }
Subregion: if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; }
Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (== @w16 0 ) )) { 17 = new <Application,Ljava/lang/AssertionError>@102 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @106 exception:18 throw 17 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } }
Subregion: if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; }
Starting region analysis for fieldTest1(VeritestingPerf.fieldTest1(I)I) Subregion: if ((! (== @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 5 } else { skip; }
Starting region analysis for arrayLoad0(VeritestingPerf.arrayLoad0(II)I) Subregion: if ((> @w3 0 )) { @w11 = @w6[@w2:<Primordial,I>] @w14 := (+ @w11 2 ); } else { skip; } @w15 := (Gamma @w3>0 @w14 2);
Starting region analysis for arrayStore0(VeritestingPerf.arrayStore0(II)I) Subregion: if ((! (> @w3 0 ) )) { skip; } else { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 } @w14 := (Gamma !(@w3>0) 2 1);
Subregion: if ((! (!= @w17 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w20 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w24 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; }
Subregion: if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; }
Starting region analysis for arrayLoadStore0(VeritestingPerf.arrayLoadStore0(II)I) Subregion: if ((> @w3 0 )) { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 @w12 = @w6[@w2:<Primordial,I>] @w13 := (+ @w12 2 ); @w14 := (+ @w13 2 ); @w6[@w2:<Primordial,I>] = @w14 } else { skip; } @w15 := (Gamma @w3>0 @w13 2);
Subregion: if ((! (!= @w16 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; }
Subregion: if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; }
Starting region analysis for arrayLoad1(VeritestingPerf.arrayLoad1([III)Z) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (!= @w3 1 ) )) { @w2[@w10:<Primordial,I>] = @w4 } else { skip; }
Starting region analysis for countBitsSet(VeritestingPerf.countBitsSet(I)I) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (== @w6 0 ) )) { @w7 := (+ @w11 1 ); } else { skip; } @w8 := (Gamma !(@w6==0) @w7 @w11);
Starting region analysis for fieldTest2(VeritestingPerf.fieldTest2(I)I) Subregion: if ((== @w2 0 )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 } else { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w15 2 ) )) { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 } else { skip; }
Subregion: if ((! (!= @w12 @w14 ) )) { skip; } else { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 }
Starting region analysis for fieldTest3(VeritestingPerf.fieldTest3(I)I) Subregion: if ((! (== @w2 0 ) )) { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 11 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w12 := (+ @w11 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w17 3 ) )) { 18 = new <Application,Ljava/lang/AssertionError>@78 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @82 exception:19 throw 18 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Starting region analysis for simpleRegion(VeritestingPerf.simpleRegion(I)I) Subregion: if ((! (<= @w2 0 ) )) { skip; } else { skip; } @w9 := (Gamma !(@w2<=0) 3 4);
Starting region analysis for main(VeritestingPerf.main([Ljava/lang/String;)V) Starting region analysis for fieldTest4(VeritestingPerf.fieldTest4(I)I) Subregion: if ((<= @w2 0 )) { if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; } } else { if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } } putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 11 }
Subregion: if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; }
Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (== @w16 0 ) )) { 17 = new <Application,Ljava/lang/AssertionError>@102 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @106 exception:18 throw 17 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } }
Subregion: if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; }
Starting region analysis for fieldTest1(VeritestingPerf.fieldTest1(I)I) Subregion: if ((! (== @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 5 } else { skip; }
Starting region analysis for arrayLoad0(VeritestingPerf.arrayLoad0(II)I) Subregion: if ((> @w3 0 )) { @w11 = @w6[@w2:<Primordial,I>] @w14 := (+ @w11 2 ); } else { skip; } @w15 := (Gamma @w3>0 @w14 2);
Starting region analysis for arrayStore0(VeritestingPerf.arrayStore0(II)I) Subregion: if ((! (> @w3 0 ) )) { skip; } else { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 } @w14 := (Gamma !(@w3>0) 2 1);
Subregion: if ((! (!= @w17 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w20 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w24 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; }
Subregion: if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; }
Starting region analysis for arrayLoadStore0(VeritestingPerf.arrayLoadStore0(II)I) Subregion: if ((> @w3 0 )) { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 @w12 = @w6[@w2:<Primordial,I>] @w13 := (+ @w12 2 ); @w14 := (+ @w13 2 ); @w6[@w2:<Primordial,I>] = @w14 } else { skip; } @w15 := (Gamma @w3>0 @w13 2);
Subregion: if ((! (!= @w16 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; }
Subregion: if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; }
Starting region analysis for arrayLoad1(VeritestingPerf.arrayLoad1([III)Z) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (!= @w3 1 ) )) { @w2[@w10:<Primordial,I>] = @w4 } else { skip; }
Starting region analysis for countBitsSet(VeritestingPerf.countBitsSet(I)I) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (== @w6 0 ) )) { @w7 := (+ @w11 1 ); } else { skip; } @w8 := (Gamma !(@w6==0) @w7 @w11);
Starting region analysis for fieldTest2(VeritestingPerf.fieldTest2(I)I) Subregion: if ((== @w2 0 )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 } else { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w15 2 ) )) { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 } else { skip; }
Subregion: if ((! (!= @w12 @w14 ) )) { skip; } else { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 }
Starting region analysis for fieldTest3(VeritestingPerf.fieldTest3(I)I) Subregion: if ((! (== @w2 0 ) )) { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 11 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w12 := (+ @w11 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w17 3 ) )) { 18 = new <Application,Ljava/lang/AssertionError>@78 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @82 exception:19 throw 18 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Starting region analysis for simpleRegion(VeritestingPerf.simpleRegion(I)I) Subregion: if ((! (<= @w2 0 ) )) { skip; } else { skip; } @w9 := (Gamma !(@w2<=0) 3 4);
Starting region analysis for main(VeritestingPerf.main([Ljava/lang/String;)V) Starting method analysis for fieldTest4(VeritestingPerf.fieldTest4(I)I) Subregion: if ((<= @w2 0 )) { if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; } } else { if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } } putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 11 }
Subregion: if ((! (>= @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 } else { skip; }
Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (== @w16 0 ) )) { 17 = new <Application,Ljava/lang/AssertionError>@102 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @106 exception:18 throw 17 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Subregion: if ((! (!= @w2 1 ) )) { 6 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w6 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 } else { if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; } }
Subregion: if ((! (!= @w2 2 ) )) { 9 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w9 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { skip; }
Unexpected number (3) of self-contained regions in findConditionalSuccessors Unable to create a method summary subregion for: fieldTest4 Starting method analysis for fieldTest1(VeritestingPerf.fieldTest1(I)I) Subregion: if ((! (== @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 5 } else { skip; }
Method if ((! (== @w2 0 ) )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 5 } else { skip; } return 2
Starting method analysis for arrayLoad0(VeritestingPerf.arrayLoad0(II)I) Subregion: if ((> @w3 0 )) { @w11 = @w6[@w2:<Primordial,I>] @w14 := (+ @w11 2 ); } else { skip; } @w15 := (Gamma @w3>0 @w14 2);
Unable to find condition. Basic block: BB[SSA:0..1]1 - VeritestingPerf.arrayLoad0(II)I Instruction: 6 = new <Primordial,[I>@15 End of block: BB[SSA:0..1]1 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:2..5]2 - VeritestingPerf.arrayLoad0(II)I Instruction: arraystore 6[7] = 8 End of block: BB[SSA:2..5]2 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:6..9]3 - VeritestingPerf.arrayLoad0(II)I Instruction: arraystore 6[9] = 10 End of block: BB[SSA:6..9]3 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:10..15]4 - VeritestingPerf.arrayLoad0(II)I Instruction: conditional branch(gt, to iindex=19) 3,7 End of block: BB[SSA:10..15]4 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:16..18]5 - VeritestingPerf.arrayLoad0(II)I Instruction: goto (from iindex= 18 to iindex = 25) End of block: BB[SSA:16..18]5 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:19..21]6 - VeritestingPerf.arrayLoad0(II)I Instruction: 11 = arrayload 6[2] End of block: BB[SSA:19..21]6 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:22..24]7 - VeritestingPerf.arrayLoad0(II)I Instruction: 14 = binaryop(add) 11 , 5 End of block: BB[SSA:22..24]7 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:25..25]8 - VeritestingPerf.arrayLoad0(II)I Instruction: 15 = phi 5,14 Instruction: goto (from iindex= 25 to iindex = 29) End of block: BB[SSA:25..25]8 - VeritestingPerf.arrayLoad0(II)I Basic block: BB(Handler)[SSA]9 - VeritestingPerf.arrayLoad0(II)I Instruction: 12 = getCaughtException End of block: BB(Handler)[SSA]9 - VeritestingPerf.arrayLoad0(II)I Basic block: BB[SSA:29..30]10 - VeritestingPerf.arrayLoad0(II)I Instruction: 17 = phi 15,13 Instruction: return 17 End of block: BB[SSA:29..30]10 - VeritestingPerf.arrayLoad0(II)I Method 6 = new <Primordial,[I>@15 @w6[@w7:<Primordial,I>] = @w8 @w6[@w9:<Primordial,I>] = @w10 if ((> @w3 0 )) { @w11 = @w6[@w2:<Primordial,I>] @w14 := (+ @w11 2 ); } else { skip; } @w15 := (Gamma @w3>0 @w14 2); @w17 := @w15; return 17
Starting method analysis for arrayStore0(VeritestingPerf.arrayStore0(II)I) Subregion: if ((! (> @w3 0 ) )) { skip; } else { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 } @w14 := (Gamma !(@w3>0) 2 1);
Subregion: if ((! (!= @w17 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w20 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w24 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; }
Subregion: if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; }
Subregion: if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; }
Unable to find condition. Basic block: BB[SSA:0..1]1 - VeritestingPerf.arrayStore0(II)I Instruction: 6 = new <Primordial,[I>@15 End of block: BB[SSA:0..1]1 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:2..5]2 - VeritestingPerf.arrayStore0(II)I Instruction: arraystore 6[7] = 8 End of block: BB[SSA:2..5]2 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:6..9]3 - VeritestingPerf.arrayStore0(II)I Instruction: arraystore 6[9] = 10 End of block: BB[SSA:6..9]3 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:10..15]4 - VeritestingPerf.arrayStore0(II)I Instruction: conditional branch(gt, to iindex=19) 3,7 End of block: BB[SSA:10..15]4 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:16..18]5 - VeritestingPerf.arrayStore0(II)I Instruction: goto (from iindex= 18 to iindex = 25) End of block: BB[SSA:16..18]5 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:19..24]6 - VeritestingPerf.arrayStore0(II)I Instruction: 11 = binaryop(add) 9 , 5 Instruction: arraystore 6[2] = 11 End of block: BB[SSA:19..24]6 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:25..25]7 - VeritestingPerf.arrayStore0(II)I Instruction: 14 = phi 5,9 Instruction: goto (from iindex= 25 to iindex = 29) End of block: BB[SSA:25..25]7 - VeritestingPerf.arrayStore0(II)I Basic block: BB(Handler)[SSA]8 - VeritestingPerf.arrayStore0(II)I Instruction: 12 = getCaughtException End of block: BB(Handler)[SSA]8 - VeritestingPerf.arrayStore0(II)I Basic block: BB[SSA:29..31]9 - VeritestingPerf.arrayStore0(II)I Instruction: 16 = phi 14,13 Instruction: 17 = getstatic < Application, LVeritestingPerf, $assertionsDisabled, <Primordial,Z> > Instruction: conditional branch(ne, to iindex=43) 17,7 End of block: BB[SSA:29..31]9 - VeritestingPerf.arrayStore0(II)I Method 6 = new <Primordial,[I>@15 @w6[@w7:<Primordial,I>] = @w8 @w6[@w9:<Primordial,I>] = @w10 if ((! (> @w3 0 ) )) { skip; } else { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 } @w14 := (Gamma !(@w3>0) 2 1); @w16 := @w14; 17 = getstatic < Application, LVeritestingPerf, $assertionsDisabled, <Primordial,Z> > if ((! (!= @w17 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w16 2 )) { 18 = new <Application,Ljava/lang/AssertionError>@63 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @67 exception:19 throw 18 } else { skip; } } else { skip; } } else { skip; } 20 = getstatic < Application, LVeritestingPerf, $assertionsDisabled, <Primordial,Z> > if ((! (!= @w20 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 0 ) )) { @w21 = @w6[@w7:<Primordial,I>] if ((!= @w21 3 )) { 22 = new <Application,Ljava/lang/AssertionError>@95 invokespecial < Application, Ljava/lang/AssertionError, ()V > 22 @99 exception:23 throw 22 } else { skip; } } else { skip; } } else { skip; } } else { skip; } 24 = getstatic < Application, LVeritestingPerf, $assertionsDisabled, <Primordial,Z> > if ((! (!= @w24 0 ) )) { if ((! (<= @w3 0 ) )) { if ((! (!= @w2 1 ) )) { @w25 = @w6[@w9:<Primordial,I>] if ((! (!= @w25 3 ) )) { skip; } else { 26 = new <Application,Ljava/lang/AssertionError>@128 invokespecial < Application, Ljava/lang/AssertionError, ()V > 26 @132 exception:27 throw 26 } } else { skip; } } else { skip; } } else { skip; } return 16
Starting method analysis for arrayLoadStore0(VeritestingPerf.arrayLoadStore0(II)I) Subregion: if ((> @w3 0 )) { @w11 := (+ 1 2 ); @w6[@w2:<Primordial,I>] = @w11 @w12 = @w6[@w2:<Primordial,I>] @w13 := (+ @w12 2 ); @w14 := (+ @w13 2 ); @w6[@w2:<Primordial,I>] = @w14 } else { skip; } @w15 := (Gamma @w3>0 @w13 2);
Subregion: if ((! (!= @w16 0 ) )) { if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; } } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: region contains condition that cannot be instantiated Subregion: if ((! (> @w3 0 ) )) { if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; } } else { skip; }
Subregion: if ((!= @w15 2 )) { 17 = new <Application,Ljava/lang/AssertionError>@69 invokespecial < Application, Ljava/lang/AssertionError, ()V > 17 @73 exception:18 throw 17 } else { skip; }
Unable to create a method summary subregion for: arrayLoadStore0 Starting method analysis for arrayLoad1(VeritestingPerf.arrayLoad1([III)Z) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (!= @w3 1 ) )) { @w2[@w10:<Primordial,I>] = @w4 } else { skip; }
Unable to find condition. Basic block: BB[SSA:0..5]1 - VeritestingPerf.arrayLoad1([III)Z End of block: BB[SSA:0..5]1 - VeritestingPerf.arrayLoad1([III)Z Basic block: BB[SSA:6..8]2 - VeritestingPerf.arrayLoad1([III)Z Instruction: 10 = phi 9,7 Instruction: conditional branch(ge, to iindex=21) 10,8 End of block: BB[SSA:6..8]2 - VeritestingPerf.arrayLoad1([III)Z Unable to create a method summary subregion for: arrayLoad1 Starting method analysis for countBitsSet(VeritestingPerf.countBitsSet(I)I) Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: FindStructuredBlockEndNode: mal-formed region Subregion: if ((! (== @w6 0 ) )) { @w7 := (+ @w11 1 ); } else { skip; } @w8 := (Gamma !(@w6==0) @w7 @w11);
Unable to find condition. Basic block: BB[SSA:0..1]1 - VeritestingPerf.countBitsSet(I)I End of block: BB[SSA:0..1]1 - VeritestingPerf.countBitsSet(I)I Basic block: BB[SSA:2..4]2 - VeritestingPerf.countBitsSet(I)I Instruction: 10 = phi 9,2 Instruction: 11 = phi 8,4 Instruction: conditional branch(eq, to iindex=19) 10,4 End of block: BB[SSA:2..4]2 - VeritestingPerf.countBitsSet(I)I Unable to find condition. Basic block: BB[SSA:0..1]1 - VeritestingPerf.countBitsSet(I)I End of block: BB[SSA:0..1]1 - VeritestingPerf.countBitsSet(I)I Basic block: BB[SSA:2..4]2 - VeritestingPerf.countBitsSet(I)I Instruction: 10 = phi 9,2 Instruction: 11 = phi 8,4 Instruction: conditional branch(eq, to iindex=19) 10,4 End of block: BB[SSA:2..4]2 - VeritestingPerf.countBitsSet(I)I Unable to create a method summary subregion for: countBitsSet Starting method analysis for fieldTest2(VeritestingPerf.fieldTest2(I)I) Subregion: if ((== @w2 0 )) { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 } else { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w15 2 ) )) { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 } else { skip; }
Subregion: if ((! (!= @w12 @w14 ) )) { skip; } else { 16 = new <Application,Ljava/lang/AssertionError>@68 invokespecial < Application, Ljava/lang/AssertionError, ()V > 16 @72 exception:17 throw 16 }
Unable to create a method summary subregion for: fieldTest2 Starting method analysis for fieldTest3(VeritestingPerf.fieldTest3(I)I) Subregion: if ((! (== @w2 0 ) )) { 5 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w7 := (+ @w5 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 7 8 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w10 := (+ @w8 2 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 10 } else { putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 9 11 = getfield < Application, LVeritestingPerf, count, <Primordial,I> > 1 @w12 := (+ @w11 1 ); putfield 1.< Application, LVeritestingPerf, count, <Primordial,I> > = 12 }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: stateful condition Subregion: if ((! (== @w17 3 ) )) { 18 = new <Application,Ljava/lang/AssertionError>@78 invokespecial < Application, Ljava/lang/AssertionError, ()V > 18 @82 exception:19 throw 18 } else { skip; }
Unable to create subregion. Reason: gov.nasa.jpf.symbc.veritesting.StaticRegionException: createComplexIfCondition: unconditional branch (continue or break) Unable to create a method summary subregion for: fieldTest3 Starting method analysis for simpleRegion(VeritestingPerf.simpleRegion(I)I) Subregion: if ((! (<= @w2 0 ) )) { skip; } else { skip; } @w9 := (Gamma !(@w2<=0) 3 4);
Method if ((! (<= @w2 0 ) )) { skip; } else { skip; } @w9 := (Gamma !(@w2<=0) 3 4); return 9
Starting method analysis for main(VeritestingPerf.main([Ljava/lang/String;)V) Method 3 = new <Application,LVeritestingPerf>@0 invokespecial < Application, LVeritestingPerf, ()V > 3 @4 exception:4 8 = invokevirtual < Application, LVeritestingPerf, arrayLoad1([III)Z > 3,5,6,6 @10 exception:7 10 = new <Primordial,[I>@159 @w10[@w11:<Primordial,I>] = @w12 @w10[@w6:<Primordial,I>] = @w13 return
---------- STARTING Transformations for conditional region: VeritestingPerf.arrayLoad1([III)Z#17 if ((! (!= @w3 1 ) )) { @w2[@w10:<Primordial,I>] = @w4 } else { skip; }
Region Stack Slot Map (var -> slot) @w10 --------- [6] @w3 --------- [2] @w2 --------- [1] @w9 --------- [6]
printing Region Input Table (var->slot) @w3 --------- 2 @w2 --------- 1 @w10 --------- 6
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w10 --------- int @w8 --------- int @w3 --------- int @w6 --------- int @w2 --------- cone:<Primordial,[I> @w9 --------- int @w7 --------- int
--------------- UNIQUENESS TRANSFORMATION --------------- if ((! (!= @w3$1 1 ) )) { @w2$1[@w10$1:<Primordial,I>] = @w4$1 } else { skip; }
printing stack-slot table (var->slot) @w2$1 --------- [1] @w3$1 --------- [2] @w10$1 --------- [6]
printing Region Input Table (var->slot) @w2$1 --------- 1 @w3$1 --------- 2 @w10$1 --------- 6
printing WalaVarTypeTable ( var ->type) @w2$1 --------- cone:<Primordial,[I> @w3$1 --------- int @w10$1 --------- int
printing Region Output Table (slot->var)
--------------- SUBSTITUTION TRANSFORMATION ---------------
if ((! (!= @w3$1 1 ) )) { @w2$1[@w10$1:<Primordial,I>] = @w4$1 } else { skip; }
printing stack-slot table (var->slot) @w2$1 --------- [1] @w3$1 --------- [2] @w10$1 --------- [6]
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w2$1 --------- cone:<Primordial,[I> @w3$1 --------- int @w10$1 --------- int
--------------- AFTER SUBSTITUTION TRANSFORMATION ---------------
if ((! (!= index0 1 ) )) { 0[0:<Primordial,I>] = @w4$1 } else { skip; }
printing stack-slot table (var->slot) @w2$1 --------- [1] @w3$1 --------- [2] @w10$1 --------- [6]
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w2$1 --------- cone:<Primordial,[I> @w3$1 --------- int @w10$1 --------- int
--------------- FIELD REFERENCE TRANSFORMATION ---------------
if ((! (!= index0 1 ) )) { 0[0:<Primordial,I>] = @w4$1 } else { skip; }
printing FieldRefTypeTable (FieldRefVarExpr->type)
--------------- ARRAY TRANSFORMATION ---------------
--------------- SPFCases TRANSFORMATION 1ST PASS --------------- if ((! (!= index0 1 ) )) { <SPFCase: cond: (&& (== 0 0 ) (! (!= index0 1 ) ) ), reason: THROW> } else { skip; }
--------------- SPFCases TRANSFORMATION 2ND PASS --------------- skip;
--------------- LINEARIZATION TRANSFORMATION --------------- skip;
--------------- NO-SKIP OPTIMIZATION --------------- skip;
--------------- TO GREEN TRANSFORMATION --------------- (0 == 0)
--------------- SPFCases GREEN PREDICATE --------------- (|| (== 0 1 ) (&& (== 0 0 ) (! (!= index0 1 ) ) ) )
=========Executing static region choice in BranchCG
---------- STARTING Transformations for conditional region: VeritestingPerf.arrayLoad1([III)Z#17 if ((! (!= @w3 1 ) )) { @w2[@w10:<Primordial,I>] = @w4 } else { skip; }
Region Stack Slot Map (var -> slot) @w10 --------- [6] @w3 --------- [2] @w2 --------- [1] @w9 --------- [6]
printing Region Input Table (var->slot) @w3 --------- 2 @w2 --------- 1 @w10 --------- 6
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w10 --------- int @w8 --------- int @w3 --------- int @w6 --------- int @w2 --------- cone:<Primordial,[I> @w9 --------- int @w7 --------- int
--------------- UNIQUENESS TRANSFORMATION --------------- if ((! (!= @w3$2 1 ) )) { @w2$2[@w10$2:<Primordial,I>] = @w4$2 } else { skip; }
printing stack-slot table (var->slot) @w2$2 --------- [1] @w3$2 --------- [2] @w10$2 --------- [6]
printing Region Input Table (var->slot) @w2$2 --------- 1 @w3$2 --------- 2 @w10$2 --------- 6
printing WalaVarTypeTable ( var ->type) @w2$2 --------- cone:<Primordial,[I> @w3$2 --------- int @w10$2 --------- int
printing Region Output Table (slot->var)
--------------- SUBSTITUTION TRANSFORMATION ---------------
if ((! (!= @w3$2 1 ) )) { @w2$2[@w10$2:<Primordial,I>] = @w4$2 } else { skip; }
printing stack-slot table (var->slot) @w2$2 --------- [1] @w3$2 --------- [2] @w10$2 --------- [6]
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w2$2 --------- cone:<Primordial,[I> @w3$2 --------- int @w10$2 --------- int
--------------- AFTER SUBSTITUTION TRANSFORMATION ---------------
if ((! (!= index0 1 ) )) { 0[1:<Primordial,I>] = @w4$2 } else { skip; }
printing stack-slot table (var->slot) @w2$2 --------- [1] @w3$2 --------- [2] @w10$2 --------- [6]
printing Region Output Table (slot->var)
printing WalaVarTypeTable ( var ->type) @w2$2 --------- cone:<Primordial,[I> @w3$2 --------- int @w10$2 --------- int
--------------- FIELD REFERENCE TRANSFORMATION ---------------
if ((! (!= index0 1 ) )) { 0[1:<Primordial,I>] = @w4$2 } else { skip; }
printing FieldRefTypeTable (FieldRefVarExpr->type)
--------------- ARRAY TRANSFORMATION ---------------
--------------- SPFCases TRANSFORMATION 1ST PASS --------------- if ((! (!= index0 1 ) )) { <SPFCase: cond: (&& (== 0 0 ) (! (!= index0 1 ) ) ), reason: THROW> } else { skip; }
--------------- SPFCases TRANSFORMATION 2ND PASS --------------- skip;
--------------- LINEARIZATION TRANSFORMATION --------------- skip;
--------------- NO-SKIP OPTIMIZATION --------------- skip;
--------------- TO GREEN TRANSFORMATION --------------- (0 == 0)
--------------- SPFCases GREEN PREDICATE --------------- (|| (== 0 1 ) (&& (== 0 0 ) (! (!= index0 1 ) ) ) )
=========Executing static region choice in BranchCG
=========Executing then choice Instruction:
=========Executing else choice Instruction:
=========Executing then choice Instruction:
====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.NullPointerException at VeritestingPerf.arrayLoad1(VeritestingPerf.java:141) at VeritestingPerf.main(VeritestingPerf.java:154)
====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at VeritestingPerf.arrayLoad1(VeritestingPerf.java:141) at VeritestingPerf.main(VeritestingPerf.java:154)
====================================================== VeritestingListener report:
/************************ Printing Regions Statistics ***************** *** Region Key = VeritestingPerf.arrayLoad1([III)Z#17 Veritested? | hitNumber | failReason Yes | 2 | null
/************************ Printing Time Decomposition Statistics ***************** static analysis time = 358 msec Veritesting Dyn Time = 529 msec
/************************ Printing Solver Statistics ***************** Total Solver Queries Count = 5 Total Solver Time = 33 msec Total Solver Parse Time = 9 msec Total Solver Clean up Time = 0 msec
/************************ Printing Accumulative Statistics ***************** Number of Distinct Veritested Regions = 1 Number of Distinct Un-Veritested Symbolic Regions = 0 Number of Distinct Un-Veritested Concrete Regions = 0 Number of Distinct Failed Regions for Field Reference = 0 Number of Distinct Failed Regions for SPFCases = 0 Number of Distinct Failed Regions for Other Reasons = 0 Total number of Distinct regions = 1 Number of Veritested Regions Instances = 2
====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException at VeritestingPerf..."
====================================================== statistics elapsed time: 00:00:00 states: new=7,visited=0,backtracked=4,end=1 search: maxDepth=4,constraints=0 choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=3 heap: new=362,released=13,maxLive=345,gcCycles=2 instructions: 3173 max memory: 303MB loaded code: classes=64,methods=1320
====================================================== search finished: 10/2/18 1:58 PM