Allow calls to side-effect-free ghost methods from expressions

3 files changed, 57 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 9570a0ba..5b341f1f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -381,6 +381,9 @@ ResolutionErrors.dfy(730,16): Error: a hint is not allowed to update heap locati
 ResolutionErrors.dfy(731,21): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(732,8): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(735,19): Error: a while statement used inside a hint is not allowed to have a modifies clause

+ResolutionErrors.dfy(760,4): Error: calls to methods with side-effects are not allowed inside a statement expression

+ResolutionErrors.dfy(761,4): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(762,4): Error: wrong number of method result arguments (got 0, expected 1)

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

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

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -454,7 +457,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses

-107 resolution/type errors detected in ResolutionErrors.dfy

+110 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1187,8 +1190,16 @@ Execution trace:
     (0,0): anon0

     (0,0): anon6_Then

     StatementExpressions.dfy(50,7): anon8_Else

+StatementExpressions.dfy(74,6): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+StatementExpressions.dfy(85,5): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

 

-Dafny program verifier finished with 9 verified, 2 errors

+Dafny program verifier finished with 13 verified, 4 errors

 

 -------------------- Coinductive.dfy --------------------

 Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index b96b0867..926f08ae 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -747,4 +747,19 @@ module StatementsInExpressions {
     }

     5;

   }

+

+  ghost method MyLemma()

+  ghost method MyGhostMethod()

+    modifies this;

+  method OrdinaryMethod()

+  ghost method OutParamMethod() returns (y: int)

+

+  function UseLemma(): int

+  {

+    MyLemma();

+    MyGhostMethod();   // error: modifies state

+    OrdinaryMethod();  // error: not a ghost

+    OutParamMethod();  // error: has out-parameters

+    10

+  }

 }

diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy
index 9f33b282..386d030b 100644
--- a/Test/dafny0/StatementExpressions.dfy
+++ b/Test/dafny0/StatementExpressions.dfy
@@ -56,3 +56,32 @@ ghost method Q(n: nat)
     assert y == 102;  // error: assertion does not hold

   }

 }

+

+// ---------------------

+

+function Fact(n: nat): nat

+{

+  if n == 0 then 1 else n * Fact(n-1)

+}

+

+lemma L(n: nat)

+  ensures 1 <= Fact(n);

+{

+}

+

+function F_Fails(n: nat): int

+{

+  50 / Fact(n)  // error: possible division by zero

+}

+

+function F_Succeeds(n: nat): int

+{

+  L(n);

+  50 / Fact(n)

+}

+

+function F_PreconditionViolation(n: int): int

+{

+  L(n);  // error: argument might be negative

+  50 / Fact(n)

+}