Bug fix: check that assign-such-that constraint is of type boolean

2 files changed, 20 insertions, 1 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 900c7459..1354e533 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1373,3 +1373,18 @@ module NonTypeVariableNames {
     Y := k;  // error: module name used as variable

   }

 }

+

+// ------------------- assign-such-that and let-such-that -------------------

+

+module SuchThat {

+  method M() {

+    var x: int;

+    x :| 5 + 7;  // error: constraint should be boolean

+    x :| x;  // error: constraint should be boolean

+    var y :| 4;  // error: constraint should be boolean

+  }

+  function F(): int {

+    var w :| 6 + 8;  // error: constraint should be boolean

+    w

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 481b47e0..b5c93ac1 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -104,6 +104,10 @@ ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable
 ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)

 ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable

 ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable

+ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int)

+ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int)

 ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

@@ -196,4 +200,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-198 resolution/type errors detected in ResolutionErrors.dfy

+202 resolution/type errors detected in ResolutionErrors.dfy