Remove some missed colons

KeYProject · Mar 6, 2023 · 752fc30 · 752fc30
1 parent ea741d5
commit 752fc30
Show file tree

Hide file tree

Showing 25 changed files with 301 additions and 305 deletions.
diff --git a/...c/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodSubsetPO.java b/...c/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodSubsetPO.java
@@ -25,7 +25,7 @@ public void testDoSomethingElseBranch() throws Exception {
             "doSomething",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_elsebranch.xml", null,
             new Position(24, 27), new Position(25, 33),
-            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x-=42;return x; } }");
+            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x-=42;return x; } }");
     }
 
     /**
@@ -36,25 +36,25 @@ public void testDoSomethingIfBranch() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest",
             "doSomething", "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_ifbranch.xml",
             null, new Position(20, 27), new Position(21, 31),
-            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x=x*-1; x+=2; } }");
+            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x=x*-1; x+=2; } }");
     }
 
     /**
      * Tests
-     * {@code {method-frame(source=doSomething(int, String, boolean)@MethodPartPOTest,this=self): {if (asdf<0)
+     * {@code {method-frame(source=doSomething(int, String, boolean)@MethodPartPOTest,this=self) {if (asdf<0)
      * { x=x*-1; x+=2; }else { x-=42;return x; } } }} of {@code doSomething} with precondition.
      */
     @Test
     public void testDoSomethingIf() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest",
             "doSomething", "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_if.xml", null,
             new Position(19, 17), new Position(26, 17),
-            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): {if (asdf<0) { x=x*-1; x+=2; }else  { x-=42;return x; } } }");
+            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) {if (asdf<0) { x=x*-1; x+=2; }else  { x-=42;return x; } } }");
     }
 
     /**
      * Tests
-     * {@code {method-frame(source=doSomething(int, String, boolean)@MethodPartPOTest,this=self): {int x = 0;if (asdf<0)
+     * {@code {method-frame(source=doSomething(int, String, boolean)@MethodPartPOTest,this=self) {int x = 0;if (asdf<0)
      * { x=x*-1; x+=2; }else { x-=42;return x; } x=1*asdf; } }} of {@code doSomething} with
      * precondition.
      */
