Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Commitf98ebdb

Browse files
authored
Merge pull request#204 from mbaluda-org/Contracts6
Contracts6
2 parentsc3a6231 +ec548d0 commitf98ebdb

File tree

21 files changed

+609
-8
lines changed

21 files changed

+609
-8
lines changed

‎.vscode/tasks.json‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,11 @@
193193
"Classes",
194194
"Comments",
195195
"Contracts1",
196+
"Contracts2",
197+
"Contracts3",
198+
"Contracts4",
199+
"Contracts5",
200+
"Contracts6",
196201
"Concurrency",
197202
"Concurrency",
198203
"Concurrency1",
Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
#EXP40-C: Do not modify constant objects
2+
3+
This query implements the CERT-C rule EXP40-C:
4+
5+
>Do not modify constant objects
6+
7+
8+
##Description
9+
10+
The C Standard, 6.7.3, paragraph 6\[[IS](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)[O/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)\], states
11+
12+
>If an attempt is made to modify an object defined with a`const`-qualified type through use of an[lvalue](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-lvalue) with non-`const`-qualified type, the behavior is undefined.
13+
14+
15+
See also[undefined behavior 64](https://wiki.sei.cmu.edu/confluence/display/c/CC.+Undefined+Behavior#CC.UndefinedBehavior-ub_64).
16+
17+
There are existing compiler[implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation) that allow`const`-qualified objects to be modified without generating a warning message.
18+
19+
Avoid casting away`const` qualification because doing so makes it possible to modify`const`-qualified objects without issuing diagnostics. (See[EXP05-C. Do not cast away a const qualification](https://wiki.sei.cmu.edu/confluence/display/c/EXP05-C.+Do+not+cast+away+a+const+qualification) and[STR30-C. Do not attempt to modify string literals](https://wiki.sei.cmu.edu/confluence/display/c/STR30-C.+Do+not+attempt+to+modify+string+literals) for more details.)
20+
21+
##Noncompliant Code Example
22+
23+
This noncompliant code example allows a constant object to be modified:
24+
25+
```cpp
26+
constint **ipp;
27+
int *ip;
28+
constint i =42;
29+
30+
voidfunc(void) {
31+
ipp = &ip; /* Constraint violation*/
32+
*ipp = &i; /* Valid*/
33+
*ip = 0; /* Modifies constant i (was 42)*/
34+
}
35+
```
36+
The first assignment is unsafe because it allows the code that follows it to attempt to change the value of the `const` object `i`.
37+
38+
**Implementation Details**
39+
40+
If `ipp`, `ip`, and `i` are declared as automatic variables, this example compiles without warning with Microsoft Visual Studio 2013 when compiled in C mode (`/TC`) and the resulting program changes the value of `i`. GCC 4.8.1 generates a warning but compiles, and the resulting program changes the value of `i`.
41+
42+
If `ipp`, `ip`, and `i` are declared with static storage duration, this program compiles without warning and terminates abnormally with Microsoft Visual Studio 2013, and compiles with warning and terminates abnormally with GCC 4.8.1.
43+
44+
## Compliant Solution
45+
46+
The compliant solution depends on the intent of the programmer. If the intent is that the value of `i` is modifiable, then it should not be declared as a constant, as in this compliant solution:
47+
48+
```cpp
49+
int **ipp;
50+
int *ip;
51+
int i = 42;
52+
53+
void func(void) {
54+
ipp = &ip; /* Valid */
55+
*ipp = &i; /* Valid */
56+
*ip = 0; /* Valid */
57+
}
58+
```
59+
If the intent is that the value of i is not meant to change, then do not write noncompliant code that attempts to modify it.
60+
61+
##Risk Assessment
62+
63+
Modifying constant objects through nonconstant references is[undefined behavior](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-undefinedbehavior).
64+
65+
<table> <tbody> <tr> <th> Rule </th> <th> Severity </th> <th> Likelihood </th> <th> Remediation Cost </th> <th> Priority </th> <th> Level </th> </tr> <tr> <td> EXP40-C </td> <td> Low </td> <td> Unlikely </td> <td> Medium </td> <td> <strong>P2</strong> </td> <td> <strong>L3</strong> </td> </tr> </tbody> </table>
66+
67+
68+
##Automated Detection
69+
70+
<table> <tbody> <tr> <th> Tool </th> <th> Version </th> <th> Checker </th> <th> Description </th> </tr> <tr> <td> <a> Astrée </a> </td> <td> 22.04 </td> <td> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>pointer-qualifier-cast-const</strong> <strong>pointer-qualifier-cast-const-implicit</strong> <strong>write-to-constant-memory</strong> </td> <td> Fully checked </td> </tr> <tr> <td> <a> Axivion Bauhaus Suite </a> </td> <td> 7.2.0 </td> <td> <strong>CertC-EXP40</strong> </td> <td> </td> </tr> <tr> <td> <a> Coverity </a> </td> <td> 2017.07 </td> <td> <strong>PW</strong> <strong>MISRA C 2004 Rule 11.5</strong> </td> <td> Implemented </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.3 </td> <td> <strong>C0563</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>582 S</strong> </td> <td> Fully implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.1 </td> <td> <strong>CERT_C-EXP40-a</strong> </td> <td> A cast shall not remove any 'const' or 'volatile' qualification from the type of a pointer or reference </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule EXP40-C </a> </td> <td> Checks for write operations on const qualified objects (rule fully covered) </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>0563</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> RuleChecker </a> </td> <td> 22.04 </td> <td> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>pointer-qualifier-cast-const</strong> <strong>pointer-qualifier-cast-const-implicit</strong> </td> <td> Partially checked </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>mem_access</strong> </td> <td> Exhaustively verified (see <a> the compliant and the non-compliant example </a> ). </td> </tr> </tbody> </table>
71+
72+
73+
##Related Vulnerabilities
74+
75+
Search for[vulnerabilities](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability) resulting from the violation of this rule on the[CERT website](https://www.kb.cert.org/vulnotes/bymetric?searchview&query=FIELD+KEYWORDS+contains+EXP40-C).
76+
77+
##Related Guidelines
78+
79+
[Key here](https://wiki.sei.cmu.edu/confluence/display/c/How+this+Coding+Standard+is+Organized#HowthisCodingStandardisOrganized-RelatedGuidelines) (explains table format and definitions)
80+
81+
<table> <tbody> <tr> <th> Taxonomy </th> <th> Taxonomy item </th> <th> Relationship </th> </tr> <tr> <td> <a> CERT C Secure Coding Standard </a> </td> <td> <a> EXP05-C. Do not cast away a const qualification </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C Secure Coding Standard </a> </td> <td> <a> STR30-C. Do not attempt to modify string literals </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> </tbody> </table>
82+
83+
84+
##Bibliography
85+
86+
<table> <tbody> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> Subclause 6.7.3, "Type Qualifiers" </td> </tr> </tbody> </table>
87+
88+
89+
##Implementation notes
90+
91+
The implementation does not consider pointer aliasing via multiple indirection.
92+
93+
##References
94+
95+
* CERT-C:[EXP40-C: Do not modify constant objects](https://wiki.sei.cmu.edu/confluence/display/c)
Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/**
2+
* @id c/cert/do-not-modify-constant-objects
3+
* @name EXP40-C: Do not modify constant objects
4+
* @description Do not modify constant objects. This may result in undefined behavior.
5+
* @kind path-problem
6+
* @precision high
7+
* @problem.severity error
8+
* @tags external/cert/id/exp40-c
9+
* correctness
10+
* external/cert/obligation/rule
11+
*/
12+
13+
import cpp
14+
import codingstandards.c.cert
15+
import semmle.code.cpp.dataflow.DataFlow
16+
import DataFlow::PathGraph
17+
import codingstandards.cpp.SideEffect
18+
19+
classConstRemovingCastextendsCast{
20+
ConstRemovingCast(){
21+
this.getExpr().getType().(DerivedType).getBaseType*().isConst()and
22+
notthis.getType().(DerivedType).getBaseType*().isConst()
23+
}
24+
}
25+
26+
classMaybeReturnsStringLiteralFunctionCallextendsFunctionCall{
27+
MaybeReturnsStringLiteralFunctionCall(){
28+
getTarget().getName()in[
29+
"strpbrk","strchr","strrchr","strstr","wcspbrk","wcschr","wcsrchr","wcsstr",
30+
"memchr","wmemchr"
31+
]
32+
}
33+
}
34+
35+
classMyDataFlowConfCastextends DataFlow::Configuration{
36+
MyDataFlowConfCast(){this="MyDataFlowConfCast"}
37+
38+
overridepredicateisSource(DataFlow::Nodesource){
39+
source.asExpr().getFullyConverted()instanceofConstRemovingCast
40+
or
41+
source.asExpr().getFullyConverted()=any(MaybeReturnsStringLiteralFunctionCallc)
42+
}
43+
44+
overridepredicateisSink(DataFlow::Nodesink){
45+
sink.asExpr()=any(Assignmenta).getLValue().(PointerDereferenceExpr).getOperand()
46+
}
47+
}
48+
49+
fromMyDataFlowConfCastconf, DataFlow::PathNodesrc, DataFlow::PathNodesink
50+
where
51+
conf.hasFlowPath(src,sink)
52+
or
53+
sink.getNode()
54+
.asExpr()
55+
.(VariableEffect)
56+
.getTarget()
57+
.getType()
58+
.(DerivedType)
59+
.getBaseType*()
60+
.isConst()
61+
selectsink,src,sink,"Const variable assigned with non const-value."
Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
edges
2+
| test.c:5:8:5:9 | & ... | test.c:6:4:6:5 | aa |
3+
| test.c:26:15:26:15 | a | test.c:27:4:27:4 | a |
4+
| test.c:34:13:34:14 | & ... | test.c:39:7:39:8 | p1 |
5+
| test.c:39:7:39:8 | p1 | test.c:26:15:26:15 | a |
6+
| test.c:40:7:40:9 | * ... | test.c:26:15:26:15 | a |
7+
| test.c:59:7:59:8 | & ... | test.c:60:4:60:4 | p |
8+
| test.c:79:11:79:16 | call to strchr | test.c:81:6:81:12 | ... ++ |
9+
nodes
10+
| test.c:5:8:5:9 | & ... | semmle.label | & ... |
11+
| test.c:6:4:6:5 | aa | semmle.label | aa |
12+
| test.c:26:15:26:15 | a | semmle.label | a |
13+
| test.c:27:4:27:4 | a | semmle.label | a |
14+
| test.c:34:13:34:14 | & ... | semmle.label | & ... |
15+
| test.c:39:7:39:8 | p1 | semmle.label | p1 |
16+
| test.c:40:7:40:9 | * ... | semmle.label | * ... |
17+
| test.c:59:7:59:8 | & ... | semmle.label | & ... |
18+
| test.c:60:4:60:4 | p | semmle.label | p |
19+
| test.c:74:12:74:12 | s | semmle.label | s |
20+
| test.c:79:11:79:16 | call to strchr | semmle.label | call to strchr |
21+
| test.c:81:6:81:12 | ... ++ | semmle.label | ... ++ |
22+
subpaths
23+
#select
24+
| test.c:6:4:6:5 | aa | test.c:5:8:5:9 | & ... | test.c:6:4:6:5 | aa | Const variable assigned with non const-value. |
25+
| test.c:27:4:27:4 | a | test.c:34:13:34:14 | & ... | test.c:27:4:27:4 | a | Const variable assigned with non const-value. |
26+
| test.c:27:4:27:4 | a | test.c:40:7:40:9 | * ... | test.c:27:4:27:4 | a | Const variable assigned with non const-value. |
27+
| test.c:60:4:60:4 | p | test.c:59:7:59:8 | & ... | test.c:60:4:60:4 | p | Const variable assigned with non const-value. |
28+
| test.c:74:12:74:12 | s | test.c:74:12:74:12 | s | test.c:74:12:74:12 | s | Const variable assigned with non const-value. |
29+
| test.c:81:6:81:12 | ... ++ | test.c:79:11:79:16 | call to strchr | test.c:81:6:81:12 | ... ++ | Const variable assigned with non const-value. |
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/EXP40-C/DoNotModifyConstantObjects.ql

‎c/cert/test/rules/EXP40-C/test.c‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
voidf1() {
2+
constinta=3;
3+
int*aa;
4+
5+
aa=&a;
6+
*aa=100;// NON_COMPLIANT
7+
}
8+
9+
voidf1a() {
10+
constinta=3;
11+
int*aa;
12+
13+
aa=&a;// COMPLIANT
14+
}
15+
16+
voidf2() {
17+
inta=3;
18+
int*aa;
19+
a=3;
20+
21+
aa=&a;
22+
*aa=a;
23+
*aa=&a;
24+
}
25+
26+
voidf4a(int*a) {
27+
*a=100;// NON_COMPLIANT
28+
}
29+
30+
voidf4b(int*a) {}
31+
32+
voidf4() {
33+
constinta=100;
34+
int*p1=&a;// COMPLIANT
35+
constint**p2;
36+
37+
*p2=&a;// COMPLIANT
38+
39+
f4a(p1);// COMPLIANT
40+
f4a(*p2);// COMPLIANT
41+
}
42+
43+
voidf5() {
44+
constinta=100;
45+
int*p1=&a;// COMPLIANT
46+
constint**p2;
47+
48+
*p2=&a;// COMPLIANT
49+
50+
f4b(p1);
51+
f4b(*p2);
52+
}
53+
54+
#include<string.h>
55+
56+
voidf6a() {
57+
char*p;
58+
constcharc='A';
59+
p=&c;
60+
*p=0;// NON_COMPLIANT
61+
}
62+
63+
voidf6b() {
64+
constchar**cpp;
65+
char*p;
66+
constcharc='A';
67+
cpp=&p;
68+
*cpp=&c;
69+
*p=0;// NON_COMPLIANT[FALSE_NEGATIVE]
70+
}
71+
72+
constchars[]="foo";// source
73+
voidf7() {
74+
*(char*)s='\0';// NON_COMPLIANT
75+
}
76+
77+
constchar*f8(constchar*pathname) {
78+
char*slash;
79+
slash=strchr(pathname,'/');
80+
if (slash) {
81+
*slash++='\0';// NON_COMPLIANT
82+
returnslash;
83+
}
84+
returnpathname;
85+
}
Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
/**
2+
* @id c/misra/array-function-argument-number-of-elements
3+
* @name RULE-17-5: An array founction argument shall have an appropriate number of elements
4+
* @description The function argument corresponding to an array parameter shall have an appropriate
5+
* number of elements.
6+
* @kind problem
7+
* @precision high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-17-5
10+
* correctness
11+
* external/misra/obligation/advisory
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.misra
16+
import semmle.code.cpp.dataflow.DataFlow
17+
18+
/**
19+
* Models a function parameter of type array with specified size
20+
* ```
21+
* void f1(int ar[3]);
22+
* ```
23+
*/
24+
classArrayParameterextendsParameter{
25+
ArrayParameter(){this.getType().(ArrayType).hasArraySize()}
26+
27+
ExprgetAMatchingArgument(){
28+
exists(FunctionCallfc|
29+
this.getFunction()=fc.getTarget()and
30+
result=fc.getArgument(this.getIndex())
31+
)
32+
}
33+
34+
intgetArraySize(){result=this.getType().(ArrayType).getArraySize()}
35+
}
36+
37+
/**
38+
* The number of initialized elements in an ArrayAggregateLiteral.
39+
* In the following examples the result=2
40+
* ```
41+
* int arr3[3] = {1, 2};
42+
* int arr2[2] = {1, 2, 3};
43+
* ```
44+
*/
45+
intcountElements(ArrayAggregateLiterall){result=count(l.getElementExpr(_))}
46+
47+
classSmallArrayConfigextends DataFlow::Configuration{
48+
SmallArrayConfig(){this="SmallArrayConfig"}
49+
50+
overridepredicateisSource(DataFlow::Nodesrc){src.asExpr()instanceofArrayAggregateLiteral}
51+
52+
overridepredicateisSink(DataFlow::Nodesink){
53+
sink.asExpr()=any(ArrayParameterp).getAMatchingArgument()
54+
}
55+
}
56+
57+
fromExprarg,ArrayParameterp
58+
where
59+
notisExcluded(arg, Contracts6Package::arrayFunctionArgumentNumberOfElementsQuery())and
60+
exists(SmallArrayConfigconfig|arg=p.getAMatchingArgument()|
61+
// the argument is a value and not an arrey
62+
notarg.getType()instanceofDerivedType
63+
or
64+
// the argument is an array too small
65+
arg.getType().(ArrayType).getArraySize()<p.getArraySize()
66+
or
67+
// the argument is a pointer and its value does not come from a literal of the correct
68+
arg.getType()instanceofPointerTypeand
69+
notexists(ArrayAggregateLiterall|
70+
config.hasFlow(DataFlow::exprNode(l), DataFlow::exprNode(arg))and
71+
countElements(l)>=p.getArraySize()
72+
)
73+
)
74+
selectarg,
75+
"The function argument does not have a sufficient number or elements declared in the $@.",p,
76+
"parameter"
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/**
2+
* @id c/misra/value-returned-by-a-function-not-used
3+
* @name RULE-17-7: Return values should be used or cast to void
4+
* @description The value returned by a function having non-void return type shall be used or cast
5+
* to void.
6+
* @kind problem
7+
* @precision very-high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-17-7
10+
* correctness
11+
* external/misra/obligation/required
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.misra
16+
import semmle.code.cpp.dataflow.DataFlow
17+
18+
fromCallc
19+
where
20+
notisExcluded(c, Contracts6Package::valueReturnedByAFunctionNotUsedQuery())and
21+
// Calls in `ExprStmt`s indicate that the return value is ignored
22+
c.getParent()instanceofExprStmtand
23+
// Ignore calls to void functions or where the return value is cast to `void`
24+
notc.getActualType()instanceofVoidTypeand
25+
// Exclude cases where the function call is generated within a macro, as the user of the macro is
26+
// not necessarily able to address thoes results
27+
notc.isAffectedByMacro()
28+
selectc,"The value returned by this call shall be used or cast to `void`."

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp