This is the first intruction of @-attributes in Dafny.
In this PR @-attributes are parsed only for top-level declarations and member declarations
Old-style attributes are still supported
An early resolution rewriting phase takes care of converting these new attributes whose name is "@" and have one argument, to regular attributes
Boogie does not receives these user-supplied @- attributes for now
@-attributes are resolved as if they were datatypes
For attributes used during parsing (i.e. options), I changed the code to also detect @-attributes
Formatting of @-attributes
Future features in development not included in this PR
User-defined @-attributes
@-attributes on clauses, statements, expressions
Language server auto-complete of @-attributes
How has this been tested?
Existing CI tests ensure we did not loose existing attributes
One test to pass when @-attributes are correctly supplied
Two failure tests to verify that @-attributes have correct resolution errors and don't parse @-calls
The Compile(false) on the new version of some DafnyCore/**/.dfy files is tested by the fact that the generated code still does not contain the modules annotated that way.
Pretty-printing checked by all checked Dafny source files in DafnyCore and DafnyStandardLibraries
Note that I could not reach in this PR a failing test to trigger the "Attribute not expected here" error, because Coco interprets an @-attribute as the start of a TopLevelDecl for now. In an upcoming PR, non-empty @-attributes will be returned by TopDecl so this error message will be tested.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Related to #5795
Description
This is the first intruction of @-attributes in Dafny.
Future features in development not included in this PR
How has this been tested?
Compile(false)on the new version of someDafnyCore/**/.dfyfiles is tested by the fact that the generated code still does not contain the modules annotated that way.Note that I could not reach in this PR a failing test to trigger the "Attribute not expected here" error, because Coco interprets an @-attribute as the start of a TopLevelDecl for now. In an upcoming PR, non-empty @-attributes will be returned by TopDecl so this error message will be tested.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.