diff options
| author |  wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
| commit | 607ef28aadb281ab61a2be493a637126e967a388 (patch) | |
| tree | aae16c049c860e443920f9c6ee31af4e35f8a800 /Test/dafny0/RefinementErrors.dfy.expect | |
| parent | dc0a9130355352d0f47e07232d8119fc7219ccbc (diff) | |
Set up the same test infrastructure as in Boogie.
Diffstat (limited to 'Test/dafny0/RefinementErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/RefinementErrors.dfy.expect | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Test/dafny0/RefinementErrors.dfy.expect b/Test/dafny0/RefinementErrors.dfy.expect new file mode 100644 index 00000000..12183e32 --- /dev/null +++ b/Test/dafny0/RefinementErrors.dfy.expect @@ -0,0 +1,12 @@ +RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions
+RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause
+RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate
+RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field
+RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
+RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')
+RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')
+RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')
+RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
+RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
+RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
+11 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\RefinementErrors.dfy
|