Skip to content

Commit dbb4523

Browse files
Address most MISRA C 2012 rule amendments in Amendment3.
Does not address amendments that are covered in other PRs (clarifications) or Generics behavior. Most updates related to complex floating types. One update related to emergent language features.
1 parent 89bd9b4 commit dbb4523

28 files changed

+1104
-640
lines changed

amendments.csv

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
language,standard,amendment,rule_id,supportable,implementation_category,implemented,difficulty
2-
c,MISRA-C-2012,Amendment3,DIR-4-6,Yes,Expand,No,Easy
2+
c,MISRA-C-2012,Amendment3,DIR-4-6,Yes,Expand,Yes,Easy
33
c,MISRA-C-2012,Amendment3,DIR-4-9,Yes,Refine,No,Easy
44
c,MISRA-C-2012,Amendment3,DIR-4-11,Yes,Refine,No,Import
5-
c,MISRA-C-2012,Amendment3,RULE-1-4,Yes,Replace,No,Easy
6-
c,MISRA-C-2012,Amendment3,RULE-10-1,Yes,Replace,No,Easy
7-
c,MISRA-C-2012,Amendment3,RULE-10-3,Yes,Refine,No,Easy
8-
c,MISRA-C-2012,Amendment3,RULE-10-4,Yes,Refine,No,Import
9-
c,MISRA-C-2012,Amendment3,RULE-10-5,Yes,Expand,No,Easy
10-
c,MISRA-C-2012,Amendment3,RULE-10-7,Yes,Refine,No,Import
11-
c,MISRA-C-2012,Amendment3,RULE-10-8,Yes,Refine,No,Import
5+
c,MISRA-C-2012,Amendment3,RULE-1-4,Yes,Replace,Yes,Easy
6+
c,MISRA-C-2012,Amendment3,RULE-10-1,Yes,Replace,Yes,Easy
7+
c,MISRA-C-2012,Amendment3,RULE-10-3,Yes,Refine,Yes,Easy
8+
c,MISRA-C-2012,Amendment3,RULE-10-4,Yes,Refine,Yes,Import
9+
c,MISRA-C-2012,Amendment3,RULE-10-5,Yes,Expand,Yes,Easy
10+
c,MISRA-C-2012,Amendment3,RULE-10-7,Yes,Refine,Yes,Import
11+
c,MISRA-C-2012,Amendment3,RULE-10-8,Yes,Refine,Yes,Import
1212
c,MISRA-C-2012,Amendment3,RULE-21-11,Yes,Clarification,No,Import
1313
c,MISRA-C-2012,Amendment3,RULE-21-12,Yes,Replace,No,Easy
1414
c,MISRA-C-2012,Amendment4,RULE-11-3,Yes,Expand,No,Easy
@@ -24,7 +24,7 @@ c,MISRA-C-2012,Corrigendum2,RULE-8-9,Yes,Clarification,No,Import
2424
c,MISRA-C-2012,Corrigendum2,RULE-9-4,Yes,Clarification,No,Import
2525
c,MISRA-C-2012,Corrigendum2,RULE-10-1,Yes,Clarification,No,Import
2626
c,MISRA-C-2012,Corrigendum2,RULE-18-3,Yes,Clarification,No,Import
27-
c,MISRA-C-2012,Corrigendum2,RULE-1-4,Yes,Replace,No,Easy
27+
c,MISRA-C-2012,Corrigendum2,RULE-1-4,Yes,Replace,Yes,Easy
2828
c,MISRA-C-2012,Corrigendum2,RULE-9-1,Yes,Refine,No,Easy
2929
c,MISRA-C-2012,Corrigendum2,RULE-9-2,Yes,Refine,No,Import
3030
c,MISRA-C-2012,Corrigendum2,DIR-4-10,Yes,Clarification,No,Import

c/misra/src/codingstandards/c/misra/EssentialTypes.qll

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,17 @@ import codingstandards.c.misra
66
import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
77
import MisraExpressions
88

