diff options
| author |  leino <unknown> | 2015-04-03 21:44:11 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-03 21:44:11 -0700 |
| commit | 9c8ad44b64373fb9d85aef5a05809e8e25416684 (patch) | |
| tree | b1e03bd6ac48c26e659bebe1e56180d34b8fcc8a /Test/dafny0/Trait/TraitsDecreases.dfy.expect | |
| parent | 8a332057c2c9fc76e5fb112d430404d1aa47ea0d (diff) | |
Added test cases and fixes for overrides termination checks
Removed syntactic presence checks for specifications--these will be checked semantically by the verifier
Diffstat (limited to 'Test/dafny0/Trait/TraitsDecreases.dfy.expect')
| -rw-r--r-- | Test/dafny0/Trait/TraitsDecreases.dfy.expect | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect new file mode 100644 index 00000000..6c76f9a8 --- /dev/null +++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect @@ -0,0 +1,17 @@ +TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 63 verified, 5 errors
|