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/Answer | |
| parent | 8bf9d3f838df8e8e42f496d9de5468e2946bd5e4 (diff) | |
Dafny: fixed lack of assign-such-that restriction in parallel statement
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 4 |
1 files changed, 3 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.
|