[Checkers] QReadOnly Insertion

Mahmood Ali mahmood at MIT.EDU
Thu Aug 21 03:31:45 EDT 2008

Hi Telmo,

> I think there were issues with errors being generated when the type  
> variable did not had the annotation @QReadOnly implicitly added to  
> it, on the past, which pointed that those annotations were honored.  
> Or so it was on a previous revision. Though this "honoring" occurs  
> on the JavariChecker, not on the framework, if I am not mistaken.

So those cases were actually bugs in the framework.  QReadOnly  
surpress those errors, as Javari's TypeHierarchy always pass the  
subtyping test if the type has QReadOnly.

I corrected the framework and commented out the Javari code of  
inserting QReadOnly.  Please test it further and report to me any  
errors you find.


More information about the checkers mailing list