Commit 50f4c070 authored by Joachim Müssig's avatar Joachim Müssig

create newest version of false positiv example 'mixture'

parent 2256ebb4
......@@ -14,7 +14,7 @@ HE 5;
HE 6;
HE 9;
HE 15;
HE 147;
HE 144;
PS 3;
PS 4;
CF 4;
......@@ -25,7 +25,7 @@ CD 15;
CE 2;
CE 3;
CE 4;
CE 147;
CE 144;
}
EXIT 2 {
O exit;
......@@ -44,7 +44,7 @@ T "Ljava/lang/Exception";
P 4;
S "Mixture.java":0,0-0,0;
B "<exception>":-2;
CF 147: "exc";
CF 144: "exc";
PO 36;
}
FRMI 4 {
......@@ -56,7 +56,7 @@ S "Mixture.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
PS 147;
PS 144;
CF 5;
}
NORM 5 {
......@@ -81,13 +81,13 @@ B "Mixture.main([Ljava/lang/String;)V":4;
Z 0;
HE 7;
HE 8;
HE 148;
HE 145;
PS 7;
PS 8;
CF 154;
CE 7;
CE 8;
CE 148;
CE 145;
CE 154;
CL 37: "virtual";
}
......@@ -99,11 +99,11 @@ P 4;
S "Mixture.java":5,0-5,0;
B "<param> 0":-2;
Z 0;
PS 148;
PS 145;
CF 6;
CD 6;
SU 8;
SU 148;
SU 145;
PI 40;
}
ACTO 8 {
......@@ -212,7 +212,7 @@ P 4;
S "Mixture.java":6,0-6,0;
B "Mixture.main([Ljava/lang/String;)V":13;
Z 0;
CF 147;
CF 144;
}
ENTR 20 {
O entry;
......@@ -261,13 +261,13 @@ Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 24;
HE 25;
HE 142;
HE 146;
HE 151;
PS 24;
CF 151;
CD 25;
CE 24;
CE 142;
CE 146;
CE 151;
}
ACTO 24 {
......@@ -381,7 +381,7 @@ U "java.lang.Object.<init>()V";
HE 32;
HE 33;
HE 34;
HE 143;
HE 147;
HE 149;
HE 152;
PS 32;
......@@ -390,7 +390,7 @@ CF 152;
CD 34;
CE 32;
CE 33;
CE 143;
CE 147;
CE 149;
CE 152;
}
......@@ -402,7 +402,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
PS 143;
PS 147;
CF 31;
CD 31;
DD 152;
......@@ -429,13 +429,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 35;
HE 36;
HE 144;
HE 148;
PS 35;
PS 36;
CF 156;
CE 35;
CE 36;
CE 144;
CE 148;
CE 156;
CL 1: "virtual";
}
......@@ -447,7 +447,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
PS 144;
PS 148;
CF 34;
PI 4;
}
......@@ -475,7 +475,7 @@ HE 38;
HE 39;
HE 40;
HE 41;
HE 145;
HE 142;
PS 39;
PS 40;
CF 40;
......@@ -483,7 +483,7 @@ CD 41;
CE 38;
CE 39;
CE 40;
CE 145;
CE 142;
}
EXIT 38 {
O exit;
......@@ -503,7 +503,7 @@ P 6;
S "Mixture.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 145: "exc";
CF 142: "exc";
PO 8;
}
FRMI 40 {
......@@ -515,7 +515,7 @@ S "Mixture.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
LD ["null"];
PS 145;
PS 142;
CF 42;
DD 42;
}
......@@ -531,7 +531,7 @@ U "java.lang.Object.<init>()V";
HE 42;
HE 43;
HE 44;
HE 146;
HE 143;
HE 150;
HE 153;
PS 42;
......@@ -540,7 +540,7 @@ CF 153;
CD 44;
CE 42;
CE 43;
CE 146;
CE 143;
CE 150;
CE 153;
}
......@@ -552,7 +552,7 @@ P 6;
S "Mixture.java":1,0-1,0;
B "<param> 0":-2;
Z 0;
PS 146;
PS 143;
CF 41;
CD 41;
DD 153;
......@@ -577,7 +577,7 @@ P 6;
S "Mixture.java":1,0-1,0;
B "Mixture.<init>()V":4;
Z 0;
CF 145;
CF 142;
}
ENTR 46 {
O entry;
......@@ -1457,85 +1457,85 @@ Z 0;
CF 136;
DD 136;
}
ACTO 142 {
O act-out;
FRMO 142 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
P 6;
S "Mixture.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 24: "exc";
CF 25;
CF 38;
PO 145;
}
ACTO 143 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
P 6;
S "Mixture.java":1,0-1,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 33: "exc";
CF 35;
DD 149;
CF 43: "exc";
CF 44;
DD 150;
DH 142;
}
ACTO 144 {
O act-out;
FRMO 144 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
P 4;
S "Mixture.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 21;
CF 36: "exc";
CF 2;
PO 148;
}
FRMO 145 {
O form-out;
ACTO 145 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 6;
S "Mixture.java":0,0-0,0;
P 4;
S "Mixture.java":5,0-5,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 38;
PO 148;
CF 8;
DH 144;
}
ACTO 146 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 6;
S "Mixture.java":1,0-1,0;
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 43: "exc";
CF 44;
DD 150;
DH 145;
CF 24: "exc";
CF 25;
}
FRMO 147 {
O form-out;
ACTO 147 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "Mixture.java":0,0-0,0;
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 2;
PO 144;
CF 33: "exc";
CF 35;
DD 149;
}
ACTO 148 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "Mixture.java":5,0-5,0;
P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 8;
DH 147;
CF 21;
CF 36: "exc";
}
NORM 149 {
O compound;
......@@ -1544,7 +1544,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 143;
CF 147;
DD 25;
}
NORM 150 {
......@@ -1554,7 +1554,7 @@ P 6;
S "Mixture.java":0,0-0,0;
B "Mixture.<init>()V":-1;
Z 0;
CF 146;
CF 143;
DD 40;
}
NORM 151 {
......@@ -1564,9 +1564,9 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 142;
CF 146;
DD 24;
DD 142;
DD 146;
}
NORM 152 {
O compound;
......@@ -1577,7 +1577,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 149;
DD 33;
DD 143;
DD 147;
}
NORM 153 {
O compound;
......@@ -1588,7 +1588,7 @@ B "Mixture.<init>()V":-1;
Z 0;
CF 150;
DD 43;
DD 146;
DD 143;
}
NORM 154 {
O compound;
......@@ -1597,7 +1597,7 @@ P 4;
S "Mixture.java":5,0-5,0;
B "Mixture.main([Ljava/lang/String;)V":-9;
Z 0;
CF 148;
CF 145;
}
NORM 155 {
O compound;
......@@ -1615,7 +1615,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
Z 0;
CF 144;
CF 148;
}
NORM 157 {
O compound;
......
directoryPath : "/home/joachim/git/KeYJoana/keyjoana/testdata/FalsePositiveExamples/mixture",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/Mixture.pdg",
entryMethod : "Mixture",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/Mixture.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int Mixture.testMethod(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int Mixture.testMethod(int, int)"}}]
\ No newline at end of file
public class Mixture
{
public static void main ( String [ ] args )
{
new Mixture ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = mixture ( low , high ) ;
return l ;
}
public int mixture ( int low , int high )
{
int i = identity ( low , high ) ;
int j = precondition ( low , high ) ;
int k = secure ( low ) ;
return i + j + k ;
}
private int secure ( int low )
{
return low ;
}
public int identity ( int l , int h )
{
l = l + h ;
l = l - h ;
return l ;
}
public int precondition ( int l , int h )
{
int x = 0 ;
if ( x > 0 )
{
l = h ;
}
return l ;
}
public static void main ( String [ ] args )
{
new Mixture ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = mixture ( low , high ) ;
return l ;
}
public int mixture ( int low , int high )
{
int i = identity ( low , high ) ;
int j = precondition ( low , high ) ;
int k = secure ( low ) ;
return i + j + k ;
}
private int secure ( int low )
{
return low ;
}
public int identity ( int l , int h )
{
l = l + h ;
l = l - h ;
return l ;
}
public int precondition ( int l , int h )
{
int x = 0 ;
if ( x > 0 )
{
l = h ;
}
return l ;
}
/*@
@ requires true;
@ ensures b;
......
public class Mixture
{
public static void main ( String [ ] args )
{
new Mixture ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = mixture ( low , high ) ;
return l ;
}
public int mixture ( int low , int high )
{
int i = identity ( low , high ) ;
int j = precondition ( low , high ) ;
int k = secure ( low ) ;
return i + j + k ;
}
private int secure ( int low )
{
return low ;
}
public int identity ( int l , int h )
{
l = l + h ;
l = l - h ;
return l ;
}
public int precondition ( int l , int h )
{
int x = 0 ;
if ( x > 0 )
{
l = h ;
}
return l ;
}
public static void main ( String [ ] args )
{
new Mixture ( ) . testMethod ( 1 , 2 ) ;
}
public int testMethod ( int high , int low )
{
int l = mixture ( low , high ) ;
return l ;
}
public int mixture ( int low , int high )
{
int i = identity ( low , high ) ;
int j = precondition ( low , high ) ;
int k = secure ( low ) ;
return i + j + k ;
}
private int secure ( int low )
{
return low ;
}
public int identity ( int l , int h )
{
l = l + h ;
l = l - h ;
return l ;
}
public int precondition ( int l , int h )
{
int x = 0 ;
if ( x > 0 )
{
l = h ;
}
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