@@ -64,7 +64,7 @@ public void testDoSomethingIfWithSurroundingStatements() throws Exception {
             "doSomething",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_if_surroundingStatements.xml",
             null, new Position(17, 63), new Position(27, 29),
-            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): {int x = 0;if (asdf<0) { x=x*-1; x+=2; }else  { x-=42;return x; } x=1*asdf; } }");
+            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) {int x = 0;if (asdf<0) { x=x*-1; x+=2; }else  { x-=42;return x; } x=1*asdf; } }");
     }
 
     /**
@@ -78,7 +78,7 @@ public void testDoSomethingWithReturn_Precondition() throws Exception {
             "doSomething",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_withReturn_precondition.xml",
             "x == 1 && asdf == 2 && this.field == 3", new Position(27, 19), new Position(31, 25),
-            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue;return z; } }");
+            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue;return z; } }");
     }
 
     /**
@@ -92,7 +92,7 @@ public void testDoSomethingWithReturn() throws Exception {
             "doSomething",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_withReturn.xml", null,
             new Position(27, 19), new Position(31, 25),
-            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue;return z; } }");
+            "{method-frame(result->result_doSomething, source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue;return z; } }");
     }
 
     /**
@@ -106,7 +106,7 @@ public void testDoSomethingNoReturn_Precondition() throws Exception {
             "doSomething",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_noReturn_precondition.xml",
             "x == 1 && asdf == 2 && this.field == 3", new Position(27, 19), new Position(30, 44),
-            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue; } }");
+            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue; } }");
     }
 
     /**
@@ -119,7 +119,7 @@ public void testDoSomethingNoReturn() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest",
             "doSomething", "/set/methodPartPOTest/oracle/MethodPartPOTest_doSomething_noReturn.xml",
             null, new Position(27, 19), new Position(30, 44),
-            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self): { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue; } }");
+            "{method-frame(source=doSomething(int, java.lang.String, boolean)@MethodPartPOTest,this=self) { x=1*asdf;int y = 2+MethodPartPOTest.CONSTANT+this.field;int doubleValue = doubleValue(x);int z = x+y+doubleValue; } }");
     }
 
     /**
@@ -130,7 +130,7 @@ public void testVoidMethodWithReturn_Precondition() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest", "voidMethod",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_voidMethod_withReturn_precondition.xml",
             "y == -2", new Position(11, 22), new Position(13, 31),
-            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self): {int b = 3*y;return ; } }");
+            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self) {int b = 3*y;return ; } }");
     }
 
     /**
@@ -141,7 +141,7 @@ public void testVoidMethodWithReturn() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest", "voidMethod",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_voidMethod_withReturn.xml", null,
             new Position(11, 22), new Position(13, 31),
-            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self): {int b = 3*y;return ; } }");
+            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self) {int b = 3*y;return ; } }");
     }
 
     /**
@@ -152,7 +152,7 @@ public void testVoidMethodNoReturn_Precondition() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest", "voidMethod",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_voidMethod_noReturn_precondition.xml",
             "y == 2", new Position(8, 24), new Position(9, 38),
-            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self): {int a = 2*y; } }");
+            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self) {int a = 2*y; } }");
     }
 
     /**
@@ -163,7 +163,7 @@ public void testVoidMethodNoReturn() throws Exception {
         doTest("/set/methodPartPOTest/test/MethodPartPOTest.java", "MethodPartPOTest", "voidMethod",
             "/set/methodPartPOTest/oracle/MethodPartPOTest_voidMethod_noReturn.xml", null,
             new Position(8, 24), new Position(9, 38),
-            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self): {int a = 2*y; } }");
+            "{method-frame(source=voidMethod(boolean, int)@MethodPartPOTest,this=self) {int a = 2*y; } }");
     }
 
     /**

diff --git a/...c/test/resources/testcase/set/lineBreakpointsWithLoopInvariantTest/oracle/ArrayUtil_2.xml b/...c/test/resources/testcase/set/lineBreakpointsWithLoopInvariantTest/oracle/ArrayUtil_2.xml
@@ -9,31 +9,31 @@
       -&gt; !array[j] = toSearch))&lt;&lt;SC&gt;&gt;;
 variant: javaSubInt(array.length, i)
 mod: false" pathCondition="true" pathConditionChanged="false" initiallyValid="true">
-            <branchCondition name="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+            <branchCondition name="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
-}\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i))))))))" pathCondition="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+}\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i))))))))" pathCondition="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
-}\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i))))))))" pathConditionChanged="true" branchCondition="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+}\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i))))))))" pathConditionChanged="true" branchCondition="update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
 }\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i))))))))" mergedBranchCondition="false" isBranchConditionComputed="true" additionalBranchLabel="Body Preserves Invariant">
-               <branchCondition name="not(update-application(elem-update(x)(i_0),equals(array,null)))" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+               <branchCondition name="not(update-application(elem-update(x)(i_0),equals(array,null)))" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
 }\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i)))))))),not(update-application(elem-update(x)(i_0),equals(array,null))))" pathConditionChanged="true" branchCondition="not(update-application(elem-update(x)(i_0),equals(array,null)))" mergedBranchCondition="false" isBranchConditionComputed="true">
-                  <loopCondition name="i&lt;array.length" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+                  <loopCondition name="i&lt;array.length" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
 }\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i)))))))),not(update-application(elem-update(x)(i_0),equals(array,null))))" pathConditionChanged="false" blockOpened="false">
                   </loopCondition>
                </branchCondition>
-               <branchCondition name="update-application(elem-update(x)(i_0),equals(array,null))" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+               <branchCondition name="update-application(elem-update(x)(i_0),equals(array,null))" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
 }\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i)))))))),update-application(elem-update(x)(i_0),equals(array,null)))" pathConditionChanged="true" branchCondition="update-application(elem-update(x)(i_0),equals(array,null))" mergedBranchCondition="false" isBranchConditionComputed="true">
-                  <loopCondition name="i&lt;array.length" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil): {
+                  <loopCondition name="i&lt;array.length" pathCondition="and(update-application(parallel-upd(elem-update(exc)(null),elem-update(i)(Z(0(#)))),update-application(parallel-upd(elem-update(heapBefore_LOOP)(heap),elem-update(iBefore_LOOP)(i)),update-application(elem-update(i)(i_0),update-application(elem-update(variant)(javaSubInt(length(array),i)),\[{method-frame(source=indexOf(java.lang.Object[], java.lang.Object)@ArrayUtil) {
     boolean b = i&lt;array.length;
   }
 }\] (and(equals(b,TRUE),and(and(and(geq(i,Z(0(#))),leq(i,length(array)))&lt;&lt;SC&gt;&gt;,all{j:int}(imp(and(and(geq(j,Z(0(#))),lt(j,i))&lt;&lt;SC&gt;&gt;,inInt(j)),not(equals(java.lang.Object::select(heap,array,arr(j)),toSearch)))))&lt;&lt;SC&gt;&gt;,inInt(i)))))))),update-application(elem-update(x)(i_0),equals(array,null)))" pathConditionChanged="false" blockOpened="false">