assert m.containsKey(k), dataflow, and AssumeAssertion

[GoogleCodeExporter]

I expect the attached test case to issue no warnings.

It is committed to the repository.

Original issue reported on code.google.com by michael.ernst@gmail.com on 10 Apr 2015 at 6:24

Attachments:

• Issue427.java

[GoogleCodeExporter]

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

[GoogleCodeExporter]

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

• Changed state: Invalid

[GoogleCodeExporter]

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

[GoogleCodeExporter]

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

[GoogleCodeExporter]

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

[GoogleCodeExporter]

Either way is OK with me.

Original comment by michael.ernst@gmail.com on 11 Apr 2015 at 12:25