UIEffect: is @UIType inherited?

[Jo D]

Hi all,

I couldn't find an authoritative answer to this question, only hints that this is not the case but I am not experienced enough with CheckerFramework to be 100% sure.

BTW is there a way to validate assumptions about this kind of stuff?

E.g. a file where Checker Framework outputs all inferred annotations.

Regards,

Jo

[Colin Stebbins Gordon]

Hi Jo,

@UIType is not inherited by normal class declarations, but is inherited by anonymous inner classes.

Currently there's no single place to look for this kind of information, which comes from a combination of some shared machinery, and custom logic in each checker. Neither currently emits a summary of it's decisions, though this is certainly worth considering.  

Probably the best short-term solutions for getting this sort of policy information are experimenting with small examples. Short-to-medium term, this is information that I should add to the documentation for that checker.

*Some* inferred annotations are persisted in the compiled .class files, where they could in principle be extracted by tools like the Annotation File Utilities (https://checkerframework.org/annotation-file-utilities/). It would include annotations explicitly registered by the checkers, but not those inferred in passing, which is how the GUI Effect checker handles the consequences of @UIType. For example, the GUIType Checker would not emit a @UIEffect annotation on every method of a @UIType in the class file; it doesn't need to for its own correctness, since compiling against a library with an @UIType would replay the same logic as if the @UIType were in the same compilation unit.  The GUI Effect checker is perhaps worse in this regard than most other checkers, since it's a different style of checker and therefore has more logic that cannot be shared across checkers, but this is a good reason to reevaluate how much of that information we can at least persist into class files, if not through other means.

-Colin

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/f8b880dc-7559-4b57-b5db-71e95649154cn%40googlegroups.com.

[Durchholz, Joachim]

Thanks for the information!

 

Good thing you mentioned anonymous inners, that would have been my next question.

 

About longer-term plans, let me state my personal preferences as a data point:

• I’d prefer output in text form, I’m already struggling with too many utilities.
• A text format that’s both human-readable and parseable would be ideal.
• I’d want the output in a single file, so it’s easier to find the interesting information in one place.
• The other useful output format would be Java sources with effective annotations added. These would be useful as alternative source files for use in the IDE. (Big point that I don’t know a good solution for: How to make sure that the generated output and the real library sources stay in sync.)

 

Regards,

Jo

Sensitivity: C2 Internal

The content of this e-mail is intended only for the confidential use of the person addressed.
If you are not the intended recipient, please notify the sender and delete this e-mail immediately.
Thank you.

[Jo D]

Ah, I forgot the most important thing: I need a list how the JDK files are annotated.

(I just noticed that I don't see a jdk11.astub anywhere - so how does UIEffect checker even know what JDK members are @UIEffect?)