Commit 4fff3159 authored by Joachim Müssig's avatar Joachim Müssig

create OCnewest version of false positiv examples 'excluding'

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