Skip to content

Warning for when bounds declarations are not provably true. #343

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

Merged
merged 1 commit into from
Jul 7, 2017

Conversation

dtarditi
Copy link
Member

@dtarditi dtarditi commented Jul 6, 2017

This adds a warning message for when bounds declarations are not provably true. The warning is off by default because we cannot prove much yet about bounds declarations. This addresses work item #338.

We test the error message by adding checking of bounds declarations after assignments. We handle a few basic cases where the declared bounds for the target variable are implied by the inferred bounds of the source expression, that is a check for subsumption of bounds. Given e1 = e2, we allow the cases where:

  • the declared bounds of e1 and inferred bounds of e2 are syntactically equal.
  • the declared bounds of e1 is bounds(none), in which case any inferred bounds works for e2.
  • the inferred bounds of e2 is bounds(any).

Testing:

  • Added two new test cases. In one case, the bounds has syntactically identical. In another case, they are not syntactically identical because of the way that 'count' expands, so we produce a warning. When we extend the bounds subsumption check to understand facts about variables being equal, the second test case should no longer produce a warning

This adds a warning message for when bounds declarations are not
provably true.  The warning is off by default because we cannot
prove much yet.
Copy link
Collaborator

@lenary lenary left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM 👍

@dtarditi dtarditi merged commit 00f49f1 into checkedc:master Jul 7, 2017
@dtarditi dtarditi deleted the issue338 branch September 21, 2017 01:04
sulekhark pushed a commit that referenced this pull request Feb 27, 2021
- Add -output-dir option to write updated files to a directory structure
  parallel to the base dir (#347). When -output-dir is used, a source
  file outside the base dir can't be handled because there is no way to
  compute its output path. For consistency, this is now an error even
  when -output-dir is not used.

- Convert all 3C regression tests from -output-postfix to -output-dir to
  avoid leaving temporary files in the clang/test/3C directory (#378).

- Expand "3c -help" documentation. In particular, direct the user to pass
  "--" when they don't want to use a compilation database to avoid
  accidentally using unwanted compiler options and suppress the warning
  if no compilation database is found (#343).

- For consistency, have stdout mode output the main file even if it is
  unchanged (#328).

- Fix bugs in matching of file paths against the base dir (#327).

- Other minor bug fixes: see the pull request description for details.

Co-authored-by: John Kastner <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants