Fix check error

federicomarra · federicomarra · commit 738cdf9f1e64 · 2024-12-02T14:55:30.000+01:00
diff --git a/tests/abstract-function-bad.slang b/tests/abstract-function-bad.slang
@@ -1,8 +1,8 @@
-function square(n: Int) : Int
-    ensures result == n * n
-
-method c() {
-    var y: Int := 4;
-    // @CheckError
-    assert 15 == square(y)
+function square(n: Int) : Int
+    ensures result == n * n
+
+method c() {
+    var y: Int := 4;
+    //@CheckError
+    assert 15 == square(y)
 }
diff --git a/tests/assert-assign-bad.slang b/tests/assert-assign-bad.slang
@@ -1,5 +1,5 @@
 method client() {
     var x: Int := 2 ;
-    // @CheckError
+    //@CheckError
     assert x == 3
 }
diff --git a/tests/assert-false.slang b/tests/assert-false.slang
@@ -1,4 +1,4 @@
 method client() {
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/assert-sum-bad.slang b/tests/assert-sum-bad.slang
@@ -1,4 +1,4 @@
 method client() {
-    // @CheckError
+    //@CheckError
     assert 1 + 2 == 4
 }
diff --git a/tests/assert-true-false.slang b/tests/assert-true-false.slang
@@ -1,5 +1,5 @@
 method client() {
     assert true;
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/assume-true.slang b/tests/assume-true.slang
@@ -1,5 +1,5 @@
 method client() {
     assume 2 == 2;
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/break-paths-complex.slang b/tests/break-paths-complex.slang
@@ -23,13 +23,13 @@ method client(n: Int)
             assert j == -1,
         n % 2 == 1 =>
             // This fails because j is actually -2
-            // @CheckError
+            //@CheckError
             assert j == -3,
         n % 2 == 2 =>
             assert false
     };
 
     // this is reachable so should also fail
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/broke-bad.slang b/tests/broke-bad.slang
@@ -10,7 +10,7 @@ method client()
         true =>
             match {
                 i == 15 =>
-                // @CheckError
+                //@CheckError
                 break
             };
             i := i - 1
diff --git a/tests/broke-good.slang b/tests/broke-good.slang
@@ -14,6 +14,6 @@ method client()
             i := i - 1
     };
     assert i == 15;
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/continue-invariant-bad.slang b/tests/continue-invariant-bad.slang
@@ -11,7 +11,7 @@ method client(n: Int)
             match {
                 i == 6 =>
                     i := i + 1;
-                    // @CheckError
+                    //@CheckError
                     continue
             };
             i := i + 2
diff --git a/tests/continue-variant-bad.slang b/tests/continue-variant-bad.slang
@@ -10,7 +10,7 @@ method client(n: Int)
             match {
                 i == 6 =>
                     i := i + 1;
-                    // @CheckError
+                    //@CheckError
                     continue
             };
             i := i - 2
diff --git a/tests/core-feature-A-bad.slang b/tests/core-feature-A-bad.slang
@@ -8,6 +8,6 @@ method m(x: Int): Int
     var acc: Int := 0;
     acc := x / 2;
     acc := acc * 6;
-    // @CheckError
+    //@CheckError
     return acc
 }
diff --git a/tests/custom-type-bad.slang b/tests/custom-type-bad.slang
@@ -10,6 +10,6 @@ domain Pair {
 method client(x: Int, y: Int)
 {
   var xy: Pair := pair(x,y);
-  // @CheckError
+  //@CheckError
   assert fst(xy) == y
 }
diff --git a/tests/division-by-zero-double.slang b/tests/division-by-zero-double.slang
@@ -1,7 +1,7 @@
 method client() {
     var x: Int;
-    // @CheckError
+    //@CheckError
     x := x / ((2*x / x) - 1);
-    // @CheckError
+    //@CheckError
     x := x / ((x / x) - 1)
 }
diff --git a/tests/division-by-zero-single.slang b/tests/division-by-zero-single.slang
@@ -1,5 +1,5 @@
 method client() {
     var x: Int;
-    // @CheckError
+    //@CheckError
     x := x / ((x / x) - 1)
 }
diff --git a/tests/division-by-zero-tenary-bad.slang b/tests/division-by-zero-tenary-bad.slang
@@ -1,5 +1,5 @@
 method client() {
     var x : Int;
-    // @CheckError
+    //@CheckError
     x := true ? 1 / 0 : 1
 }
diff --git a/tests/dsa-bad.slang b/tests/dsa-bad.slang
@@ -12,7 +12,7 @@ method main () {
             z := z - x ;
             z := z + 4 * y,
     };
-    // @CheckError
+    //@CheckError
     assert (z < 0 && z == x - y + 2 * x) || (z >= 0 && z == x - y + 4 * y);
     assert (z < 0 && z == x - y + y + 2 * x) || (z >= 0 && z == x - y - x + 4 * y)
 }
diff --git a/tests/early-return-bad.slang b/tests/early-return-bad.slang
@@ -4,7 +4,7 @@ method M(n: Int) : Int
 {
   match {
     n == 1 =>
-        // @CheckError
+        //@CheckError
         return 9
   };
   return 3
diff --git a/tests/error-masking.slang b/tests/error-masking.slang
@@ -1,12 +1,12 @@
 method client() {
     var x: Int;
-    // @CheckError
+    //@CheckError
     assert x == 2;
     assert x > 0;
     assert x + 2 == 4;
     var y: Int;
-    // @CheckError
+    //@CheckError
     assert y > 0;
-    // @CheckError
+    //@CheckError
     assert y == 2
 }
diff --git a/tests/exercise8.3-bad.slang b/tests/exercise8.3-bad.slang
@@ -38,7 +38,7 @@ method client(n: Int, m: Int) : Int
    var i: Int := m;
    loop
         invariant i <= m
-        // @CheckError
+        //@CheckError
         invariant i >= n
         invariant sum == sumDown(i, m)
    {
diff --git a/tests/for-bounded-bad.slang b/tests/for-bounded-bad.slang
@@ -3,6 +3,6 @@ method client() {
     for i in -1..5 {
         acc := i
     };
-    // @CheckError
+    //@CheckError
     assert acc == 5
 }
diff --git a/tests/for-unbounded-bad.slang b/tests/for-unbounded-bad.slang
@@ -3,7 +3,7 @@ method client(n: Int)
 {
     var counter: Int := 0;
     for i in 0..n
-        // @CheckError 
+        //@CheckError
         invariant counter == i
     {
         counter := counter + 1;
diff --git a/tests/global-bad.slang b/tests/global-bad.slang
@@ -2,7 +2,7 @@ global counter : Int
 
 method inc()
     modifies counter
-    // @CheckError
+    //@CheckError
     ensures counter == old(counter) + 1
 {
     counter := counter + 2
diff --git a/tests/global-loop-old-bad.slang b/tests/global-loop-old-bad.slang
@@ -9,7 +9,7 @@ ensures i == old(i) + n
     assert j <= n;
     loop
         invariant j >= 0 && j <= n
-        // @CheckError
+        //@CheckError
         invariant i == old(i) + j
     {
         j < n =>
diff --git a/tests/global-modifies-unspecified-variable.slang b/tests/global-modifies-unspecified-variable.slang
@@ -7,7 +7,7 @@ method inc()
     ensures counter == old(counter) + 1
 {
     counter := counter + 1;
-    // @CheckError
+    //@CheckError
     counter2 := 0
 }
 
diff --git a/tests/global-replace-old-in-body-bad.slang b/tests/global-replace-old-in-body-bad.slang
@@ -5,6 +5,6 @@ modifies x
 
 {
     x := x + 1;
-    // @CheckError
+    //@CheckError
     assert x == old(x) + 2
 }
diff --git a/tests/global-variables-modified-by-called-mathod.slang b/tests/global-variables-modified-by-called-mathod.slang
@@ -9,6 +9,6 @@ method inc()
 
 method c()
 {
-    // @CheckError
+    //@CheckError
     inc()
 }
diff --git a/tests/havoc-bad.slang b/tests/havoc-bad.slang
@@ -1,6 +1,6 @@
 method main() {
     var x: Int;
     x := 35;
-    // @CheckError
+    //@CheckError
     var x: Int
 }
diff --git a/tests/havoc-good.slang b/tests/havoc-good.slang
@@ -3,6 +3,6 @@ method main() {
     x := 35;
     var y: Int;
     x := y;
-    // @CheckError
+    //@CheckError
     assert x == 35
 }
diff --git a/tests/lemma-bad.slang b/tests/lemma-bad.slang
@@ -1,5 +1,5 @@
 method client()
-    // @CheckError
+    //@CheckError
     ensures 1 == 2
 {
     assert true
diff --git a/tests/loop-core-bad.slang b/tests/loop-core-bad.slang
@@ -4,7 +4,7 @@ method iter(n: Int): Int
     var i: Int := 0;
     loop
         // false: when the loop terminates, i == n + 1
-        // @CheckError
+        //@CheckError
         invariant i <= n
     {
         i > n + 1 => break,
diff --git a/tests/loop-decrease-bad.slang b/tests/loop-decrease-bad.slang
@@ -10,7 +10,7 @@ method client(n: Int)
         i == 10 && n >= 20 =>
             counter := counter - 10;
             i := i + 10,
-        // @CheckError
+        //@CheckError
         i < n && i >= 0 => 
             counter := counter - 1;
             j := j + 1;
diff --git a/tests/method-call-bad-requires.slang b/tests/method-call-bad-requires.slang
@@ -10,7 +10,7 @@ method sum(n: Int) : Int
 
 method client() {
     var z: Int;
-    // @CheckError
+    //@CheckError
     z := sum(-1);
     assert z == 9
 }
diff --git a/tests/method-call-wrong-body.slang b/tests/method-call-wrong-body.slang
@@ -14,6 +14,6 @@ method Square(x: Int) : Int
     // CheckError
     ensures result == x * x
 {
-    // @CheckError
+    //@CheckError
     return 2 * x
 }
diff --git a/tests/method-call-wrong-ensures.slang b/tests/method-call-wrong-ensures.slang
@@ -9,7 +9,7 @@ method Sum(n: Int) : Int
     match {
         n == 0 => return -1,
         true =>
-            // @CheckError
+            //@CheckError
             return n + sq
     }
 }
diff --git a/tests/method-might-not-return-bad.slang b/tests/method-might-not-return-bad.slang
@@ -2,7 +2,7 @@ method client2(n: Int) : Int {
     return 4
 }
 
-// @CheckError
+//@CheckError
 method client(n: Int) : Int {
     match {
          n == 1 => return 2,
diff --git a/tests/method-variant-bad.slang b/tests/method-variant-bad.slang
@@ -9,7 +9,7 @@ method sumn(n: Int): Int
             ret := 0,
         true => 
             var res: Int;
-            // @CheckError
+            //@CheckError
             res := sumn(n + 1);
             ret := res + n
     };
diff --git a/tests/modular-arithmetic-division-by-zero.slang b/tests/modular-arithmetic-division-by-zero.slang
@@ -1,5 +1,5 @@
 method client() {
     var x: Int;
-    // @CheckError
+    //@CheckError
     x := x % x
 }
diff --git a/tests/multi-break-after-loop-knowledge.slang b/tests/multi-break-after-loop-knowledge.slang
@@ -26,6 +26,6 @@ requires x >= 15 && x <= 30
     assume y != 17 && y != 20 && y != 15;
     assert i != y;
     assert i == 17 || i == 20 || i == 15;
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/preconditions-do-not-mess-up-bad.slang b/tests/preconditions-do-not-mess-up-bad.slang
@@ -7,6 +7,6 @@ method a(n: Int)
 method b(n: Int)
     requires n < 0
 {
-    // @CheckError
+    //@CheckError
     assert false
 }
diff --git a/tests/quantifier-bad.slang b/tests/quantifier-bad.slang
@@ -1,6 +1,6 @@
 method client() {
     var x : Int;
     x := 1;
-    // @CheckError
+    //@CheckError
     assert (forall i : Int :: i + x == i)
 }
diff --git a/tests/quantifier-division-self-bad.slang b/tests/quantifier-division-self-bad.slang
@@ -1,4 +1,4 @@
 method client() {
-    // @CheckError
+    //@CheckError
     assert (forall i : Int :: i / i == 1)
 }
diff --git a/tests/quantifier-division-var-bad copy.slang b/tests/quantifier-division-var-bad copy.slang
@@ -1,6 +1,6 @@
 method client() {
     var x : Int;
     x := 0;
-    // @CheckError
+    //@CheckError
     assert (forall i : Int :: i / x == i)
 }
diff --git a/tests/redeclare.slang b/tests/redeclare.slang
diff --git a/tests/return-in-loop-bad.slang b/tests/return-in-loop-bad.slang
diff --git a/tests/scoping-bad.not-included b/tests/scoping-bad.not-included
diff --git a/tests/user-defined-function-bad.slang b/tests/user-defined-function-bad.slang

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,5 @@`
`1`	`1`	`method client() {`
`2`	`2`	`var x: Int := 2 ;`
`3`		`- // @CheckError`
	`3`	`+ //@CheckError`
`4`	`4`	`assert x == 3`
`5`	`5`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`	`1`	`method client() {`
`2`		`- // @CheckError`
	`2`	`+ //@CheckError`
`3`	`3`	`assert false`
`4`	`4`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,5 @@`
`1`	`1`	`method client() {`
`2`	`2`	`assert true;`
`3`		`- // @CheckError`
	`3`	`+ //@CheckError`
`4`	`4`	`assert false`
`5`	`5`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,5 @@`
`1`	`1`	`method client() {`
`2`	`2`	`assume 2 == 2;`
`3`		`- // @CheckError`
	`3`	`+ //@CheckError`
`4`	`4`	`assert false`
`5`	`5`	`}`
Original file line number	Diff line number	Diff line change
`@@ -14,6 +14,6 @@ method client()`
`14`	`14`	`i := i - 1`
`15`	`15`	`};`
`16`	`16`	`assert i == 15;`
`17`		`- // @CheckError`
	`17`	`+ //@CheckError`
`18`	`18`	`assert false`
`19`	`19`	`}`