Commit c008fbd2 authored by Joachim Müssig's avatar Joachim Müssig

create newest version of false positiv example 'ifloop2' and 'lostInCast'

parent 42ea5499
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples (Kopie)/IFLoop2/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/IFLoop.pdg",
entryMethod : "IFLoop",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/IFLoop.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "98", sdgNode : "IFLoop.callInsecure()V -> [R] |0|UNIQ(high) FRMI"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "99", sdgNode : "IFLoop.callInsecure()V -> [M] |0|UNIQ(low) FRMO"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 98, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {
}}},
{ "sdg_node" : 36, "cg_node" : {"id" : 3, "cg_node_id" :8, "ir" : {
}}},
{ "sdg_node" : 54, "cg_node" : {"id" : 6, "cg_node_id" :11, "ir" : {
}}},
{ "sdg_node" : 105, "cg_node" : {"id" : 6, "cg_node_id" :11, "ir" : {
}}},
{ "sdg_node" : 90, "cg_node" : {"id" : 7, "cg_node_id" :12, "ir" : {
}}},
{ "sdg_node" : 91, "cg_node" : {"id" : 7, "cg_node_id" :12, "ir" : {
}}},
{ "sdg_node" : 45, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {
}}},
],
"cg_nodes" : [
{"id" : 0, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 1, "cg_node_id" :0, "ir" : {
}},
{"id" : 2, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 3, "cg_node_id" :8, "ir" : {
}},
{"id" : 4, "cg_node_id" :9, "ir" : {
}},
{"id" : 5, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 6, "cg_node_id" :11, "ir" : {
}},
{"id" : 7, "cg_node_id" :12, "ir" : {
}},
],
"localPointerKeys" : [{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
{"id" : 4, "value_number" : 1, "node" : 4
},
{"id" : 5, "value_number" : 1, "node" : 5
},
{"id" : 6, "value_number" : 1, "node" : 6
},
{"id" : 7, "value_number" : 1, "node" : 7
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 42, "cg_node" : 9},
{ "sdg_node" : 87, "cg_node" : 12},
{ "sdg_node" : 16, "cg_node" : 0},
{ "sdg_node" : 33, "cg_node" : 8},
{ "sdg_node" : 51, "cg_node" : 11},
{ "sdg_node" : 1, "cg_node" : 5},
],
"nodeToSSA" : [{ "sdg_node" : 95, "iIndex" : 3},
{ "sdg_node" : 94, "iIndex" : 2},
{ "sdg_node" : 93, "iIndex" : 2},
{ "sdg_node" : 92, "iIndex" : 2},
{ "sdg_node" : 70, "iIndex" : 25},
{ "sdg_node" : 69, "iIndex" : 24},
{ "sdg_node" : 68, "iIndex" : 22},
{ "sdg_node" : 67, "iIndex" : 18},
{ "sdg_node" : 65, "iIndex" : 14},
{ "sdg_node" : 64, "iIndex" : 14},
{ "sdg_node" : 63, "iIndex" : 14},
{ "sdg_node" : 62, "iIndex" : 12},
{ "sdg_node" : 58, "iIndex" : 9},
{ "sdg_node" : 57, "iIndex" : 6},
{ "sdg_node" : 49, "iIndex" : 2},
{ "sdg_node" : 46, "iIndex" : 1},
{ "sdg_node" : 40, "iIndex" : 2},
{ "sdg_node" : 37, "iIndex" : 1},
{ "sdg_node" : 30, "iIndex" : 5},
{ "sdg_node" : 27, "iIndex" : 4},
{ "sdg_node" : 26, "iIndex" : 3},
{ "sdg_node" : 25, "iIndex" : 3},
{ "sdg_node" : 24, "iIndex" : 3},
{ "sdg_node" : 23, "iIndex" : 3},
{ "sdg_node" : 22, "iIndex" : 2},
{ "sdg_node" : 21, "iIndex" : 1},
{ "sdg_node" : 19, "iIndex" : 0},
{ "sdg_node" : 12, "iIndex" : 6},
{ "sdg_node" : 9, "iIndex" : 5},
{ "sdg_node" : 6, "iIndex" : 2},
{ "sdg_node" : 5, "iIndex" : 0},
]
}
\ No newline at end of file
SDG "IFLoop.main(java.lang.String[])" root 16 {
ENTR 1 {
O entry;
V "IFLoop.main(java.lang.String[])";
P 4;
S "IFLoop.java":0,0-0,0;
B "IFLoop.main([Ljava/lang/String;)V":-1;
Z 0;
C "Application";
HE 2;
HE 3;
HE 4;
HE 5;
HE 6;
HE 9;
HE 12;
HE 111;
PS 3;
PS 4;
CF 4;
CD 5;
CD 6;
CD 9;
CD 12;
CE 2;
CE 3;
CE 4;
CE 111;
}
EXIT 2 {
O exit;
V "IFLoop.main(java.lang.String[])";
T "V";
P 4;
S "IFLoop.java":0,0-0,0;
B "<exit>":-2;
Z 0;
RF 122;
}
FRMO 3 {
O form-out;
V "_exception_";
T "Ljava/lang/Exception";
P 4;
S "IFLoop.java":0,0-0,0;
B "<exception>":-2;
CF 111: "exc";
PO 32;
}
FRMI 4 {
O form-in;
V "param 1";
T "[Ljava/lang/String";
P 4;
S "IFLoop.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
PS 111;
CF 5;
}
NORM 5 {
O declaration;
V "v3 = new IFLoop";
T "LIFLoop";
P 4;
S "IFLoop.java":7,0-7,0;
B "IFLoop.main([Ljava/lang/String;)V":0;
Z 0;
CF 7;
DD 7;
DD 10;
}
CALL 6 {
O call;
V "v3.<init>()";
T "V";
P 4;
S "IFLoop.java":7,0-7,0;
B "IFLoop.main([Ljava/lang/String;)V":4;
Z 0;
HE 7;
HE 8;
HE 112;
PS 7;
PS 8;
CF 120;
CE 7;
CE 8;
CE 112;
CE 120;
CL 33: "virtual";
}
ACTI 7 {
O act-in;
V "this [v3]";
T "LIFLoop";
P 4;
S "IFLoop.java":7,0-7,0;
B "<param> 0":-2;
Z 0;
PS 112;
CF 6;
CD 6;
SU 8;
SU 112;
PI 36;
}
ACTO 8 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 4;
S "IFLoop.java":7,0-7,0;
B "<exception>":-2;
Z 0;
HE 120;
CF 10;
CE 120;
}
CALL 9 {
O call;
V "v3.callInsecure()";
T "V";
P 4;
S "IFLoop.java":8,0-8,0;
B "IFLoop.main([Ljava/lang/String;)V":9;
Z 0;
HE 10;
HE 11;
HE 113;
HE 114;
PS 10;
PS 11;
CF 121;
CE 10;
CE 11;
CE 113;
CE 114;
CE 121;
CL 42: "virtual";
}
ACTI 10 {
O act-in;
V "this [v3]";
T "LIFLoop";
P 4;
S "IFLoop.java":8,0-8,0;
B "<param> 0":-2;
Z 0;
PS 113;
PS 114;
CF 113;
CD 9;
SU 114;
PI 45;
}
ACTO 11 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 4;
S "IFLoop.java":8,0-8,0;
B "<exception>":-2;
Z 0;
HE 121;
CF 12;
CE 121;
}
NORM 12 {
O compound;
V "return";
T "V";
P 4;
S "IFLoop.java":9,0-9,0;
B "IFLoop.main([Ljava/lang/String;)V":12;
Z 0;
CF 111;
}
ENTR 16 {
O entry;
V "com.ibm.wala.FakeRootClass.fakeRootMethod()";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
C "Primordial";
HE 17;
HE 18;
HE 19;
PS 18;
CF 19;
CD 19;
CE 17;
CE 18;
}
EXIT 17 {
O exit;
V "com.ibm.wala.FakeRootClass.fakeRootMethod()";
T "V";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<exit>":-2;
Z 0;
}
FRMO 18 {
O form-out;
V "_exception_";
T "Ljava/lang/Exception";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 17: "exc";
}
CALL 19 {
O call;
V "fakeWorldClinit()";
T "V";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 20;
HE 21;
HE 102;
HE 117;
PS 20;
CF 117;
CD 21;
CE 20;
CE 102;
CE 117;
}
ACTO 20 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 18: "exc";
DD 18;
}
NORM 21 {
O declaration;
V "v3 = new java.lang.String[]";
T "[Ljava/lang/String";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 22;
HE 24;
CF 18: "exc";
CF 22;
CD 18;
CD 22;
CD 24;
DD 24;
DD 28;
DD 31;
}
NORM 22 {
O declaration;
V "v5 = new java.lang.String";
T "Ljava/lang/String";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 24;
DD 23;
}
EXPR 23 {
O modify;
V "v3[#(0)] = v5";
T "Ljava/lang/String";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 25;
CE 25;
DD 25;
}
NORM 24 {
O compound;
V "base";
T "[Ljava/lang/Object";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 25;
HE 26;
HE 27;
PS 25;
CF 18: "exc";
CF 26;
CF 28;
CD 18;
CD 25;
CD 26;
CD 27;
CE 26;
DD 23;
}
NORM 25 {
O compound;
V "field [java.lang.Object]";
T "Ljava/lang/Object";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 24;
}
NORM 26 {
O compound;
V "index";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 23;
CF 23;
CE 23;
CE 24;
DD 23;
}
CALL 27 {
O call;
V "v3.<init>()";
T "V";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
U "java.lang.Object.<init>()V";
HE 28;
HE 29;
HE 30;
HE 103;
HE 115;
HE 118;
PS 28;
PS 29;
CF 118;
CD 30;
CE 28;
CE 29;
CE 103;
CE 115;
CE 118;
}
ACTI 28 {
O act-in;
V "this [v3]";
T "Ljava/lang/Object";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
PS 103;
CF 27;
CD 27;
DD 118;
}
ACTO 29 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 18: "exc";
DD 18;
DD 115;
}
CALL 30 {
O call;
V "main(v3)";
T "V";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 31;
HE 32;
HE 104;
PS 31;
PS 32;
CF 122;
CE 31;
CE 32;
CE 104;
CE 122;
CL 1: "virtual";
}
ACTI 31 {
O act-in;
V "param 1 [v3]";
T "[Ljava/lang/String";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
PS 104;
CF 30;
PI 4;
}
ACTO 32 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<exception>":-2;
Z 0;
HE 122;
CF 18: "exc";
CE 122;
}
ENTR 33 {
O entry;
V "IFLoop.<init>()";
P 6;
S "IFLoop.java":0,0-0,0;
B "IFLoop.<init>()V":-1;
Z 0;
C "Application";
HE 34;
HE 35;
HE 36;
HE 37;
HE 109;
PS 35;
PS 36;
CF 36;
CD 37;
CE 34;
CE 35;
CE 36;
CE 109;
}
EXIT 34 {
O exit;
V "IFLoop.<init>()";
T "V";
P 6;
S "IFLoop.java":0,0-0,0;
B "<exit>":-2;
Z 0;
RF 120;
}
FRMO 35 {
O form-out;
V "_exception_";
T "Ljava/lang/Exception";
P 6;
S "IFLoop.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 109: "exc";
PO 8;
}
FRMI 36 {
O form-in;
V "this";
T "LIFLoop";
P 6;
S "IFLoop.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
LD ["null"];
PS 109;
CF 38;
DD 38;
}
CALL 37 {
O call;
V "p0 $null .<init>()";
T "V";
P 6;
S "IFLoop.java":1,0-1,0;
B "IFLoop.<init>()V":1;
Z 0;
U "java.lang.Object.<init>()V";
HE 38;
HE 39;
HE 40;
HE 110;
HE 116;
HE 119;
PS 38;
PS 39;
CF 119;
CD 40;
CE 38;
CE 39;
CE 110;
CE 116;
CE 119;
}