Commit 2256ebb4 authored by Joachim Müssig's avatar Joachim Müssig
Browse files

create newest version of false positiv example 'loop'

parent 4fff3159
...@@ -261,13 +261,13 @@ Z 0; ...@@ -261,13 +261,13 @@ Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V"; U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 24; HE 24;
HE 25; HE 25;
HE 95; HE 97;
HE 104; HE 104;
PS 24; PS 24;
CF 104; CF 104;
CD 25; CD 25;
CE 24; CE 24;
CE 95; CE 97;
CE 104; CE 104;
} }
ACTO 24 { ACTO 24 {
...@@ -381,7 +381,7 @@ U "java.lang.Object.<init>()V"; ...@@ -381,7 +381,7 @@ U "java.lang.Object.<init>()V";
HE 32; HE 32;
HE 33; HE 33;
HE 34; HE 34;
HE 96; HE 98;
HE 102; HE 102;
HE 105; HE 105;
PS 32; PS 32;
...@@ -390,7 +390,7 @@ CF 105; ...@@ -390,7 +390,7 @@ CF 105;
CD 34; CD 34;
CE 32; CE 32;
CE 33; CE 33;
CE 96; CE 98;
CE 102; CE 102;
CE 105; CE 105;
} }
...@@ -402,7 +402,7 @@ P 5; ...@@ -402,7 +402,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2; B "<param> 0":-2;
Z 0; Z 0;
PS 96; PS 98;
CF 31; CF 31;
CD 31; CD 31;
DD 105; DD 105;
...@@ -429,13 +429,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1; ...@@ -429,13 +429,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0; Z 0;
HE 35; HE 35;
HE 36; HE 36;
HE 97; HE 99;
PS 35; PS 35;
PS 36; PS 36;
CF 109; CF 109;
CE 35; CE 35;
CE 36; CE 36;
CE 97; CE 99;
CE 109; CE 109;
CL 1: "virtual"; CL 1: "virtual";
} }
...@@ -447,7 +447,7 @@ P 5; ...@@ -447,7 +447,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2; B "<param> 1":-2;
Z 0; Z 0;
PS 97; PS 99;
CF 34; CF 34;
PI 4; PI 4;
} }
...@@ -475,7 +475,7 @@ HE 38; ...@@ -475,7 +475,7 @@ HE 38;
HE 39; HE 39;
HE 40; HE 40;
HE 41; HE 41;
HE 98; HE 95;
PS 39; PS 39;
PS 40; PS 40;
CF 40; CF 40;
...@@ -483,7 +483,7 @@ CD 41; ...@@ -483,7 +483,7 @@ CD 41;
CE 38; CE 38;
CE 39; CE 39;
CE 40; CE 40;
CE 98; CE 95;
} }
EXIT 38 { EXIT 38 {
O exit; O exit;
...@@ -503,7 +503,7 @@ P 6; ...@@ -503,7 +503,7 @@ P 6;
S "LoopOverride.java":0,0-0,0; S "LoopOverride.java":0,0-0,0;
B "<exception>":-2; B "<exception>":-2;
Z 0; Z 0;
CF 98: "exc"; CF 95: "exc";
PO 8; PO 8;
} }
FRMI 40 { FRMI 40 {
...@@ -515,7 +515,7 @@ S "LoopOverride.java":0,0-0,0; ...@@ -515,7 +515,7 @@ S "LoopOverride.java":0,0-0,0;
B "<param> 0":-2; B "<param> 0":-2;
Z 0; Z 0;
LD ["null"]; LD ["null"];
PS 98; PS 95;
CF 42; CF 42;
DD 42; DD 42;
} }
...@@ -531,7 +531,7 @@ U "java.lang.Object.<init>()V"; ...@@ -531,7 +531,7 @@ U "java.lang.Object.<init>()V";
HE 42; HE 42;
HE 43; HE 43;
HE 44; HE 44;
HE 99; HE 96;
HE 103; HE 103;
HE 106; HE 106;
PS 42; PS 42;
...@@ -540,7 +540,7 @@ CF 106; ...@@ -540,7 +540,7 @@ CF 106;
CD 44; CD 44;
CE 42; CE 42;
CE 43; CE 43;
CE 99; CE 96;
CE 103; CE 103;
CE 106; CE 106;
} }
...@@ -552,7 +552,7 @@ P 6; ...@@ -552,7 +552,7 @@ P 6;
S "LoopOverride.java":1,0-1,0; S "LoopOverride.java":1,0-1,0;
B "<param> 0":-2; B "<param> 0":-2;
Z 0; Z 0;
PS 99; PS 96;
CF 41; CF 41;
CD 41; CD 41;
DD 106; DD 106;
...@@ -577,7 +577,7 @@ P 6; ...@@ -577,7 +577,7 @@ P 6;
S "LoopOverride.java":1,0-1,0; S "LoopOverride.java":1,0-1,0;
B "LoopOverride.<init>()V":4; B "LoopOverride.<init>()V":4;
Z 0; Z 0;
CF 98; CF 95;
} }
ENTR 46 { ENTR 46 {
O entry; O entry;
...@@ -975,28 +975,29 @@ Z 0; ...@@ -975,28 +975,29 @@ Z 0;
CF 65; CF 65;
DD 65; DD 65;
} }
ACTO 95 { FRMO 95 {
O act-out; O form-out;
V "[M] |0|UNIQ(code)"; V "[M] |0|UNIQ(code)";
T "I"; T "I";
P 5; P 6;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "LoopOverride.java":0,0-0,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 24: "exc"; CF 38;
CF 25; PO 101;
} }
ACTO 96 { ACTO 96 {
O act-out; O act-out;
V "[M] |0|UNIQ(code)"; V "[M] |0|UNIQ(code)";
T "I"; T "I";
P 5; P 6;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "LoopOverride.java":1,0-1,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 33: "exc"; CF 43: "exc";
CF 35; CF 44;
DD 102; DD 103;
DH 95;
} }
ACTO 97 { ACTO 97 {
O act-out; O act-out;
...@@ -1006,32 +1007,31 @@ P 5; ...@@ -1006,32 +1007,31 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 21; CF 24: "exc";
CF 36: "exc"; CF 25;
} }
FRMO 98 { ACTO 98 {
O form-out; O act-out;
V "[M] |0|UNIQ(code)"; V "[M] |0|UNIQ(code)";
T "I"; T "I";
P 6; P 5;
S "LoopOverride.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 38; CF 33: "exc";
PO 101; CF 35;
DD 102;
} }
ACTO 99 { ACTO 99 {
O act-out; O act-out;
V "[M] |0|UNIQ(code)"; V "[M] |0|UNIQ(code)";
T "I"; T "I";
P 6; P 5;
S "LoopOverride.java":1,0-1,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 43: "exc"; CF 21;
CF 44; CF 36: "exc";
DD 103;
DH 98;
} }
FRMO 100 { FRMO 100 {
O form-out; O form-out;
...@@ -1042,7 +1042,7 @@ S "LoopOverride.java":0,0-0,0; ...@@ -1042,7 +1042,7 @@ S "LoopOverride.java":0,0-0,0;
B "Ljava/lang/Object.code":-4; B "Ljava/lang/Object.code":-4;
Z 0; Z 0;
CF 2; CF 2;
PO 97; PO 99;
} }
ACTO 101 { ACTO 101 {
O act-out; O act-out;
...@@ -1062,7 +1062,7 @@ P 5; ...@@ -1062,7 +1062,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1; B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0; Z 0;
CF 96; CF 98;
DD 25; DD 25;
} }
NORM 103 { NORM 103 {
...@@ -1072,7 +1072,7 @@ P 6; ...@@ -1072,7 +1072,7 @@ P 6;
S "LoopOverride.java":0,0-0,0; S "LoopOverride.java":0,0-0,0;
B "LoopOverride.<init>()V":-1; B "LoopOverride.<init>()V":-1;
Z 0; Z 0;
CF 99; CF 96;
DD 40; DD 40;
} }
NORM 104 { NORM 104 {
...@@ -1082,9 +1082,9 @@ P 5; ...@@ -1082,9 +1082,9 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1; B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0; Z 0;
CF 95; CF 97;
DD 24; DD 24;
DD 95; DD 97;
} }
NORM 105 { NORM 105 {
O compound; O compound;
...@@ -1095,7 +1095,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1; ...@@ -1095,7 +1095,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0; Z 0;
CF 102; CF 102;
DD 33; DD 33;
DD 96; DD 98;
} }
NORM 106 { NORM 106 {
O compound; O compound;
...@@ -1106,7 +1106,7 @@ B "LoopOverride.<init>()V":-1; ...@@ -1106,7 +1106,7 @@ B "LoopOverride.<init>()V":-1;
Z 0; Z 0;
CF 103; CF 103;
DD 43; DD 43;
DD 99; DD 96;
} }
NORM 107 { NORM 107 {
O compound; O compound;
...@@ -1133,7 +1133,7 @@ P 5; ...@@ -1133,7 +1133,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0; S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9; B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
Z 0; Z 0;
CF 97; CF 99;
} }
NORM 110 { NORM 110 {
O compound; O compound;
......
directoryPath : "/home/joachim/git/KeYJoana/keyjoana/testdata/FalsePositiveExamples/loop",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/LoopOverride.pdg",
entryMethod : "LoopOverride",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/LoopOverride.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int LoopOverride.testMethod(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int LoopOverride.testMethod(int, int)"}}]
\ No newline at end of file
public class LoopOverride public class LoopOverride
{ {
public static void main ( String [ ] args ) public static void main ( String [ ] args )
{ {
new LoopOverride ( ) . testMethod ( 1 , 2 ) ; new LoopOverride ( ) . testMethod ( 1 , 2 ) ;
} }
public int testMethod ( int high , int low ) public int testMethod ( int high , int low )
{ {
int l = loopOverride ( low , high ) ; int l = loopOverride ( low , high ) ;
return l ; return l ;
} }
public int loopOverride ( int l , int h ) public int loopOverride ( int l , int h )
{ {
int y = l ; int y = l ;
for ( int i = 0 ; for ( int i = 0 ;
i < 5 ; i < 5 ;
i ++ ) i ++ )
{ {
if ( i < 4 ) if ( i < 4 )
{ {
l = l + h ; l = l + h ;
} }
else else
{ {
assume(false); assume(false);
l = y ; l = y ;
} }
} }
return l ; return l ;
} }
/*@ /*@
@ requires true; @ requires true;
@ ensures b; @ ensures b;
......
public class LoopOverride public class LoopOverride
{ {
public static void main ( String [ ] args ) public static void main ( String [ ] args )
{ {
new LoopOverride ( ) . testMethod ( 1 , 2 ) ; new LoopOverride ( ) . testMethod ( 1 , 2 ) ;
} }
public int testMethod ( int high , int low ) public int testMethod ( int high , int low )
{ {
int l = loopOverride ( low , high ) ; int l = loopOverride ( low , high ) ;
return l ; return l ;
} }
public int loopOverride ( int l , int h ) public int loopOverride ( int l , int h )
{ {
int y = l ; int y = l ;
for ( int i = 0 ; for ( int i = 0 ;
i < 5 ; i < 5 ;
i ++ ) i ++ )
{ {
if ( i < 4 ) if ( i < 4 )
{ {
l = l + h ; l = l + h ;
} }
else else
{ {
l = y ; l = y ;
} }
} }
return l ; return l ;
} }
} }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment