create newest version of false positiv example 'nested'

fadac632 · Joachim Müssig · 76480379 · fadac632 · fadac632 · fadac632
Commit fadac632 authored Nov 22, 2019 by Joachim Müssig
5 changed files
--- a/testdata/FalsePositiveExamples/nested/SDG/Nested.pdg
+++ b/testdata/FalsePositiveExamples/nested/SDG/Nested.pdg
@@ -14,7 +14,7 @@ HE 5;
 HE 6;
 HE 9;
 HE 15;
-HE 118;
+HE 119;
 PS 3;
 PS 4;
 CF 4;
@@ -25,7 +25,7 @@ CD 15;
 CE 2;
 CE 3;
 CE 4;
-CE 118;
+CE 119;
 }
 EXIT 2 {
 O exit;
@@ -44,7 +44,7 @@ T "Ljava/lang/Exception";
 P 4;
 S "Nested.java":0,0-0,0;
 B "<exception>":-2;
-CF 118: "exc";
+CF 119: "exc";
 PO 36;
 }
 FRMI 4 {
@@ -56,7 +56,7 @@ S "Nested.java":0,0-0,0;
 B "<param> 1":-2;
 Z 0;
 LD ["null"];
-PS 118;
+PS 119;
 CF 5;
 }
 NORM 5 {
@@ -81,13 +81,13 @@ B "Nested.main([Ljava/lang/String;)V":4;
 Z 0;
 HE 7;
 HE 8;
-HE 119;
+HE 120;
 PS 7;
 PS 8;
 CF 128;
 CE 7;
 CE 8;
-CE 119;
+CE 120;
 CE 128;
 CL 37: "virtual";
 }
@@ -99,11 +99,11 @@ P 4;
 S "Nested.java":5,0-5,0;
 B "<param> 0":-2;
 Z 0;
-PS 119;
+PS 120;
 CF 6;
 CD 6;
 SU 8;
-SU 119;
+SU 120;
 PI 40;
 }
 ACTO 8 {
@@ -212,7 +212,7 @@ P 4;
 S "Nested.java":6,0-6,0;
 B "Nested.main([Ljava/lang/String;)V":13;
 Z 0;
-CF 118;
+CF 119;
 }
 ENTR 20 {
 O entry;
@@ -261,13 +261,13 @@ Z 0;
 U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
 HE 24;
 HE 25;
-HE 120;
+HE 116;
 HE 125;
 PS 24;
 CF 125;
 CD 25;
 CE 24;
-CE 120;
+CE 116;
 CE 125;
 }
 ACTO 24 {
@@ -381,7 +381,7 @@ U "java.lang.Object.<init>()V";
 HE 32;
 HE 33;
 HE 34;
-HE 121;
+HE 117;
 HE 123;
 HE 126;
 PS 32;
@@ -390,7 +390,7 @@ CF 126;
 CD 34;
 CE 32;
 CE 33;
-CE 121;
+CE 117;
 CE 123;
 CE 126;
 }
@@ -402,7 +402,7 @@ P 5;
 S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
 B "<param> 0":-2;
 Z 0;
-PS 121;
+PS 117;
 CF 31;
 CD 31;
 DD 126;
@@ -429,13 +429,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
 Z 0;
 HE 35;
 HE 36;
-HE 122;
+HE 118;
 PS 35;
 PS 36;
 CF 130;
 CE 35;
 CE 36;
-CE 122;
+CE 118;
 CE 130;
 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 122;
+PS 118;
 CF 34;
 PI 4;
 }
@@ -475,7 +475,7 @@ HE 38;
 HE 39;
 HE 40;
 HE 41;
-HE 116;
+HE 121;
 PS 39;
 PS 40;
 CF 40;
@@ -483,7 +483,7 @@ CD 41;
 CE 38;
 CE 39;
 CE 40;
-CE 116;
+CE 121;
 }
 EXIT 38 {
 O exit;
@@ -503,7 +503,7 @@ P 6;
 S "Nested.java":0,0-0,0;
 B "<exception>":-2;
 Z 0;
-CF 116: "exc";
+CF 121: "exc";
 PO 8;
 }
 FRMI 40 {
@@ -515,7 +515,7 @@ S "Nested.java":0,0-0,0;
 B "<param> 0":-2;
 Z 0;
 LD ["null"];
-PS 116;
+PS 121;
 CF 42;
 DD 42;
 }