9+
newtype TEssentialFloatCategory =
10+
Real() or
11+
Complex()
12+
913
newtype TEssentialTypeCategory =
1014
EssentiallyBooleanType() or
1115
EssentiallyCharacterType() or
1216
EssentiallyEnumType() or
1317
EssentiallySignedType() or
1418
EssentiallyUnsignedType() or
15-
EssentiallyFloatingType()
19+
EssentiallyFloatingType(TEssentialFloatCategory c)
1620

1721
/** An essential type category, as specified by Appendix D.1. */
1822
class EssentialTypeCategory extends TEssentialTypeCategory {
@@ -27,7 +31,9 @@ class EssentialTypeCategory extends TEssentialTypeCategory {
2731
or
2832
this = EssentiallyUnsignedType() and result = "essentially Unsigned type"
2933
or
30-
this = EssentiallyFloatingType() and result = "essentially Floating type"
34+
this = EssentiallyFloatingType(Real()) and result = "essentially Floating type"
35+
or
36+
this = EssentiallyFloatingType(Complex()) and result = "essentially Complex Floating type"
3137
}
3238
}
3339

@@ -143,8 +149,11 @@ EssentialTypeCategory getEssentialTypeCategory(Type type) {
143149
essentialType instanceof NamedEnumType and
144150
not essentialType instanceof MisraBoolType
145151
or
146-
result = EssentiallyFloatingType() and
147-
essentialType instanceof FloatingPointType
152+
result = EssentiallyFloatingType(Real()) and
153+
essentialType instanceof RealNumberType
154+
or
155+
result = EssentiallyFloatingType(Complex()) and
156+
essentialType instanceof ComplexNumberType
148157
)
149158
}
150159

