diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 17:30:42 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 17:30:42 -0700 |
| commit | 46b31d5f040c6849bf9053a97e1c9f2041070cea (patch) | |
| tree | a53f937a12f2998de5e7e07575e0c79d9707ea40 /Test/dafny0 | |
| parent | a4b9ca4e83da80a7e0b994196272cf28c9cd370e (diff) | |
Dafny: fixed lack of assign-such-that restriction in parallel statement
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 7 |
2 files changed, 10 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 22c24816..589a43e2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1078,7 +1078,9 @@ ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
-14 resolution/type errors detected in ParallelResolveErrors.dfy
+ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
+15 resolution/type errors detected in ParallelResolveErrors.dfy
-------------------- Parallel.dfy --------------------
Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 98f1ae3a..ab711d02 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -99,3 +99,10 @@ method M1() { }
}
}
+
+method M2() {
+ var a := new int[100];
+ parallel (x | 0 <= x < 100) {
+ a[x] :| a[x] > 0; // error: not allowed to update heap location in a parallel statement with a(n implicit) assume
+ }
+}
|