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

add secure example with interfaces

parent c008fbd2
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples (Kopie)/interface-noleak/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/Main.pdg",
entryMethod : "Main",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/Main.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int Main.callNoLeak(int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int Main.callNoLeak(int):4) return v4"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 85, "cg_node" : {"id" : 4, "cg_node_id" :11, "ir" : {
}}},
{ "sdg_node" : 104, "cg_node" : {"id" : 6, "cg_node_id" :14, "ir" : {
}}},
{ "sdg_node" : 94, "cg_node" : {"id" : 5, "cg_node_id" :13, "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" :0, "ir" : {
"1" : "this"
}},
{"id" : 4, "cg_node_id" :11, "ir" : {
}},
{"id" : 5, "cg_node_id" :13, "ir" : {
}},
{"id" : 6, "cg_node_id" :14, "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
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 91, "cg_node" : 13},
{ "sdg_node" : 100, "cg_node" : 14},
{ "sdg_node" : 40, "cg_node" : 12},
{ "sdg_node" : 14, "cg_node" : 0},
{ "sdg_node" : 82, "cg_node" : 11},
{ "sdg_node" : 58, "cg_node" : 10},
{ "sdg_node" : 31, "cg_node" : 1},
{ "sdg_node" : 48, "cg_node" : 8},
{ "sdg_node" : 1, "cg_node" : 5},
],
"nodeToSSA" : [{ "sdg_node" : 95, "iIndex" : 1},
{ "sdg_node" : 106, "iIndex" : 3},
{ "sdg_node" : 89, "iIndex" : 2},
{ "sdg_node" : 86, "iIndex" : 1},
{ "sdg_node" : 75, "iIndex" : 11},
{ "sdg_node" : 70, "iIndex" : 10},
{ "sdg_node" : 67, "iIndex" : 6},
{ "sdg_node" : 66, "iIndex" : 4},
{ "sdg_node" : 63, "iIndex" : 2},
{ "sdg_node" : 62, "iIndex" : 0},
{ "sdg_node" : 56, "iIndex" : 2},
{ "sdg_node" : 52, "iIndex" : 1},
{ "sdg_node" : 45, "iIndex" : 2},
{ "sdg_node" : 44, "iIndex" : 1},
{ "sdg_node" : 43, "iIndex" : 1},
{ "sdg_node" : 38, "iIndex" : 2},
{ "sdg_node" : 36, "iIndex" : 1},
{ "sdg_node" : 34, "iIndex" : 0},
{ "sdg_node" : 28, "iIndex" : 5},
{ "sdg_node" : 25, "iIndex" : 4},
{ "sdg_node" : 24, "iIndex" : 3},
{ "sdg_node" : 23, "iIndex" : 3},
{ "sdg_node" : 22, "iIndex" : 3},
{ "sdg_node" : 21, "iIndex" : 3},
{ "sdg_node" : 20, "iIndex" : 2},
{ "sdg_node" : 19, "iIndex" : 1},
{ "sdg_node" : 17, "iIndex" : 0},
{ "sdg_node" : 108, "iIndex" : 5},
{ "sdg_node" : 107, "iIndex" : 3},
{ "sdg_node" : 9, "iIndex" : 5},
{ "sdg_node" : 105, "iIndex" : 2},
{ "sdg_node" : 5, "iIndex" : 3},
{ "sdg_node" : 98, "iIndex" : 2},
]
}
\ No newline at end of file
This diff is collapsed.
public class C1 implements I
{
public int m ( int i )
{
return i ;
}
}
public class C2 implements I
{
static int si = 0 ;
public int m ( int i )
{
si = i * 3 ;
return 0 ;
}
}
public interface I
{
public int m ( int i ) ;
}
public class Main
{
public static void main ( String [ ] args )
{
int value = 5 ;
callNoLeak ( value ) ;
}
public static int callNoLeak ( int h )
{
return noLeak ( h ) ;
}
public static int noLeak ( int h )
{
I i = new C1 ( ) ;
i = new C2 ( ) ;
return i . m ( h ) ;
}
}
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