From 46b31d5f040c6849bf9053a97e1c9f2041070cea Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 15 Mar 2012 17:30:42 -0700 Subject: Dafny: fixed lack of assign-such-that restriction in parallel statement --- Test/dafny0/Answer | 4 +++- Test/dafny0/ParallelResolveErrors.dfy | 7 +++++++ 2 files changed, 10 insertions(+), 1 deletion(-) (limited to 'Test/dafny0') 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 + } +} -- cgit v1.2.3