-
Notifications
You must be signed in to change notification settings - Fork 59
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
Add C Contracts
package
#512
Open
lcartey
wants to merge
16
commits into
main
Choose a base branch
from
lcartey/contracts
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Adds a query that finds cases where extern inlined functions reference internal linkage objects, or declare objects which are static or thread local.
Add query which detects domain and pole errors for math.h functions.
Create a new shared query from the implementation of M0-3-2, which detects cases where error checking has not occurred after a call to a standard C library function.
Specify the scope of each of the newly supported rules.
30 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
I recently reviewed a number of unimplemented MISRA C and CERT C rules related to the contracts which we had marked as either "compiler supported" or "covered by other rules", and identified some cases which
MSC40-C
- Do not violate constraints - there is a requirement that the compiler produce a diagnostic when the constraints are violated. However, the CERT rule lists a specific cases which is known to not be reported by compilers. I have therefore added a new query to cover this case.DIR-4-7
- If a function returns error information, then that error information shall be tested - as a directive we are not required to fully cover this rule. However, we already had a query forM0-3-2
that identifies cases where C standard library functions are called and where possible error states are not checked. I have shared this implementation.DIR-4-11
- The validity of values passed to library functions shall be checked - similar toDIR-4-7
, we already have a query which identifies domain, range and pole errors with calls to functions inmath.h
. I have also shared this implementation.Change request type
.ql
,.qll
,.qls
or unit tests)Rules with added or modified queries
MSC40-C
DIR-4-7
DIR-4-11
M0-3-2
Release change checklist
A change note (development_handbook.md#change-notes) is required for any pull request which modifies:
If you are only adding new rule queries, a change note is not required.
Author: Is a change note required?
🚨🚨🚨
Reviewer: Confirm that format of shared queries (not the .qll file, the
.ql file that imports it) is valid by running them within VS Code.
Reviewer: Confirm that either a change note is not required or the change note is required and has been added.
Query development review checklist
For PRs that add new queries or modify existing queries, the following checklist should be completed by both the author and reviewer:
Author
As a rule of thumb, predicates specific to the query should take no more than 1 minute, and for simple queries be under 10 seconds. If this is not the case, this should be highlighted and agreed in the code review process.
Reviewer
As a rule of thumb, predicates specific to the query should take no more than 1 minute, and for simple queries be under 10 seconds. If this is not the case, this should be highlighted and agreed in the code review process.