Skip to content

Conversation

@umutdural
Copy link
Collaborator

This PR fixes the following issues by resolving annotations to only intrinsic annotation declarations, skipping the current scope. Hence other declaration kinds can't shadow annotation declarations anymore.

@Philipp15b
Copy link
Collaborator

In addition to the fix of handling the missing annotation declaration, this PR changes resolution to be a bit smarter and consider the "kind" of declaration during search, instead of just taking the first one it finds. I guess that's the way to go? Alternatively, one could just report an error of a kind mismatch, no?

}

/// Get all annotation declarations that can be used on top of statements. These are slicing and encoding annotations.
pub fn get_statement_annotations(&self) -> IndexMap<Symbol, Rc<DeclKind>> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand why you want to create this new IndexMap instead of just creating a version of get for annotations specifically? Seems wasteful.


match self.tcx.get(*ident).as_deref() {
None => {} // Declaration not found
// Resolve the annotation ident to the declaration
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment formatting and dots at end of sentences

@Philipp15b
Copy link
Collaborator

Philipp15b commented Dec 19, 2025

Clippy failure was unrelated and is fixed on main now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Undeclared functions in invariants Error when using the name "invariant" in an invariant Calculus Annotation - Procedures with name k_induction

2 participants