diff options
| author |  leino <unknown> | 2014-10-30 15:12:31 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-30 15:12:31 -0700 |
| commit | 9f41b35b514eba87a037cbada83f0c294eafb936 (patch) | |
| tree | 06b875a433e0ca8ca80dc41cc7ed34bbef5514b8 /Test/dafny0/LhsDuplicates.dfy.expect | |
| parent | c612305e78f057b9d1e91a0d154989cb866a7906 (diff) | |
Allow assignment LHSs in a forall statement to be the same, so long as the they are assigned the same RHS value.
Don't include havoc assignments in LHS-duplicate checks.
Diffstat (limited to 'Test/dafny0/LhsDuplicates.dfy.expect')
| -rw-r--r-- | Test/dafny0/LhsDuplicates.dfy.expect | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Test/dafny0/LhsDuplicates.dfy.expect b/Test/dafny0/LhsDuplicates.dfy.expect new file mode 100644 index 00000000..a864390f --- /dev/null +++ b/Test/dafny0/LhsDuplicates.dfy.expect @@ -0,0 +1,28 @@ +LhsDuplicates.dfy(18,10): Error: left-hand sides for different forall-statement bound variables may refer to the same location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon16_Else
+ (0,0): anon18_Else
+ (0,0): anon21_Then
+ (0,0): anon13
+LhsDuplicates.dfy(34,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon16_Else
+ (0,0): anon18_Else
+ (0,0): anon21_Then
+ (0,0): anon13
+LhsDuplicates.dfy(42,12): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value
+Execution trace:
+ (0,0): anon0
+LhsDuplicates.dfy(51,18): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value
+Execution trace:
+ (0,0): anon0
+LhsDuplicates.dfy(60,16): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value
+Execution trace:
+ (0,0): anon0
+LhsDuplicates.dfy(69,20): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 6 verified, 6 errors
|