Commit 1761487e authored by Joachim Müssig's avatar Joachim Müssig

create newest version of false positiv example 'plusminus'

parent fadac632
directoryPath : "/home/joachim/git/KeYJoana/keyjoana/testdata/FalsePositiveExamples/plusminus",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/PlusMinusFalsePos.pdg",
entryMethod : "PlusMinusFalsePos",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/PlusMinusFalsePos.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int PlusMinusFalsePos.test(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int PlusMinusFalsePos.test(int, int)"}}]
\ No newline at end of file
public class PlusMinusFalsePos
{
public static void main ( String args [ ] )
{
new PlusMinusFalsePos ( ) . test ( 0 , 1 ) ;
}
public int test ( int high , int low )
{
int result = identity ( high , low ) ;
return result ;
}
public int identity ( int high , int low )
{
low = low + high ;
low = low - high ;
return low ;
}
public static void main ( String args [ ] )
{
new PlusMinusFalsePos ( ) . test ( 0 , 1 ) ;
}
public int test ( int high , int low )
{
int result = identity ( high , low ) ;
return result ;
}
public int identity ( int high , int low )
{
low = low + high ;
low = low - high ;
return low ;
}
/*@
@ requires true;
@ ensures b;
......
public class PlusMinusFalsePos
{
public static void main ( String args [ ] )
{
new PlusMinusFalsePos ( ) . test ( 0 , 1 ) ;
}
public int test ( int high , int low )
{
int result = identity ( high , low ) ;
return result ;
}
public int identity ( int high , int low )
{
low = low + high ;
low = low - high ;
return low ;
}
public static void main ( String args [ ] )
{
new PlusMinusFalsePos ( ) . test ( 0 , 1 ) ;
}
public int test ( int high , int low )
{
int result = identity ( high , low ) ;
return result ;
}
public int identity ( int high , int low )
{
low = low + high ;
low = low - high ;
return low ;
}
}
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