@@ -531,7 +531,7 @@ U "java.lang.Object.<init>()V";
 HE 42;
 HE 43;
 HE 44;
-HE 117;
+HE 122;
 HE 124;
 HE 127;
 PS 42;
@@ -540,7 +540,7 @@ CF 127;
 CD 44;
 CE 42;
 CE 43;
-CE 117;
+CE 122;
 CE 124;
 CE 127;
 }
@@ -552,7 +552,7 @@ P 6;
 S "Nested.java":1,0-1,0;
 B "<param> 0":-2;
 Z 0;
-PS 117;
+PS 122;
 CF 41;
 CD 41;
 DD 127;
@@ -577,7 +577,7 @@ P 6;
 S "Nested.java":1,0-1,0;
 B "Nested.<init>()V":4;
 Z 0;
-CF 116;
+CF 121;
 }
 ENTR 46 {
 O entry;
@@ -1251,85 +1251,85 @@ Z 0;
 CF 105;
 DD 105;
 }
-FRMO 116 {
-O form-out;
+ACTO 116 {
+O act-out;
 V "[M] |0|UNIQ(code)";
 T "I";
-P 6;
-S "Nested.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 38;
-PO 119;
+CF 24: "exc";
+CF 25;
 }
 ACTO 117 {
 O act-out;
 V "[M] |0|UNIQ(code)";
 T "I";
-P 6;
-S "Nested.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 124;
-DH 116;
+CF 33: "exc";
+CF 35;
+DD 123;
 }
-FRMO 118 {
-O form-out;
+ACTO 118 {
+O act-out;
 V "[M] |0|UNIQ(code)";
 T "I";
-P 4;
-S "Nested.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 122;
+CF 21;
+CF 36: "exc";
 }
-ACTO 119 {
-O act-out;
+FRMO 119 {
+O form-out;
 V "[M] |0|UNIQ(code)";
 T "I";
 P 4;
-S "Nested.java":5,0-5,0;
+S "Nested.java":0,0-0,0;
 B "Ljava/lang/Object.code":-4;
 Z 0;
-CF 8;
-DH 118;
+CF 2;
+PO 118;
 }
 ACTO 120 {
 O act-out;
 V "[M] |0|UNIQ(code)";
 T "I";
-P 5;
-S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
+P 4;
+S "Nested.java":5,0-5,0;
 B "Ljava/lang/Object.code":-4;
 Z 0;
-CF 24: "exc";
-CF 25;
+CF 8;
+DH 119;
 }
-ACTO 121 {
-O act-out;
+FRMO 121 {
+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 "Nested.java":0,0-0,0;
 B "Ljava/lang/Object.code":-4;
 Z 0;
-CF 33: "exc";
-CF 35;
-DD 123;
+CF 38;
+PO 120;
 }
 ACTO 122 {
 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 "Nested.java":1,0-1,0;
 B "Ljava/lang/Object.code":-4;
 Z 0;
-CF 21;
-CF 36: "exc";
+CF 43: "exc";
+CF 44;
+DD 124;
+DH 121;
 }
 NORM 123 {
 O compound;
@@ -1338,7 +1338,7 @@ P 5;
 S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
 B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
 Z 0;
-CF 121;
+CF 117;
 DD 25;
 }
 NORM 124 {
@@ -1348,7 +1348,7 @@ P 6;
 S "Nested.java":0,0-0,0;
 B "Nested.<init>()V":-1;
 Z 0;
-CF 117;
+CF 122;
 DD 40;
 }
 NORM 125 {
@@ -1358,9 +1358,9 @@ P 5;
 S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
 B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
 Z 0;
-CF 120;
+CF 116;
 DD 24;
-DD 120;
+DD 116;
 }
 NORM 126 {
 O compound;
@@ -1371,7 +1371,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
 Z 0;
 CF 123;
 DD 33;
-DD 121;
+DD 117;
 }
 NORM 127 {
 O compound;
@@ -1382,7 +1382,7 @@ B "Nested.<init>()V":-1;
 Z 0;
 CF 124;
 DD 43;
-DD 117;
+DD 122;
 }
 NORM 128 {
 O compound;
@@ -1391,7 +1391,7 @@ P 4;
 S "Nested.java":5,0-5,0;
 B "Nested.main([Ljava/lang/String;)V":-9;
 Z 0;
-CF 119;
+CF 120;
 }
 NORM 129 {
 O compound;
@@ -1409,7 +1409,7 @@ P 5;
 S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
 B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
 Z 0;
-CF 122;
+CF 118;
 }
 NORM 131 {
 O compound;

--- a/testdata/FalsePositiveExamples/nested/nestedNew.joak
+++ b/testdata/FalsePositiveExamples/nested/nestedNew.joak
+directoryPath : "/home/joachim/git/KeYJoana/keyjoana/testdata/FalsePositiveExamples/nested",
+pathKeY : "dependencies/Key/KeY.jar",
+javaClass : "",
+pathToJar : "testdata/build/src.jar",
+pathToJavaFile : "src/",
+pathToSDG : "SDG/Nested.pdg",
+entryMethod : "Nested",
+annotationPath : "",
+fullyAutomatic : true,
+pathToSaver : "SDG/Nested.dispro",
+sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int Nested.testMethod(int, int)"}}],
+sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int Nested.testMethod(int, int)"}}]
\ No newline at end of file
--- a/testdata/FalsePositiveExamples/nested/slices/sliceSource50Sink47/src/Nested.java
+++ b/testdata/FalsePositiveExamples/nested/slices/sliceSource50Sink47/src/Nested.java
 public class Nested 
 {
-   public static void main ( String [ ] args ) 
-   {
-      new Nested ( ) . testMethod ( 1 , 2 ) ;
-   }
-   public int testMethod ( int high , int low ) 
-   {
-      int l = nested ( high , low ) ;
-      return l ;
-   }
-   public int nested ( int high , int low ) 
-   {
-      low = plusMinus ( low , high ) ;
-      return low ;
-   }
-   private int plusMinus ( int low , int high ) 
-   {
-      low = low + high ;
-      low = minus ( low , high ) ;
-      return low ;
-   }
-   private int minus ( int low , int high ) 
-   {
-      low = low - high ;
-      return low ;
-   }
+    public static void main ( String [ ] args ) 
+    {
+        new Nested ( ) . testMethod ( 1 , 2 ) ;
+    }
+    public int testMethod ( int high , int low ) 
+    {
+        int l = nested ( high , low ) ;
+        return l ;
+    }
+    public int nested ( int high , int low ) 
+    {
+        low = plusMinus ( low , high ) ;
+        return low ;
+    }
+    private int plusMinus ( int low , int high ) 
+    {
+        low = low + high ;
+        low = minus ( low , high ) ;
+        return low ;
+    }
+    private int minus ( int low , int high ) 
+    {
+        low = low - high ;
+        return low ;
+    }
 	/*@
 	@ requires true;
 	@ ensures b;

--- a/testdata/FalsePositiveExamples/nested/src/Nested.java
+++ b/testdata/FalsePositiveExamples/nested/src/Nested.java
 public class Nested 
 {
-   public static void main ( String [ ] args ) 
-   {
-      new Nested ( ) . testMethod ( 1 , 2 ) ;
-   }
-   public int testMethod ( int high , int low ) 
-   {
-      int l = nested ( high , low ) ;
-      return l ;
-   }
-   public int nested ( int high , int low ) 
-   {
-      low = plusMinus ( low , high ) ;
-      return low ;
-   }
-   private int plusMinus ( int low , int high ) 
-   {
-      low = low + high ;
-      low = minus ( low , high ) ;
-      return low ;
-   }
-   private int minus ( int low , int high ) 
-   {
-      low = low - high ;
-      return low ;
-   }
+    public static void main ( String [ ] args ) 
+    {
+        new Nested ( ) . testMethod ( 1 , 2 ) ;
+    }
+    public int testMethod ( int high , int low ) 
+    {
+        int l = nested ( high , low ) ;
+        return l ;
+    }
+    public int nested ( int high , int low ) 
+    {
+        low = plusMinus ( low , high ) ;
+        return low ;
+    }
+    private int plusMinus ( int low , int high ) 
+    {
+        low = low + high ;
+        low = minus ( low , high ) ;
+        return low ;
+    }
+    private int minus ( int low , int high ) 
+    {
+        low = low - high ;
+        return low ;
+    }
 }
--- a/testdata/FalsePositiveExamples/nested/testdata/build/src.jar
+++ b/testdata/FalsePositiveExamples/nested/testdata/build/src.jar