@@ -166,6 +175,17 @@ Type getEssentialType(Expr e) {
166175

167176
Type getEssentialTypeBeforeConversions(Expr e) { result = e.(EssentialExpr).getEssentialType() }
168177

178+
/**
179+
* For most essential types, `Type.getSize()` is correct, except for complex floating types.
180+
*
181+
* For complex floating types, the size is the size of the real part, so we divide by 2.
182+
*/
183+
int getEssentialSize(Type essentialType) {
184+
if getEssentialTypeCategory(essentialType) = EssentiallyFloatingType(Complex())
185+
then result = essentialType.getSize() / 2
186+
else result = essentialType.getSize()
187+
}
188+
169189
class EssentialExpr extends Expr {
170190
Type getEssentialType() { result = this.getType() }
171191

c/misra/src/rules/DIR-4-6/PlainNumericalTypeUsedOverExplicitTypedef.ql

Lines changed: 51 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ class BuiltInNumericType extends BuiltInType {
2929
this instanceof DoubleType
3030
or
3131
this instanceof LongDoubleType
32+
or
33+
this instanceof ComplexNumberType
3234
}
3335
}
3436

@@ -38,22 +40,64 @@ predicate forbiddenBuiltinNumericUsedInDecl(Variable var, string message) {
3840
message = "The type " + var.getType() + " is not a fixed-width numeric type."
3941
}
4042

43+
class SizedTypeString extends string {
44+
string pattern;
45+
int size;
46+
47+
bindingset[this]
48+
pragma[inline]
49+
SizedTypeString() {
50+
pattern = "(u?int|c?float)(4|8|16|32|64|128)_t" and
51+
this.regexpMatch(pattern) and
52+
size = this.regexpCapture(pattern, 2).toInt()
53+
}
54+
55+
bindingset[this]
56+
pragma[inline]
57+
int getSize() { result = size }
58+
59+
bindingset[this]
60+
pragma[inline]
61+
predicate isComplex() { this.charAt(0) = "c" }
62+
}
63+
64+
predicate forbiddenComplexType(CTypedefType typedef, string message) {
65+
typedef.getName().(SizedTypeString).isComplex() and
66+
(
67+
if typedef.getBaseType().stripTopLevelSpecifiers() instanceof ComplexNumberType
68+
then
69+
typedef.getSize() * 8 != typedef.getName().(SizedTypeString).getSize() * 2 and
70+
message = "The typedef type " + typedef.getName() + " does not have its indicated real size."
71+
else message = "The typedef type " + typedef.getName() + " is not a complex type."
72+
)
73+
}
74+
75+
predicate forbiddenRealType(CTypedefType typedef, string message) {
76+
not typedef.getName().(SizedTypeString).isComplex() and
77+
(
78+
if typedef.getBaseType().stripTopLevelSpecifiers() instanceof ComplexNumberType
79+
then message = "The typedef name " + typedef.getName() + " does not indicate a complex type."
80+
else (
81+
typedef.getSize() * 8 != typedef.getName().(SizedTypeString).getSize() and
82+
message = "The typedef type " + typedef.getName() + " does not have its indicated size."
83+
)
84+
)
85+
}
86+
4187
predicate forbiddenTypedef(CTypedefType typedef, string message) {
4288
/* If the typedef's name contains an explicit size */
4389
(
44-
if typedef.getName().regexpMatch("u?(int|float)(4|8|16|32|64|128)_t")
90+
if typedef.getName() instanceof SizedTypeString
4591
then (
46-
/* Then the actual type size should match. */
47-
not typedef.getSize() * 8 =
48-
// times 8 because getSize() gets the size in bytes
49-
typedef.getName().regexpCapture("u?(int|float)(4|8|16|32|64|128)_t", 2).toInt() and
50-
message = "The typedef type " + typedef.getName() + " does not have its indicated size."
92+
forbiddenRealType(typedef, message)
93+
or
94+
forbiddenComplexType(typedef, message)
5195
) else (
5296
(
5397
// type def is to a built in numeric type
5498
typedef.getBaseType() instanceof BuiltInNumericType and
5599
// but does not include the size in the name
56-
not typedef.getName().regexpMatch("u?(int|float)(4|8|16|32|64|128)_t")
100+
not typedef.getName() instanceof SizedTypeString
57101
or
58102
// this is a typedef to a forbidden type def
59103
forbiddenTypedef(typedef.getBaseType(), _)

c/misra/src/rules/RULE-10-1/OperandsOfAnInappropriateEssentialType.ql

Lines changed: 57 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,15 @@ import cpp
1616
import codingstandards.c.misra
1717
import codingstandards.c.misra.EssentialTypes
1818

19+
predicate hasComparableFloatValue(Expr e) {
20+
exists(float value |
21+
value = e.getValue().toFloat() or
22+
value = -e.(UnaryMinusExpr).getOperand().getValue().toFloat()
23+
|
24+
value in [0.0, "Infinity".toFloat(), -"Infinity".toFloat()]
25+
)
26+
}
27+
1928
/**
2029
* Holds if the operator `operator` has an operand `child` that is of an inappropriate essential type
2130
* according to MISRA C 2012 Rule 10.1.
@@ -33,8 +42,11 @@ predicate isInappropriateEssentialType(
3342
etc = EssentiallyCharacterType() and
3443
rationaleId = 4
3544
or
36-
etc = EssentiallyFloatingType() and
45+
etc = EssentiallyFloatingType(Real()) and
3746
rationaleId = 1
47+
or
48+
etc = EssentiallyFloatingType(Complex()) and
49+
rationaleId = 9
3850
)
3951
or
4052
child = operator.(UnaryPlusExpr).getOperand() and
@@ -64,8 +76,6 @@ predicate isInappropriateEssentialType(
6476
rationaleId = 8
6577
)
6678
or
67-
// The table only talks about + and -, but below it clarifies ++ and -- are also considered to
68-
// be equivalent.
6979
child =
7080
[
7181
operator.(AddExpr).getAnOperand(), operator.(SubExpr).getAnOperand(),
@@ -80,6 +90,13 @@ predicate isInappropriateEssentialType(
8090
rationaleId = 5
8191
)
8292
or
93+
child =
94+
[operator.(IncrementOperation).getAnOperand(), operator.(DecrementOperation).getAnOperand()] and
95+
(
96+
etc = EssentiallyFloatingType(Complex()) and
97+
rationaleId = 9
98+
)
99+
or
83100
child =
84101
[
85102
operator.(DivExpr).getAnOperand(), operator.(MulExpr).getAnOperand(),
@@ -107,13 +124,26 @@ predicate isInappropriateEssentialType(
107124
etc = EssentiallyEnumType() and
108125
rationaleId = 5
109126
or
110-
etc = EssentiallyFloatingType() and
127+
etc = EssentiallyFloatingType(Real()) and
111128
rationaleId = 1
129+
or
130+
etc = EssentiallyFloatingType(Complex()) and
131+
rationaleId = 9
112132
)
113133
or
114134
child = operator.(RelationalOperation).getAnOperand() and
115-
etc = EssentiallyBooleanType() and
116-
rationaleId = 3
135+
(
136+
etc = EssentiallyBooleanType() and
137+
rationaleId = 3
138+
or
139+
etc = EssentiallyFloatingType(Complex()) and
140+
rationaleId = 9
141+
)
142+
or
143+
child = operator.(EqualityOperation).getAnOperand() and
144+
rationaleId = 10 and
145+
not hasComparableFloatValue(operator.(EqualityOperation).getAnOperand()) and
146+
etc = EssentiallyFloatingType(_)
117147
or
118148
child = [operator.(NotExpr).getAnOperand(), operator.(BinaryLogicalOperation).getAnOperand()] and
119149
rationaleId = 2 and
@@ -126,7 +156,7 @@ predicate isInappropriateEssentialType(
126156
or
127157
etc = EssentiallyUnsignedType()
128158
or
129-
etc = EssentiallyFloatingType()
159+
etc = EssentiallyFloatingType(_)
130160
)
131161
or
132162
child =
@@ -147,8 +177,11 @@ predicate isInappropriateEssentialType(
147177
etc = EssentiallySignedType() and
148178
rationaleId = 6
149179
or
150-
etc = EssentiallyFloatingType() and
180+
etc = EssentiallyFloatingType(Real()) and
151181
rationaleId = 1
182+
or
183+
etc = EssentiallyFloatingType(Complex()) and
184+
rationaleId = 9
152185
)
153186
or
154187
child =
@@ -171,8 +204,11 @@ predicate isInappropriateEssentialType(
171204
etc = EssentiallySignedType() and
172205
rationaleId = 7
173206
or
174-
etc = EssentiallyFloatingType() and
207+
etc = EssentiallyFloatingType(Real()) and
175208
rationaleId = 1
209+
or
210+
etc = EssentiallyFloatingType(Complex()) and
211+
rationaleId = 9
176212
)
177213
or
178214
child =
@@ -197,8 +233,11 @@ predicate isInappropriateEssentialType(
197233
etc = EssentiallySignedType() and
198234
rationaleId = 6
199235
or
200-
etc = EssentiallyFloatingType() and
236+
etc = EssentiallyFloatingType(Real()) and
201237
rationaleId = 1
238+
or
239+
etc = EssentiallyFloatingType(Complex()) and
240+
rationaleId = 9
202241
)
203242
or
204243
child = operator.(ConditionalExpr).getCondition() and
@@ -215,7 +254,7 @@ predicate isInappropriateEssentialType(
215254
etc = EssentiallyUnsignedType() and
216255
rationaleId = 2
217256
or
218-
etc = EssentiallyFloatingType() and
257+
etc = EssentiallyFloatingType(_) and
219258
rationaleId = 2
220259
)
221260
)
@@ -245,6 +284,13 @@ string getRationaleMessage(int rationaleId, EssentialTypeCategory etc) {
245284
rationaleId = 8 and
246285
result =
247286
"Operand of essentially Unsigned type will be converted to a signed type with the signedness dependent on the implemented size of int."
287+
or
288+
rationaleId = 9 and
289+
result = "Use of essentially Complex type in this way is a constraint violation."
290+
or
291+
rationaleId = 10 and
292+
result =
293+
"Floating point numbers have inherent error such that comparisons should consider precision and not exact equality."
248294
}
249295

250296
from Expr operator, Expr child, int rationaleId, EssentialTypeCategory etc

c/misra/src/rules/RULE-10-3/AssignmentOfIncompatibleEssentialType.ql

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,5 +48,11 @@ where
4848
lValueTypeCategory = EssentiallyUnsignedType() and
4949
const >= 0 and
5050
const <= 2.pow(lValueEssentialType.getSize() * 8)
51+
) and
52+
// Exception 4: Real floating point values may be assignable to complex floating point values
53+
not (
54+
lValueTypeCategory = EssentiallyFloatingType(Complex()) and
55+
rValueTypeCategory = EssentiallyFloatingType(Real()) and
56+
lValueEssentialType.getSize() >= rValueEssentialType.getSize() * 2
5157
)
5258
select rValue, message

c/misra/src/rules/RULE-10-4/OperandsWithMismatchedEssentialTypeCategory.ql

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,11 @@ where
3030
rightOpTypeCategory = getEssentialTypeCategory(rightOpEssentialType) and
3131
(
3232
not leftOpTypeCategory = rightOpTypeCategory and
33+
not (
34+
// Exception 3: Operands where both are real or complex floating types are allowed.
35+
leftOpTypeCategory = EssentiallyFloatingType(_) and
36+
rightOpTypeCategory = EssentiallyFloatingType(_)
37+
) and
3338
message =
3439
"The operands of this operator with usual arithmetic conversions have mismatched essential types (left operand: "
3540
+ leftOpTypeCategory + ", right operand: " + rightOpTypeCategory + ")."

c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,14 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
2323
toCat =
2424
[
2525
EssentiallyCharacterType(), EssentiallyEnumType(), EssentiallySignedType(),
26-
EssentiallyUnsignedType(), EssentiallyFloatingType().(TEssentialTypeCategory)
26+
EssentiallyUnsignedType(), EssentiallyFloatingType(_).(TEssentialTypeCategory)
2727
]
2828
or
2929
fromCat = EssentiallyCharacterType() and
3030
toCat =
3131
[
3232
EssentiallyBooleanType(), EssentiallyEnumType(),
33-
EssentiallyFloatingType().(TEssentialTypeCategory)
33+
EssentiallyFloatingType(_).(TEssentialTypeCategory)
3434
]
3535
or
3636
fromCat = EssentiallyEnumType() and
@@ -42,7 +42,7 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
4242
fromCat = EssentiallyUnsignedType() and
4343
toCat = [EssentiallyBooleanType(), EssentiallyEnumType().(TEssentialTypeCategory)]
4444
or
45-
fromCat = EssentiallyFloatingType() and
45+
fromCat = EssentiallyFloatingType(_) and
4646
toCat =
4747
[
4848
EssentiallyBooleanType(), EssentiallyCharacterType(),

c/misra/src/rules/RULE-10-7/ImplicitConversionOfCompositeExpression.ql

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,10 @@ bindingset[essentialTypeLeft, essentialTypeRight]
2323
pragma[inline_late]
2424
predicate isSameEssentialTypeCategory(Type essentialTypeLeft, Type essentialTypeRight) {
2525
getEssentialTypeCategory(essentialTypeLeft) = getEssentialTypeCategory(essentialTypeRight)
26+
or
27+
// Complex and real floating types are considered interchangeable
28+
getEssentialTypeCategory(essentialTypeLeft) = EssentiallyFloatingType(_) and
29+
getEssentialTypeCategory(essentialTypeRight) = EssentiallyFloatingType(_)
2630
}
2731

2832
from
@@ -35,7 +39,7 @@ where
3539
not otherOp = compositeOp and
3640
compositeEssentialType = getEssentialType(compositeOp) and
3741
otherOpEssentialType = getEssentialType(otherOp) and
38-
compositeEssentialType.getSize() < otherOpEssentialType.getSize() and
42+
getEssentialSize(compositeEssentialType) < getEssentialSize(otherOpEssentialType) and
3943
// Operands of a different type category in an operation with the usual arithmetic conversions is
4044
// prohibited by Rule 10.4, so we only report cases here where the essential type categories are
4145
// the same

0 commit comments

Comments
 (0)