Commit 5f94a7d1 authored by Joachim Müssig's avatar Joachim Müssig

create newest version of false positiv examples

parent 8fefd96b
......@@ -13,7 +13,7 @@ HE 4;
HE 5;
HE 6;
HE 9;
HE 106;
HE 111;
PS 3;
PS 4;
CF 4;
......@@ -23,7 +23,7 @@ CD 9;
CE 2;
CE 3;
CE 4;
CE 106;
CE 111;
}
EXIT 2 {
O exit;
......@@ -43,7 +43,7 @@ P 4;
S "ArrayAccess.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 106: "exc";
CF 111: "exc";
PO 36;
}
FRMI 4 {
......@@ -55,7 +55,7 @@ S "ArrayAccess.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
PS 106;
PS 111;
CF 5;
}
NORM 5 {
......@@ -80,13 +80,13 @@ B "ArrayAccess.main([Ljava/lang/String;)V":4;
Z 0;
HE 7;
HE 8;
HE 107;
HE 112;
PS 7;
PS 8;
CF 118;
CE 7;
CE 8;
CE 107;
CE 112;
CE 118;
CL 37: "virtual";
}
......@@ -98,11 +98,11 @@ P 4;
S "ArrayAccess.java":5,0-5,0;
B "<param> 0":-2;
Z 0;
PS 107;
PS 112;
CF 6;
CD 6;
SU 8;
SU 107;
SU 112;
PI 40;
}
ACTO 8 {
......@@ -214,7 +214,7 @@ P 4;
S "ArrayAccess.java":6,0-6,0;
B "ArrayAccess.main([Ljava/lang/String;)V":13;
Z 0;
CF 106;
CF 111;
}
ENTR 20 {
O entry;
......@@ -263,13 +263,13 @@ Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 24;
HE 25;
HE 110;
HE 108;
HE 115;
PS 24;
CF 115;
CD 25;
CE 24;
CE 110;
CE 108;
CE 115;
}
ACTO 24 {
......@@ -383,7 +383,7 @@ U "java.lang.Object.<init>()V";
HE 32;
HE 33;
HE 34;
HE 111;
HE 109;
HE 113;
HE 116;
PS 32;
......@@ -392,7 +392,7 @@ CF 116;
CD 34;
CE 32;
CE 33;
CE 111;
CE 109;
CE 113;
CE 116;
}
......@@ -404,7 +404,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
PS 111;
PS 109;
CF 31;
CD 31;
DD 116;
......@@ -431,13 +431,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 35;
HE 36;
HE 112;
HE 110;
PS 35;
PS 36;
CF 120;
CE 35;
CE 36;
CE 112;
CE 110;
CE 120;
CL 1: "virtual";
}
......@@ -449,7 +449,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
PS 112;
PS 110;
CF 34;
PI 4;
}
......@@ -478,7 +478,7 @@ HE 38;
HE 39;
HE 40;
HE 41;
HE 108;
HE 106;
PS 39;
PS 40;
CF 40;
......@@ -486,7 +486,7 @@ CD 41;
CE 38;
CE 39;
CE 40;
CE 108;
CE 106;
}
EXIT 38 {
O exit;
......@@ -506,7 +506,7 @@ P 6;
S "ArrayAccess.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 108: "exc";
CF 106: "exc";
PO 8;
}
FRMI 40 {
......@@ -518,7 +518,7 @@ S "ArrayAccess.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
LD ["null"];
PS 108;
PS 106;
CF 42;
DD 42;
}
......@@ -534,7 +534,7 @@ U "java.lang.Object.<init>()V";
HE 42;
HE 43;
HE 44;
HE 109;
HE 107;
HE 114;
HE 117;
PS 42;
......@@ -543,7 +543,7 @@ CF 117;
CD 44;
CE 42;
CE 43;
CE 109;
CE 107;
CE 114;
CE 117;
}
......@@ -555,7 +555,7 @@ P 6;
S "ArrayAccess.java":1,0-1,0;
B "<param> 0":-2;
Z 0;
PS 109;
PS 107;
CF 41;
CD 41;
DD 117;
......@@ -580,7 +580,7 @@ P 6;
S "ArrayAccess.java":1,0-1,0;
B "ArrayAccess.<init>()V":4;
Z 0;
CF 108;
CF 106;
}
ENTR 46 {
O entry;
......@@ -1169,36 +1169,14 @@ FRMO 106 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "ArrayAccess.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 2;
PO 112;
}
ACTO 107 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "ArrayAccess.java":5,0-5,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 8;
DH 106;
}
FRMO 108 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 6;
S "ArrayAccess.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 38;
PO 107;
PO 112;
}
ACTO 109 {
ACTO 107 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
......@@ -1209,9 +1187,9 @@ Z 0;
CF 43: "exc";
CF 44;
DD 114;
DH 108;
DH 106;
}
ACTO 110 {
ACTO 108 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
......@@ -1222,7 +1200,7 @@ Z 0;
CF 24: "exc";
CF 25;
}
ACTO 111 {
ACTO 109 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
......@@ -1234,7 +1212,7 @@ CF 33: "exc";
CF 35;
DD 113;
}
ACTO 112 {
ACTO 110 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
......@@ -1245,6 +1223,28 @@ Z 0;
CF 21;
CF 36: "exc";
}
FRMO 111 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "ArrayAccess.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 2;
PO 110;
}
ACTO 112 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "ArrayAccess.java":5,0-5,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 8;
DH 111;
}
NORM 113 {
O compound;
V "immutable";
......@@ -1252,7 +1252,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 111;
CF 109;
DD 25;
}
NORM 114 {
......@@ -1262,7 +1262,7 @@ P 6;
S "ArrayAccess.java":0,0-0,0;
B "ArrayAccess.<init>()V":-1;
Z 0;
CF 109;
CF 107;
DD 40;
}
NORM 115 {
......@@ -1272,9 +1272,9 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 110;
CF 108;
DD 24;
DD 110;
DD 108;
}
NORM 116 {
O compound;
......@@ -1285,7 +1285,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 113;
DD 33;
DD 111;
DD 109;
}
NORM 117 {
O compound;
......@@ -1296,7 +1296,7 @@ B "ArrayAccess.<init>()V":-1;
Z 0;
CF 114;
DD 43;
DD 109;
DD 107;
}
NORM 118 {
O compound;
......@@ -1305,7 +1305,7 @@ P 4;
S "ArrayAccess.java":5,0-5,0;
B "ArrayAccess.main([Ljava/lang/String;)V":-9;
Z 0;
CF 107;
CF 112;
}
NORM 119 {
O compound;
......@@ -1325,7 +1325,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
Z 0;
CF 112;
CF 110;
}
NORM 121 {
O compound;
......
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/mihai/workspace/keyjoana/diss/array/testdata/build/src.jar",
pathToJavaFile : "/home/mihai/workspace/keyjoana/diss/array/src/",
pathToSDG : "/home/mihai/workspace/keyjoana/diss/array/SDG/ArrayAccess.pdg",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/ArrayAccess.pdg",
entryMethod : "ArrayAccess",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "/home/mihai/workspace/keyjoana/diss/array/SDG/ArrayAccess.dispro",
pathToSaver : "SDG/ArrayAccess.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int ArrayAccess.testMethod(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int ArrayAccess.testMethod(int, int)"}}]
\ No newline at end of file
public class ArrayAccess
{
public static void main ( String [ ] args )
{
new ArrayAccess ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = arrayAccess ( low , high ) ;
return l ;
}
private int arrayAccess ( int l , int h )
{
int [ ] array = new int [ 3 ] ;
array [ 0 ] = l ;
array [ 1 ] = h ;
array [ 2 ] = array [ 1 ] ;
return array [ 0 ] ;
}
public static void main ( String [ ] args )
{
new ArrayAccess ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = arrayAccess ( low , high ) ;
return l ;
}
private int arrayAccess ( int l , int h )
{
int [ ] array = new int [ 3 ] ;
array [ 0 ] = l ;
array [ 1 ] = h ;
array [ 2 ] = array [ 1 ] ;
return array [ 0 ] ;
}
/*@
@ requires true;
@ ensures b;
......
public class ArrayAccess
{
public static void main ( String [ ] args )
{
new ArrayAccess ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = arrayAccess ( low , high ) ;
return l ;
}
private int arrayAccess ( int l , int h )
{
int [ ] array = new int [ 3 ] ;
array [ 0 ] = l ;
array [ 1 ] = h ;
array [ 2 ] = array [ 1 ] ;
return array [ 0 ] ;
}
public static void main ( String [ ] args )
{
new ArrayAccess ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = arrayAccess ( low , high ) ;
return l ;
}
private int arrayAccess ( int l , int h )
{
int [ ] array = new int [ 3 ] ;
array [ 0 ] = l ;
array [ 1 ] = h ;
array [ 2 ] = array [ 1 ] ;
return array [ 0 ] ;
}
}
......@@ -14,7 +14,7 @@ HE 5;
HE 6;
HE 9;
HE 15;
HE 118;
HE 121;
PS 3;
PS 4;
CF 4;
......@@ -25,7 +25,7 @@ CD 15;
CE 2;
CE 3;
CE 4;
CE 118;
CE 121;
}
EXIT 2 {
O exit;
......@@ -44,7 +44,7 @@ T "Ljava/lang/Exception";
P 4;
S "Branching.java":0,0-0,0;
B "<exception>":-2;
CF 118: "exc";
CF 121: "exc";
PO 36;
}
FRMI 4 {
......@@ -56,7 +56,7 @@ S "Branching.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
PS 118;
PS 121;
CF 5;
}
NORM 5 {
......@@ -81,13 +81,13 @@ B "Branching.main([Ljava/lang/String;)V":4;
Z 0;
HE 7;
HE 8;
HE 119;
HE 122;
PS 7;
PS 8;
CF 130;
CE 7;
CE 8;
CE 119;
CE 122;
CE 130;
CL 37: "virtual";
}
......@@ -99,11 +99,11 @@ P 4;
S "Branching.java":5,0-5,0;
B "<param> 0":-2;
Z 0;
PS 119;
PS 122;
CF 6;
CD 6;
SU 8;
SU 119;
SU 122;
PI 40;
}
ACTO 8 {
......@@ -212,7 +212,7 @@ P 4;
S "Branching.java":6,0-6,0;
B "Branching.main([Ljava/lang/String;)V":13;
Z 0;
CF 118;
CF 121;
}
ENTR 20 {
O entry;
......@@ -261,13 +261,13 @@ Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 24;
HE 25;
HE 122;
HE 118;
HE 127;
PS 24;
CF 127;
CD 25;
CE 24;
CE 122;
CE 118;
CE 127;
}
ACTO 24 {
......@@ -381,7 +381,7 @@ U "java.lang.Object.<init>()V";
HE 32;
HE 33;
HE 34;
HE 123;
HE 119;
HE 125;
HE 128;
PS 32;
......@@ -390,7 +390,7 @@ CF 128;
CD 34;
CE 32;
CE 33;
CE 123;
CE 119;
CE 125;
CE 128;
}
......@@ -402,7 +402,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
PS 123;
PS 119;
CF 31;
CD 31;
DD 128;
......@@ -429,13 +429,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 35;
HE 36;
HE 124;
HE 120;
PS 35;
PS 36;
CF 132;
CE 35;
CE 36;
CE 124;
CE 120;
CE 132;
CL 1: "virtual";
}
......@@ -447,7 +447,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
PS 124;
PS 120;
CF 34;
PI 4;
}
......@@ -475,7 +475,7 @@ HE 38;
HE 39;
HE 40;
HE 41;
HE 120;
HE 123;
PS 39;
PS 40;
CF 40;
......@@ -483,7 +483,7 @@ CD 41;
CE 38;
CE 39;
CE 40;
CE 120;
CE 123;
}
EXIT 38 {
O exit;
......@@ -503,7 +503,7 @@ P 6;
S "Branching.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 120: "exc";
CF 123: "exc";
PO 8;
}
FRMI 40 {
......@@ -515,7 +515,7 @@ S "Branching.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
LD ["null"];
PS 120;
PS 123;
CF 42;
DD 42;
}
......@@ -531,7 +531,7 @@ U "java.lang.Object.<init>()V";
HE 42;
HE 43;
HE 44;
HE 121;
HE 124;
HE 126;
HE 129;
PS 42;
......@@ -540,7 +540,7 @@ CF 129;