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

create newest version of false positiv example 'plusminusMulti'

parent 1761487e
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/Custom/Multi",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/MultiSource.pdg",
entryMethod : "MultiSource",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/MultiSource.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int MultiSource.callmulti(int, int, int)"}},
{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 2 of method int MultiSource.callmulti(int, int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int MultiSource.callmulti(int, int, int):6) return v6"}}]
\ No newline at end of file
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/Custom/Multi",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/MultiSource.pdg",
entryMethod : "MultiSource",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/MultiSource.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "42", sdgNode : "MultiSource.callmulti(III)I -> param 1 FRMI"}},
{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "43", sdgNode : "MultiSource.callmulti(III)I -> param 2 FRMI"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "40", sdgNode : "MultiSource.callmulti(III)I -> MultiSource.callmulti(int,int,int) EXIT"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
],
"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"
}},
],
"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
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 22, "cg_node" : 0},
{ "sdg_node" : 39, "cg_node" : 8},
{ "sdg_node" : 55, "cg_node" : 10},
{ "sdg_node" : 1, "cg_node" : 5},
],
"nodeToSSA" : [{ "sdg_node" : 66, "iIndex" : 21},
{ "sdg_node" : 65, "iIndex" : 18},
{ "sdg_node" : 64, "iIndex" : 14},
{ "sdg_node" : 63, "iIndex" : 10},
{ "sdg_node" : 62, "iIndex" : 6},
{ "sdg_node" : 61, "iIndex" : 2},
{ "sdg_node" : 51, "iIndex" : 4},
{ "sdg_node" : 45, "iIndex" : 3},
{ "sdg_node" : 36, "iIndex" : 5},
{ "sdg_node" : 33, "iIndex" : 4},
{ "sdg_node" : 32, "iIndex" : 3},
{ "sdg_node" : 31, "iIndex" : 3},
{ "sdg_node" : 30, "iIndex" : 3},
{ "sdg_node" : 29, "iIndex" : 3},
{ "sdg_node" : 28, "iIndex" : 2},
{ "sdg_node" : 27, "iIndex" : 1},
{ "sdg_node" : 25, "iIndex" : 0},
{ "sdg_node" : 17, "iIndex" : 5},
{ "sdg_node" : 11, "iIndex" : 3},
{ "sdg_node" : 10, "iIndex" : 2},
{ "sdg_node" : 9, "iIndex" : 2},
{ "sdg_node" : 8, "iIndex" : 1},
{ "sdg_node" : 7, "iIndex" : 1},
{ "sdg_node" : 6, "iIndex" : 0},
{ "sdg_node" : 5, "iIndex" : 0},
]
}
\ No newline at end of file
public class MultiSource
{
public static int h1 , h2 , l ;
public static void main ( String args [ ] )
{
callmulti ( h1 , h2 , l ) ;
}
public static int callmulti ( int h1 , int h2 , int l )
{
return multi ( h1 , h2 , l ) ;
}
public static int multi ( int h1 , int h2 , int l )
{
l = l + h1 ;
l = l - h1 ;
l = l + h2 ;
l = l - h2 ;
//sliced: h1 = h1 + h2 ;
return l ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class MultiSource
{
public static int h1 , h2 , l ;
public static void main ( String args [ ] )
{
callmulti ( h1 , h2 , l ) ;
}
public static int callmulti ( int h1 , int h2 , int l )
{
return multi ( h1 , h2 , l ) ;
}
public static int multi ( int h1 , int h2 , int l )
{
l = l + h1 ;
l = l - h1 ;
l = l + h2 ;
l = l - h2 ;
//sliced: h1 = h1 + h2 ;
return l ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class MultiSource
{
public static int h1 , h2 , l ;
public static void main ( String args [ ] )
{
callmulti ( h1 , h2 , l ) ;
}
public static int callmulti ( int h1 , int h2 , int l )
{
return multi ( h1 , h2 , l ) ;
}
public static int multi ( int h1 , int h2 , int l )
{
l = l + h1 ;
l = l - h1 ;
l = l + h2 ;
l = l - h2 ;
//sliced: h1 = h1 + h2 ;
return l ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class MultiSource
{
public static int h1 , h2 , l ;
public static void main ( String args [ ] )
{
callmulti ( h1 , h2 , l ) ;
}
public static int callmulti ( int h1 , int h2 , int l )
{
return multi ( h1 , h2 , l ) ;
}
public static int multi ( int h1 , int h2 , int l )
{
l = l + h1 ;
l = l - h1 ;
l = l + h2 ;
l = l - h2 ;
//sliced: h1 = h1 + h2 ;
return l ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class MultiSource
{
public static int h1 , h2 , l ;
public static void main ( String args [ ] )
{
callmulti ( h1 , h2 , l ) ;
}
public static int callmulti ( int h1 , int h2 , int l )
{
return multi ( h1 , h2 , l ) ;
}
public static int multi ( int h1 , int h2 , int l )
{
l = l + h1 ;
l = l - h1 ;
l = l + h2 ;
l = l - h2 ;
h1 = h1 + h2 ;
return l ;
}
}
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