viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 40 forks source link

Parser changes for documentation generator #780

Open fnussbaum opened 5 months ago

fnussbaum commented 5 months ago

This PR introduces changes to the parser for the documentation generator in development: Comments starting with exactly three slashes are parsed as annotations with the key "doc". Moreover, annotations can now be put before specification keywords. Such annotations are put into a new annotations-field in the PSpecification-nodes in the parse AST. During translation into the Viper AST, specification annotations are pushed into the corresponding expression, as there are no specification nodes in the AST.