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 | 1512286c445a2aa63649e1501c38690c499e8113 (patch) | |
| tree | 0de5ecfe8a98bed9ebbba95dff613507abf8ba77 /Test/dafny0/ParallelResolveErrors.dfy | |
| parent | 8bf9d3f838df8e8e42f496d9de5468e2946bd5e4 (diff) | |
Dafny: fixed lack of assign-such-that restriction in parallel statement
Diffstat (limited to 'Test/dafny0/ParallelResolveErrors.dfy')
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 7 |
1 files changed, 7 insertions, 0 deletions
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
+ }
+}
|