Commit 55e3f655 authored by Joachim Müssig's avatar Joachim Müssig

add some jUnit tests and the corresponding data

parent b736eaae
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/TestCases/testdata/build/src.jar",
......
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/TestCases/testdata/build/src.jar",
......
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/TestCases/testdata/build/src.jar",
......
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/TestCases/testdata/build/src.jar",
pathToJavaFile : "/home/joachim/JoanaKeYBeispiele/TestCases/src/",
pathToSDG : "/home/joachim/JoanaKeYBeispiele/TestCases/SDG/BranchAnalysisTest4.pdg",
entryMethod : "BranchAnalysisTest4",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "/home/joachim/JoanaKeYBeispiele/TestCases/SDG/BranchAnalysisTest4.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "32", sdgNode : "BranchAnalysisTest4.test4(Z)I -> param 1 <param> 1"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "39", sdgNode : "BranchAnalysisTest4.test4(Z)I -> return #(1) BranchAnalysisTest4.test4(Z)I"}}]
\ No newline at end of file
directoryPath : "",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/TestCases/testdata/build/src.jar",
pathToJavaFile : "/home/joachim/JoanaKeYBeispiele/TestCases/src/",
pathToSDG : "/home/joachim/JoanaKeYBeispiele/TestCases/SDG/IFLoop.pdg",
entryMethod : "IFLoop",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "/home/joachim/JoanaKeYBeispiele/TestCases/SDG/IFLoop.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int IFLoop.test(boolean)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int IFLoop.test(boolean):17) return v8"}}]
\ No newline at end of file
SDG "BranchAnalysisTest4.main(java.lang.String[])" root 12 {
ENTR 1 {
O entry;
V "BranchAnalysisTest4.main(java.lang.String[])";
P 4;
S "BranchAnalysisTest4.java":0,0-0,0;
B "BranchAnalysisTest4.main([Ljava/lang/String;)V":-1;
Z 0;
C "Application";
HE 2;
HE 3;
HE 4;
HE 5;
HE 9;
PS 3;
PS 4;
CF 4;
CD 5;
CD 9;
CE 2;
CE 3;
CE 4;
}
EXIT 2 {
O exit;
V "BranchAnalysisTest4.main(java.lang.String[])";
T "V";
P 4;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<exit>":-2;
Z 0;
RF 61;
}
FRMO 3 {
O form-out;
V "_exception_";
T "Ljava/lang/Exception";
P 4;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<exception>":-2;
CF 2: "exc";
PO 28;
}
FRMI 4 {
O form-in;
V "param 1";
T "[Ljava/lang/String";
P 4;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
CF 6;
}
CALL 5 {
O call;
V "v5 = test4(#(0))";
T "I";
P 4;
S "BranchAnalysisTest4.java":5,0-5,0;
B "BranchAnalysisTest4.main([Ljava/lang/String;)V":1;
Z 0;
HE 6;
HE 7;
HE 8;
PS 6;
PS 7;
PS 8;
CF 60;
CE 6;
CE 7;
CE 8;
CE 60;
CL 29: "virtual";
}
ACTI 6 {
O act-in;
V "param 1 [#(0)]";
T "Z";
P 4;
S "BranchAnalysisTest4.java":5,0-5,0;
B "<param> 1":-2;
Z 0;
CF 5;
PI 32;
}
ACTO 7 {
O act-out;
V "ret 0";
T "I";
P 4;
S "BranchAnalysisTest4.java":5,0-5,0;
B "<exit>":-2;
Z 0;
CF 8;
}
ACTO 8 {
O act-out;
V "ret _exception_";
T "Ljava/lang/Exception";
P 4;
S "BranchAnalysisTest4.java":5,0-5,0;
B "<exception>":-2;
Z 0;
HE 60;
CF 9;
CE 60;
}
NORM 9 {
O compound;
V "return";
T "V";
P 4;
S "BranchAnalysisTest4.java":6,0-6,0;
B "BranchAnalysisTest4.main([Ljava/lang/String;)V":5;
Z 0;
CF 2;
}
ENTR 12 {
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 13;
HE 14;
HE 15;
PS 14;
CF 15;
CD 15;
CE 13;
CE 14;
}
EXIT 13 {
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 14 {
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 13: "exc";
}
CALL 15 {
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 16;
HE 17;
HE 55;
HE 58;
PS 16;
CF 58;
CD 17;
CE 16;
CE 55;
CE 58;
}
ACTO 16 {
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 14: "exc";
DD 14;
}
NORM 17 {
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 18;
HE 20;
CF 14: "exc";
CF 18;
CD 14;
CD 18;
CD 20;
DD 20;
DD 24;
DD 27;
}
NORM 18 {
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 20;
DD 19;
}
EXPR 19 {
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 21;
CE 21;
DD 21;
}
NORM 20 {
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 21;
HE 22;
HE 23;
PS 21;
CF 14: "exc";
CF 22;
CF 24;
CD 14;
CD 21;
CD 22;
CD 23;
CE 22;
DD 19;
}
NORM 21 {
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 20;
}
NORM 22 {
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 19;
CF 19;
CE 19;
CE 20;
DD 19;
}
CALL 23 {
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 24;
HE 25;
HE 26;
HE 56;
HE 57;
HE 59;
PS 24;
PS 25;
CF 59;
CD 26;
CE 24;
CE 25;
CE 56;
CE 57;
CE 59;
}
ACTI 24 {
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 56;
CF 23;
CD 23;
DD 59;
}
ACTO 25 {
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 14: "exc";
DD 14;
DD 57;
}
CALL 26 {
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 27;
HE 28;
PS 27;
PS 28;
CF 28: "exc";
CF 61;
CE 27;
CE 28;
CE 61;
CL 1: "virtual";
}
ACTI 27 {
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;
CF 26;
PI 4;
}
ACTO 28 {
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 61;
CF 14: "exc";
CE 61;
}
ENTR 29 {
O entry;
V "BranchAnalysisTest4.test4(boolean)";
P 6;
S "BranchAnalysisTest4.java":0,0-0,0;
B "BranchAnalysisTest4.test4(Z)I":-1;
Z 0;
C "Application";
HE 30;
HE 31;
HE 32;
HE 33;
HE 38;
HE 39;
PS 30;
PS 31;
PS 32;
CF 32;
CD 33;
CD 37;
CD 38;
CD 39;
CE 30;
CE 31;
CE 32;
}
EXIT 30 {
O exit;
V "BranchAnalysisTest4.test4(boolean)";
T "I";
P 6;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<exit>":-2;
Z 0;
RF 60;
PO 7;
}
FRMO 31 {
O form-out;
V "_exception_";
T "Ljava/lang/Exception";
P 6;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<exception>":-2;
CF 30: "exc";
PO 8;
}
FRMI 32 {
O form-in;
V "param 1";
T "Z";
P 6;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
CF 33;
DD 33;
}
PRED 33 {
O IF;
V "if (p1 $null == #(0)) goto 10";
T "Z";
P 6;
S "BranchAnalysisTest4.java":11,0-11,0;
B "BranchAnalysisTest4.test4(Z)I":5;
Z 0;
HE 34;
HE 35;
HE 36;
HE 37;
CF 34;
CF 36;
CD 34;
CD 35;
CD 36;
CD 37;
}
EXPR 34 {
O assign;
V "v8 = #(2) * #(2)";
T "Ljava/lang/Object";
P 6;
S "BranchAnalysisTest4.java":13,0-13,0;
B "BranchAnalysisTest4.test4(Z)I":10;
Z 0;
CF 35;
DD 37;
}
NORM 35 {
O compound;
V "goto 19";
T "Ljava/lang/Object";
P 6;
S "BranchAnalysisTest4.java":13,0-13,0;
B "BranchAnalysisTest4.test4(Z)I":12;
Z 0;
CF 37;
}
EXPR 36 {
O assign;
V "v7 = #(2) * #(3)";
T "Ljava/lang/Object";
P 6;
S "BranchAnalysisTest4.java":17,0-17,0;
B "BranchAnalysisTest4.test4(Z)I":17;
Z 0;
CF 37;
DD 37;
}
EXPR 37 {
O assign;
V "PHI v9 = v8, v7";
P 6;
S "BranchAnalysisTest4.java":0,0-0,0;
B "<phi>":-8;
Z 0;
CF 38;
DD 38;
}
EXPR 38 {
O assign;
V "v10 = v9 + #(1)";
T "Ljava/lang/Object";
P 6;
S "BranchAnalysisTest4.java":19,0-19,0;
B "BranchAnalysisTest4.test4(Z)I":19;
Z 0;
CF 39;
}
NORM 39 {
O compound;
V "return #(1)";
T "I";
P 6;
S "BranchAnalysisTest4.java":20,0-20,0;
B "BranchAnalysisTest4.test4(Z)I":23;
Z 0;
CF 30;
DD 30;
}
ACTO 55 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 16: "exc";
CF 17;
}
ACTO 56 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 25: "exc";
CF 27;
DD 57;
}
NORM 57 {
O compound;
V "immutable";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 56;
DD 17;
}
NORM 58 {
O compound;
V "many2many";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 55;
DD 16;
DD 55;
}
NORM 59 {
O compound;
V "many2many";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 57;
DD 25;
DD 56;
}
NORM 60 {
O compound;
V "CALL_RET";
P 4;
S "BranchAnalysisTest4.java":5,0-5,0;
B "BranchAnalysisTest4.main([Ljava/lang/String;)V":-9;
Z 0;
CF 7;
}
NORM 61 {
O compound;
V "CALL_RET";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
Z 0;
CF 13;
}
Thread 0 {
Entry 12;
Exit 13;
Fork 0;
Join 0;
Context null;
Dynamic false;
}
}
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 50, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {
}}},
{ "sdg_node" : 40, "cg_node" : {"id" : 3, "cg_node_id" :8, "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"