Closed mario-bucev closed 9 months ago
I do not understand where transitivity is implemented. Not in the diff as far as I can tell, so it was there already but not consistently so?
Before this PR, we only checked for the annotation of the direct owner (sym.owner
), now we consider all transitive owners using sym.ownersIterator.drop(1)
(where we drop the first element because ownersIterator
returns the sym
itself as first element).
Before this PR, all annotations from the direct owner of a symbol were applied to that symbol. For instance, a
@library
object containing a functionf
would (correctly) get the@library
flag, but not any of its inner functions (which is an incorrect behavior). Furthermore, a function annotated with@opaque
(incorrectly?) propagates this annotation to its direct inner functions.This PR changes the following:
stainless.annotation.ignore
stainless.annotation.library
stainless.annotation.extern
stainless.annotation.dropVCs
stainless.annotation.pure
stainless.annotation.wrapping
stainless.annotation.keep
stainless.annotation.keepFor
stainless.annotation.cCode.drop