Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

4 files changed, 58 insertions, 20 deletions

diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy
index be092261..666d9575 100644
--- a/Test/dafny4/Regression0.dfy
+++ b/Test/dafny4/Regression0.dfy
@@ -4,10 +4,10 @@
 // This once crashed Dafny

 

 method M() {

-  var s := [1, "2"];

+  var s := [1, "2"];  // error: all elements must have the same type

   if * {

-    assert exists n :: n in s && n != 1;

+    assert exists n :: n in s && n != 1;  // the type of n is inferred to be int

   } else {

-    assert "2" in s;

+    assert "2" in s;  // error: since the type of s wasn't determined

   }

 }

diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect
index 9d1e3019..566b3e3f 100644
--- a/Test/dafny4/Regression0.dfy.expect
+++ b/Test/dafny4/Regression0.dfy.expect
@@ -1,4 +1,3 @@
 Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)

-Regression0.dfy(9,28): Error: the type of this variable is underspecified

 Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)

-3 resolution/type errors detected in Regression0.dfy

+2 resolution/type errors detected in Regression0.dfy

diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy
index 71a07f3d..d093a924 100644
--- a/Test/dafny4/set-compr.dfy
+++ b/Test/dafny4/set-compr.dfy
@@ -22,7 +22,7 @@ method O() returns (ghost p: set<object>)
 

 method P() returns (p: set<object>)

 {

-  p := set o: object | true;  // not allowed -- not in a ghost context

+  p := set o: object | true;  // error: not (easily) compilable

 }

 

 ghost method Q() returns (p: set<object>)

@@ -30,26 +30,54 @@ ghost method Q() returns (p: set<object>)
   p := set o: object | true;  // allowed, since the whole method is ghost

 }

 

-function F(): int

+function F(p: object): int

+  requires p in set o: object | true  // error: function is not allowed to depend on allocation state

+  ensures p in set o: object | true  // error: ditto (although one could argue that this would be okay)

+  reads set o: object | true  // error: same as for 'requires'

+  decreases set o: object | true  // error: same as for 'ensures'

+{

+  if p in set o: object | true then  // error: function is not allowed to depend on allocation state

+    F(p)

+  else

+    0

+}

+

+function method G(p: object): int

+  requires p in set o: object | true  // error (see F)

+  ensures p in set o: object | true  // error (see F)

+  reads set o: object | true  // error (see F)

+  decreases set o: object | true  // error (see F)

+{

+  if p in set o: object | true then  // error (see F)

+    G(p)

+  else

+    0

+}

+

+method M0() returns (ghost r: int, s: int)

   requires null in set o: object | true  // allowed

   ensures null in set o: object | true  // allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // allowed

 {

-  if null in set o: object | true then  // allowed -- in a ghost context

-    F()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

 

-function method G(): int

+method M1() returns (ghost r: int, s: int)

   requires null in set o: object | true  // (X) allowed

   ensures null in set o: object | true  // (X) allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // (X) allowed

 {

-  if null in set o: object | true then  // not allowed, since this is not a ghost context

-    G()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect
index 615ee2bc..b0490a11 100644
--- a/Test/dafny4/set-compr.dfy.expect
+++ b/Test/dafny4/set-compr.dfy.expect
@@ -1,3 +1,14 @@
 set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-2 resolution/type errors detected in set-compr.dfy

+set-compr.dfy(34,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(35,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(36,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(37,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(39,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(46,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(47,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(48,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(49,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(51,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(65,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+set-compr.dfy(79,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+13 resolution/type errors detected in set-compr.dfy