Commit 4232a5fc authored by Joachim Müssig's avatar Joachim Müssig

add example exceptionalControlFlowNoLeak2

parent a8b038ab
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/ExceptionalControlFlowNoLeak2/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/program.pdg",
entryMethod : "program",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/program.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method boolean program.callFoo(boolean)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(boolean program.callFoo(boolean):4) return v4"}}]
\ No newline at end of file
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/ExceptionalControlFlowNoLeak2/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/program.pdg",
entryMethod : "program",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/program.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "39", sdgNode : "program.callFoo(Z)Z -> param 1 FRMI"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "37", sdgNode : "program.callFoo(Z)Z -> program.callFoo(boolean) EXIT"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 84, "cg_node" : {"id" : 5, "cg_node_id" :13, "ir" : {
"1" : "this"
}}},
{ "sdg_node" : 75, "cg_node" : {"id" : 4, "cg_node_id" :12, "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" :12, "ir" : {
}},
{"id" : 5, "cg_node_id" :13, "ir" : {
"1" : "this"
}},
{"id" : 6, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
],
"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" : 14, "cg_node" : 0},
{ "sdg_node" : 36, "cg_node" : 9},
{ "sdg_node" : 81, "cg_node" : 13},
{ "sdg_node" : 31, "cg_node" : 8},
{ "sdg_node" : 72, "cg_node" : 12},
{ "sdg_node" : 1, "cg_node" : 5},
{ "sdg_node" : 46, "cg_node" : 11},
],
"nodeToSSA" : [{ "sdg_node" : 79, "iIndex" : 2},
{ "sdg_node" : 76, "iIndex" : 1},
{ "sdg_node" : 62, "iIndex" : 17},
{ "sdg_node" : 60, "iIndex" : 12},
{ "sdg_node" : 57, "iIndex" : 11},
{ "sdg_node" : 56, "iIndex" : 9},
{ "sdg_node" : 55, "iIndex" : 8},
{ "sdg_node" : 52, "iIndex" : 7},
{ "sdg_node" : 51, "iIndex" : 5},
{ "sdg_node" : 50, "iIndex" : 4},
{ "sdg_node" : 44, "iIndex" : 2},
{ "sdg_node" : 40, "iIndex" : 1},
{ "sdg_node" : 34, "iIndex" : 1},
{ "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" : 12, "iIndex" : 3},
{ "sdg_node" : 8, "iIndex" : 1},
{ "sdg_node" : 5, "iIndex" : 0},
]
}
\ No newline at end of file
public class program
{
public static class T extends Exception
{
}
static boolean foo ( boolean h )
{
boolean x = false ;
try
{
if ( h )
{
throw new T ( ) ;
}
else
{
throw new T ( ) ;
}
}
catch ( T t )
{
x = true ;
}
return x ;
}
public static void main ( String [ ] args )
{
callFoo ( randBool ( ) ) ;
}
public static boolean callFoo ( boolean h )
{
return foo ( h ) ;
}
static boolean randBool ( )
{
return true ;
}
static int randInt ( )
{
return 42 ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class program
{
public static class T extends Exception
{
}
static boolean foo ( boolean h )
{
boolean x = false ;
try
{
if ( h )
{
throw new T ( ) ;
}
else
{
throw new T ( ) ;
}
}
catch ( T t )
{
x = true ;
}
return x ;
}
public static void main ( String [ ] args )
{
callFoo ( randBool ( ) ) ;
}
public static boolean callFoo ( boolean h )
{
return foo ( h ) ;
}
static boolean randBool ( )
{
return true ;
}
static int randInt ( )
{
return 42 ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class program
{
public static class T extends Exception
{
}
static boolean foo ( boolean h )
{
boolean x = false ;
try
{
if ( h )
{
throw new T ( ) ;
}
else
{
throw new T ( ) ;
}
}
catch ( T t )
{
x = true ;
}
return x ;
}
public static void main ( String [ ] args )
{
callFoo ( randBool ( ) ) ;
}
public static boolean callFoo ( boolean h )
{
return foo ( h ) ;
}
static boolean randBool ( )
{
return true ;
}
static int randInt ( )
{
return 42 ;
}
}
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