fix: For attributes, add missing resolution and fix pointless parsing

[RustanLeino]

• fix: Resolve attributes on requires and ensures clauses for functions (previously, these were never resolved)
• fix: Resolve attributes on all specification components of iterators (previously, these were never resolved)
• fix: Previously, attributes on reads clauses were parsed and then ignored. Now, they are not parsed at all. (There is no place in the AST where these are stored.)
• fix: Previously, attributes on requires clauses of lambda expressions were parsed and then ignored. Now, they are not parsed at all. (There is no place in the AST where these are stored.)
• fix: Previously, attributes on decreases clauses of functions were parsed and then ignored. Now, they are parsed and stored in the AST. (These had a place in the AST, but were previously not stored there--or anywhere.)
• Add test cases that make sure attributes on modify statements and module declarations are resolved

Note for reviewers: Review of AttributeChecks.dfy and AttributeChecks.dfy.expect are probably best done commit by commit. The first commit just adds white space to the test file, and the second commit wraps a module declaration around the contents of the file.

[cpitclaudel]

Are there any call left to ResolveAttributes that are not of the form ResolveAttributes(X, X.attributes)? If not then maybe it's worth changing the signature of that function to take one fewer parameter

[RustanLeino]

Are there any call left to ResolveAttributes that are not of the form ResolveAttributes(X, X.attributes)? If not then maybe it's worth changing the signature of that function to take one fewer parameter

@cpitclaudel Good call! This simplified all 39 call sites.