Skip to content

Take advantage of clang-3.9 new nonnull attribute #1370

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented Sep 11, 2017

Builds had started failing on Travis due to an upgrade to clang-3.9:

https://travis-ci.org/diffblue/cbmc/jobs/274155578#L799

Spotted by @smowton

@reuk
Copy link
Contributor

reuk commented Sep 11, 2017

LGTM but IMO the .travis.yml should also be updated to use clang-3.9 explicitly

@kroening
Copy link
Member

Already done by #1364.

@smowton
Copy link
Contributor

smowton commented Sep 11, 2017

@kroening compare #1369, which ignores the warning as not applicable to a library solely for CBMC's internal consumption.

It's a shame to remove if(s1!=0 && s1==s2) just because GCC/Clang would optimise that check away. Clearly CBMC would never do so, since null accesses and other undefined behaviour are always interesting to its bug-checking mission.

@smowton
Copy link
Contributor

smowton commented Sep 11, 2017

This version on the other hand is wrong I think, since it will silently accept strcmp(nullptr, nullptr), which should yield a fault report from CBMC.

@thk123
Copy link
Contributor Author

thk123 commented Sep 11, 2017

As pointed out, this is addressed (better) in other PRs.

@thk123 thk123 closed this Sep 11, 2017
@kroening
Copy link
Member

@smowton The idea is the following: the optimisation can be put back in once we add a precondition that says that the parameters must point to zero-terminated strings.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants