Closed GoogleCodeExporter closed 9 years ago
This example fails because the "AssumeAssertion" should be "@AssumeAssertion".
The example passes when I put the @ sign in front. I will close this issue.
Original comment by jbu...@cs.washington.edu
on 10 Apr 2015 at 11:20
I should note, it is a little weird to write into a string something that looks
like an annotation.
Original comment by Jonathan...@gmail.com
on 10 Apr 2015 at 11:22
My bad! Thanks for clearing that up.
The theory about why the string contains the at-sign is:
* less likely to accidentally happen to be in the string
* looks more like other warning suppressions that are annotations.
Original comment by michael.ernst@gmail.com
on 10 Apr 2015 at 11:38
We might want to consider issuing a warning if the user forgets the at-sign.
That would be a low-priority enhancement, though.
Original comment by michael.ernst@gmail.com
on 10 Apr 2015 at 11:40
That makes sense. Should I remove the issue from the test suite?
Alternatively we could re-open this as low priority and change that test to
expect the warning you just mentioned and skip it for now.
Original comment by jbu...@cs.washington.edu
on 10 Apr 2015 at 11:55
Either way is OK with me.
Original comment by michael.ernst@gmail.com
on 11 Apr 2015 at 12:25
Original issue reported on code.google.com by
michael.ernst@gmail.com
on 10 Apr 2015 at 6:24Attachments: