Patches item #2013882, was opened at 2008-07-08 16:14
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=510631&aid=2013882&group_id=65346Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: None
Group: JML4
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: Daniel M. Zimmerman (dmzimmerman)
Assigned to: Nobody/Anonymous (nobody)
Summary: JML4 Quantifiers Bugfix Patch
Initial Comment:
This patch fixes two issues with quantifier parsing and resolving: 1) the "degenerate" form (\forall int a; ; a < 0); - that is, the quantifier with an empty range with semicolon (as opposed to an omitted range and correspondingly omitted semicolon) - did not parse properly, resulting in odd errors; and 2) a null pointer exception was generated under certain circumstances when resolution of variables outside the quantifier's own scope failed.
In addition to very minor grammar changes and changes to the JmlQuantifiedExpression class, two unit tests were added to test for these issues.
-Dan Zimmerman, UW Tacoma, 2008-07-08
----------------------------------------------------------------------
You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=510631&aid=2013882&group_id=65346-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at
http://www.sourceforge.net/community/cca08_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers
