Skip to content

Warn when bounds declaration cannot be proved to be true #338

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.

Sign up for GitHub

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

Jump to bottom
Closed
dtarditi opened this issue Jul 3, 2017 · 1 comment
Closed

Warn when bounds declaration cannot be proved to be true #338

dtarditi opened this issue Jul 3, 2017 · 1 comment
Assignees
@dtarditi
Labels
work item This labels issues that are not exactly bugs but are about improvements.

Comments

@dtarditi
Copy link
Member

dtarditi commented Jul 3, 2017 •
edited
Loading

Creating a warning for when a bounds declaration cannot be proved to be true after an expression statement that assigns to a variable.
@dtarditi dtarditi added the work item This labels issues that are not exactly bugs but are about improvements. label Jul 3, 2017
@dtarditi dtarditi self-assigned this Jul 3, 2017
@dtarditi dtarditi mentioned this issue Jul 6, 2017
Merged
dtarditi added a commit that referenced this issue Jul 7, 2017
@dtarditi
Warning for when bounds declarations are not provably true. (#343)
00f49f1 
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.
@dtarditi
Copy link
Member Author

The warning flag is implemented.

dopelsunce pushed a commit to dopelsunce/checkedc-clang that referenced this issue Sep 28, 2020
@dtarditi
Fix failing tests on Windows x64. (checkedc#338)
ec46c36 
Some automated tests are failing on Windows x64 after updating the LLVM/clang sources.   The tests are platform-specific and aren't supposed to be run for 64-bit Windows targets.    The target platform name for Windows changed in the LLVM test infrastructure, which caused this failure.
mgrang pushed a commit that referenced this issue Nov 23, 2020
@mattmccutchen-cci
Merge pull request #338 from correctcomputation/header-dependencies
c781cd9 
Fix header dependencies
@secure-sw-dev-bot secure-sw-dev-bot mentioned this issue Jan 16, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@dtarditi dtarditi

Labels
work item This labels issues that are not exactly bugs but are about improvements.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@dtarditi