diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index c898386d9a..2730f99e87 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -193,6 +193,11 @@
"Classes",
"Comments",
"Contracts1",
+ "Contracts2",
+ "Contracts3",
+ "Contracts4",
+ "Contracts5",
+ "Contracts6",
"Concurrency",
"Concurrency",
"Concurrency1",
diff --git a/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.md b/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.md
new file mode 100644
index 0000000000..6effa8e7c4
--- /dev/null
+++ b/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.md
@@ -0,0 +1,95 @@
+# EXP40-C: Do not modify constant objects
+
+This query implements the CERT-C rule EXP40-C:
+
+> Do not modify constant objects
+
+
+## Description
+
+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
+
+> 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.
+
+
+See also [undefined behavior 64](https://wiki.sei.cmu.edu/confluence/display/c/CC.+Undefined+Behavior#CC.UndefinedBehavior-ub_64).
+
+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.
+
+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.)
+
+## Noncompliant Code Example
+
+This noncompliant code example allows a constant object to be modified:
+
+```cpp
+const int **ipp;
+int *ip;
+const int i = 42;
+
+void func(void) {
+ ipp = &ip; /* Constraint violation */
+ *ipp = &i; /* Valid */
+ *ip = 0; /* Modifies constant i (was 42) */
+}
+```
+The first assignment is unsafe because it allows the code that follows it to attempt to change the value of the `const` object `i`.
+
+**Implementation Details**
+
+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`.
+
+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.
+
+## Compliant Solution
+
+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:
+
+```cpp
+int **ipp;
+int *ip;
+int i = 42;
+
+void func(void) {
+ ipp = &ip; /* Valid */
+ *ipp = &i; /* Valid */
+ *ip = 0; /* Valid */
+}
+```
+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.
+
+## Risk Assessment
+
+Modifying constant objects through nonconstant references is [undefined behavior](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-undefinedbehavior).
+
+
Rule | Severity | Likelihood | Remediation Cost | Priority | Level |
EXP40-C | Low | Unlikely | Medium | P2 | L3 |
+
+
+## Automated Detection
+
+
+
+
+## Related Vulnerabilities
+
+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).
+
+## Related Guidelines
+
+[Key here](https://wiki.sei.cmu.edu/confluence/display/c/How+this+Coding+Standard+is+Organized#HowthisCodingStandardisOrganized-RelatedGuidelines) (explains table format and definitions)
+
+
+
+
+## Bibliography
+
+
+
+
+## Implementation notes
+
+The implementation does not consider pointer aliasing via multiple indirection.
+
+## References
+
+* CERT-C: [EXP40-C: Do not modify constant objects](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.ql b/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.ql
new file mode 100644
index 0000000000..08901f2016
--- /dev/null
+++ b/c/cert/src/rules/EXP40-C/DoNotModifyConstantObjects.ql
@@ -0,0 +1,61 @@
+/**
+ * @id c/cert/do-not-modify-constant-objects
+ * @name EXP40-C: Do not modify constant objects
+ * @description Do not modify constant objects. This may result in undefined behavior.
+ * @kind path-problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/exp40-c
+ * correctness
+ * external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import semmle.code.cpp.dataflow.DataFlow
+import DataFlow::PathGraph
+import codingstandards.cpp.SideEffect
+
+class ConstRemovingCast extends Cast {
+ ConstRemovingCast() {
+ this.getExpr().getType().(DerivedType).getBaseType*().isConst() and
+ not this.getType().(DerivedType).getBaseType*().isConst()
+ }
+}
+
+class MaybeReturnsStringLiteralFunctionCall extends FunctionCall {
+ MaybeReturnsStringLiteralFunctionCall() {
+ getTarget().getName() in [
+ "strpbrk", "strchr", "strrchr", "strstr", "wcspbrk", "wcschr", "wcsrchr", "wcsstr",
+ "memchr", "wmemchr"
+ ]
+ }
+}
+
+class MyDataFlowConfCast extends DataFlow::Configuration {
+ MyDataFlowConfCast() { this = "MyDataFlowConfCast" }
+
+ override predicate isSource(DataFlow::Node source) {
+ source.asExpr().getFullyConverted() instanceof ConstRemovingCast
+ or
+ source.asExpr().getFullyConverted() = any(MaybeReturnsStringLiteralFunctionCall c)
+ }
+
+ override predicate isSink(DataFlow::Node sink) {
+ sink.asExpr() = any(Assignment a).getLValue().(PointerDereferenceExpr).getOperand()
+ }
+}
+
+from MyDataFlowConfCast conf, DataFlow::PathNode src, DataFlow::PathNode sink
+where
+ conf.hasFlowPath(src, sink)
+ or
+ sink.getNode()
+ .asExpr()
+ .(VariableEffect)
+ .getTarget()
+ .getType()
+ .(DerivedType)
+ .getBaseType*()
+ .isConst()
+select sink, src, sink, "Const variable assigned with non const-value."
diff --git a/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.expected b/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.expected
new file mode 100644
index 0000000000..3211c4fab1
--- /dev/null
+++ b/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.expected
@@ -0,0 +1,29 @@
+edges
+| test.c:5:8:5:9 | & ... | test.c:6:4:6:5 | aa |
+| test.c:26:15:26:15 | a | test.c:27:4:27:4 | a |
+| test.c:34:13:34:14 | & ... | test.c:39:7:39:8 | p1 |
+| test.c:39:7:39:8 | p1 | test.c:26:15:26:15 | a |
+| test.c:40:7:40:9 | * ... | test.c:26:15:26:15 | a |
+| test.c:59:7:59:8 | & ... | test.c:60:4:60:4 | p |
+| test.c:79:11:79:16 | call to strchr | test.c:81:6:81:12 | ... ++ |
+nodes
+| test.c:5:8:5:9 | & ... | semmle.label | & ... |
+| test.c:6:4:6:5 | aa | semmle.label | aa |
+| test.c:26:15:26:15 | a | semmle.label | a |
+| test.c:27:4:27:4 | a | semmle.label | a |
+| test.c:34:13:34:14 | & ... | semmle.label | & ... |
+| test.c:39:7:39:8 | p1 | semmle.label | p1 |
+| test.c:40:7:40:9 | * ... | semmle.label | * ... |
+| test.c:59:7:59:8 | & ... | semmle.label | & ... |
+| test.c:60:4:60:4 | p | semmle.label | p |
+| test.c:74:12:74:12 | s | semmle.label | s |
+| test.c:79:11:79:16 | call to strchr | semmle.label | call to strchr |
+| test.c:81:6:81:12 | ... ++ | semmle.label | ... ++ |
+subpaths
+#select
+| 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. |
+| 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. |
+| 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. |
+| 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. |
+| 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. |
+| 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. |
diff --git a/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.qlref b/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.qlref
new file mode 100644
index 0000000000..c07ac22f37
--- /dev/null
+++ b/c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.qlref
@@ -0,0 +1 @@
+rules/EXP40-C/DoNotModifyConstantObjects.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/EXP40-C/test.c b/c/cert/test/rules/EXP40-C/test.c
new file mode 100644
index 0000000000..dca79d3d36
--- /dev/null
+++ b/c/cert/test/rules/EXP40-C/test.c
@@ -0,0 +1,85 @@
+void f1() {
+ const int a = 3;
+ int *aa;
+
+ aa = &a;
+ *aa = 100; // NON_COMPLIANT
+}
+
+void f1a() {
+ const int a = 3;
+ int *aa;
+
+ aa = &a; // COMPLIANT
+}
+
+void f2() {
+ int a = 3;
+ int *aa;
+ a = 3;
+
+ aa = &a;
+ *aa = a;
+ *aa = &a;
+}
+
+void f4a(int *a) {
+ *a = 100; // NON_COMPLIANT
+}
+
+void f4b(int *a) {}
+
+void f4() {
+ const int a = 100;
+ int *p1 = &a; // COMPLIANT
+ const int **p2;
+
+ *p2 = &a; // COMPLIANT
+
+ f4a(p1); // COMPLIANT
+ f4a(*p2); // COMPLIANT
+}
+
+void f5() {
+ const int a = 100;
+ int *p1 = &a; // COMPLIANT
+ const int **p2;
+
+ *p2 = &a; // COMPLIANT
+
+ f4b(p1);
+ f4b(*p2);
+}
+
+#include
+
+void f6a() {
+ char *p;
+ const char c = 'A';
+ p = &c;
+ *p = 0; // NON_COMPLIANT
+}
+
+void f6b() {
+ const char **cpp;
+ char *p;
+ const char c = 'A';
+ cpp = &p;
+ *cpp = &c;
+ *p = 0; // NON_COMPLIANT[FALSE_NEGATIVE]
+}
+
+const char s[] = "foo"; // source
+void f7() {
+ *(char *)s = '\0'; // NON_COMPLIANT
+}
+
+const char *f8(const char *pathname) {
+ char *slash;
+ slash = strchr(pathname, '/');
+ if (slash) {
+ *slash++ = '\0'; // NON_COMPLIANT
+ return slash;
+ }
+ return pathname;
+}
\ No newline at end of file
diff --git a/c/misra/src/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.ql b/c/misra/src/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.ql
new file mode 100644
index 0000000000..0b5b95016c
--- /dev/null
+++ b/c/misra/src/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.ql
@@ -0,0 +1,76 @@
+/**
+ * @id c/misra/array-function-argument-number-of-elements
+ * @name RULE-17-5: An array founction argument shall have an appropriate number of elements
+ * @description The function argument corresponding to an array parameter shall have an appropriate
+ * number of elements.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/misra/id/rule-17-5
+ * correctness
+ * external/misra/obligation/advisory
+ */
+
+import cpp
+import codingstandards.c.misra
+import semmle.code.cpp.dataflow.DataFlow
+
+/**
+ * Models a function parameter of type array with specified size
+ * ```
+ * void f1(int ar[3]);
+ * ```
+ */
+class ArrayParameter extends Parameter {
+ ArrayParameter() { this.getType().(ArrayType).hasArraySize() }
+
+ Expr getAMatchingArgument() {
+ exists(FunctionCall fc |
+ this.getFunction() = fc.getTarget() and
+ result = fc.getArgument(this.getIndex())
+ )
+ }
+
+ int getArraySize() { result = this.getType().(ArrayType).getArraySize() }
+}
+
+/**
+ * The number of initialized elements in an ArrayAggregateLiteral.
+ * In the following examples the result=2
+ * ```
+ * int arr3[3] = {1, 2};
+ * int arr2[2] = {1, 2, 3};
+ * ```
+ */
+int countElements(ArrayAggregateLiteral l) { result = count(l.getElementExpr(_)) }
+
+class SmallArrayConfig extends DataFlow::Configuration {
+ SmallArrayConfig() { this = "SmallArrayConfig" }
+
+ override predicate isSource(DataFlow::Node src) { src.asExpr() instanceof ArrayAggregateLiteral }
+
+ override predicate isSink(DataFlow::Node sink) {
+ sink.asExpr() = any(ArrayParameter p).getAMatchingArgument()
+ }
+}
+
+from Expr arg, ArrayParameter p
+where
+ not isExcluded(arg, Contracts6Package::arrayFunctionArgumentNumberOfElementsQuery()) and
+ exists(SmallArrayConfig config | arg = p.getAMatchingArgument() |
+ // the argument is a value and not an arrey
+ not arg.getType() instanceof DerivedType
+ or
+ // the argument is an array too small
+ arg.getType().(ArrayType).getArraySize() < p.getArraySize()
+ or
+ // the argument is a pointer and its value does not come from a literal of the correct
+ arg.getType() instanceof PointerType and
+ not exists(ArrayAggregateLiteral l |
+ config.hasFlow(DataFlow::exprNode(l), DataFlow::exprNode(arg)) and
+ countElements(l) >= p.getArraySize()
+ )
+ )
+select arg,
+ "The function argument does not have a sufficient number or elements declared in the $@.", p,
+ "parameter"
diff --git a/c/misra/src/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.ql b/c/misra/src/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.ql
new file mode 100644
index 0000000000..3b224544f2
--- /dev/null
+++ b/c/misra/src/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.ql
@@ -0,0 +1,28 @@
+/**
+ * @id c/misra/value-returned-by-a-function-not-used
+ * @name RULE-17-7: Return values should be used or cast to void
+ * @description The value returned by a function having non-void return type shall be used or cast
+ * to void.
+ * @kind problem
+ * @precision very-high
+ * @problem.severity error
+ * @tags external/misra/id/rule-17-7
+ * correctness
+ * external/misra/obligation/required
+ */
+
+import cpp
+import codingstandards.c.misra
+import semmle.code.cpp.dataflow.DataFlow
+
+from Call c
+where
+ not isExcluded(c, Contracts6Package::valueReturnedByAFunctionNotUsedQuery()) and
+ // Calls in `ExprStmt`s indicate that the return value is ignored
+ c.getParent() instanceof ExprStmt and
+ // Ignore calls to void functions or where the return value is cast to `void`
+ not c.getActualType() instanceof VoidType and
+ // Exclude cases where the function call is generated within a macro, as the user of the macro is
+ // not necessarily able to address thoes results
+ not c.isAffectedByMacro()
+select c, "The value returned by this call shall be used or cast to `void`."
diff --git a/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.expected b/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.expected
new file mode 100644
index 0000000000..913f6f1c34
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.expected
@@ -0,0 +1,9 @@
+| test.c:18:6:18:6 | 0 | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
+| test.c:19:6:19:7 | ar | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
+| test.c:21:6:21:9 | ar2p | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
+| test.c:26:9:26:9 | 0 | The function argument does not have a sufficient number or elements declared in the $@. | test.c:2:20:2:21 | ar | parameter |
+| test.c:27:9:27:10 | ar | The function argument does not have a sufficient number or elements declared in the $@. | test.c:2:20:2:21 | ar | parameter |
+| test.c:29:9:29:12 | ar2p | The function argument does not have a sufficient number or elements declared in the $@. | test.c:2:20:2:21 | ar | parameter |
+| test.c:61:6:61:8 | ar2 | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
+| test.c:62:6:62:9 | ar2b | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
+| test.c:63:6:63:9 | ar2p | The function argument does not have a sufficient number or elements declared in the $@. | test.c:1:13:1:14 | ar | parameter |
diff --git a/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.qlref b/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.qlref
new file mode 100644
index 0000000000..41a893a32c
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.qlref
@@ -0,0 +1 @@
+rules/RULE-17-5/ArrayFunctionArgumentNumberOfElements.ql
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-17-5/test.c b/c/misra/test/rules/RULE-17-5/test.c
new file mode 100644
index 0000000000..8e76a55642
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-5/test.c
@@ -0,0 +1,66 @@
+void f1(int ar[3]);
+void f2(int a, int ar[3]);
+void f3(int *ar);
+void f4(int a, int *ar);
+
+void t1() {
+ int *ar;
+
+ int ar2[3] = {1, 2};
+ int *ar2p = ar2;
+
+ int ar3[3] = {1, 2, 3};
+ int *ar3p = ar3;
+
+ int ar4[4] = {1, 2, 3};
+ int *ar4p = ar4;
+
+ f1(0); // NON_COMPLIANT
+ f1(ar); // NON_COMPLIANT
+ f1(ar2); // COMPLIANT
+ f1(ar2p); // NON_COMPLIANT
+ f1(ar3); // COMPLIANT
+ f1(ar3p); // COMPLIANT
+ f1(ar4); // COMPLIANT
+
+ f2(0, 0); // NON_COMPLIANT
+ f2(0, ar); // NON_COMPLIANT
+ f2(0, ar2); // COMPLIANT
+ f2(0, ar2p); // NON_COMPLIANT
+ f2(0, ar3); // COMPLIANT
+ f2(0, ar3p); // COMPLIANT
+ f2(0, ar4); // COMPLIANT
+
+ f3(0); // COMPLIANT
+ f3(ar); // COMPLIANT
+ f3(ar2); // COMPLIANT
+ f3(ar2p); // COMPLIANT
+ f3(ar3); // COMPLIANT
+ f3(ar3p); // COMPLIANT
+ f3(ar4); // COMPLIANT
+
+ f4(0, 0); // COMPLIANT
+ f4(0, ar); // COMPLIANT
+ f4(0, ar2); // COMPLIANT
+ f4(0, ar2p); // COMPLIANT
+ f4(0, ar3); // COMPLIANT
+ f4(0, ar3p); // COMPLIANT
+ f4(0, ar4); // COMPLIANT
+}
+
+void t2() {
+ int ar2[2] = {1, 2};
+ int ar2b[2] = {1, 2, 3};
+ int *ar2p = ar2;
+ int ar3[3];
+ ar3[0] = 1;
+ ar3[1] = 2;
+ ar3[2] = 3;
+ int ar4[4] = {1, 2, 3, 4};
+
+ f1(ar2); // NON_COMPLIANT
+ f1(ar2b); // NON_COMPLIANT
+ f1(ar2p); // NON_COMPLIANT
+ f1(ar3); // COMPLIANT
+ f1(ar4); // COMPLIANT
+}
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.expected b/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.expected
new file mode 100644
index 0000000000..95b54ed874
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.expected
@@ -0,0 +1,2 @@
+| test.c:6:3:6:4 | call to f2 | The value returned by this call shall be used or cast to `void`. |
+| test.c:15:3:15:9 | call to expression | The value returned by this call shall be used or cast to `void`. |
diff --git a/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.qlref b/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.qlref
new file mode 100644
index 0000000000..a365eed3d8
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.qlref
@@ -0,0 +1 @@
+rules/RULE-17-7/ValueReturnedByAFunctionNotUsed.ql
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-17-7/test.c b/c/misra/test/rules/RULE-17-7/test.c
new file mode 100644
index 0000000000..1d31639275
--- /dev/null
+++ b/c/misra/test/rules/RULE-17-7/test.c
@@ -0,0 +1,18 @@
+void f1() {}
+int f2() { return 0; }
+
+int t1() {
+ f1();
+ f2(); // NON_COMPLIANT
+ (void)f2(); // COMPLIANT
+ int a = f2(); // COMPLIANT
+ a = f2(); // COMPLIANT
+
+ void (*fp1)(void) = &f1;
+ int (*fp2)(void) = &f2;
+
+ (*f1)(); // COMPLIANT
+ (*f2)(); // NON_COMPLIANT
+ (void)(*f2)(); // COMPLIANT
+ a = (*f2)(); // COMPLIANT
+}
\ No newline at end of file
diff --git a/cpp/autosar/test/rules/A1-1-1/CStandardLibraryHeadersAreDeprecated.cpp b/cpp/autosar/test/rules/A1-1-1/CStandardLibraryHeadersAreDeprecated.cpp
index b984336e54..a5149ac02a 100644
--- a/cpp/autosar/test/rules/A1-1-1/CStandardLibraryHeadersAreDeprecated.cpp
+++ b/cpp/autosar/test/rules/A1-1-1/CStandardLibraryHeadersAreDeprecated.cpp
@@ -1,5 +1,5 @@
#include // NON_COMPLIANT
-#include // NON_COMPLAINT
+#include // NON_COMPLIANT
#include // NON_COMPLIANT
#include // NON_COMPLIANT
#include // NON_COMPLIANT
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/Contracts6.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/Contracts6.qll
new file mode 100644
index 0000000000..bd897bd79f
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/Contracts6.qll
@@ -0,0 +1,61 @@
+//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/
+import cpp
+import RuleMetadata
+import codingstandards.cpp.exclusions.RuleMetadata
+
+newtype Contracts6Query =
+ TDoNotModifyConstantObjectsQuery() or
+ TArrayFunctionArgumentNumberOfElementsQuery() or
+ TValueReturnedByAFunctionNotUsedQuery()
+
+predicate isContracts6QueryMetadata(Query query, string queryId, string ruleId, string category) {
+ query =
+ // `Query` instance for the `doNotModifyConstantObjects` query
+ Contracts6Package::doNotModifyConstantObjectsQuery() and
+ queryId =
+ // `@id` for the `doNotModifyConstantObjects` query
+ "c/cert/do-not-modify-constant-objects" and
+ ruleId = "EXP40-C" and
+ category = "rule"
+ or
+ query =
+ // `Query` instance for the `arrayFunctionArgumentNumberOfElements` query
+ Contracts6Package::arrayFunctionArgumentNumberOfElementsQuery() and
+ queryId =
+ // `@id` for the `arrayFunctionArgumentNumberOfElements` query
+ "c/misra/array-function-argument-number-of-elements" and
+ ruleId = "RULE-17-5" and
+ category = "advisory"
+ or
+ query =
+ // `Query` instance for the `valueReturnedByAFunctionNotUsed` query
+ Contracts6Package::valueReturnedByAFunctionNotUsedQuery() and
+ queryId =
+ // `@id` for the `valueReturnedByAFunctionNotUsed` query
+ "c/misra/value-returned-by-a-function-not-used" and
+ ruleId = "RULE-17-7" and
+ category = "required"
+}
+
+module Contracts6Package {
+ Query doNotModifyConstantObjectsQuery() {
+ //autogenerate `Query` type
+ result =
+ // `Query` type for `doNotModifyConstantObjects` query
+ TQueryC(TContracts6PackageQuery(TDoNotModifyConstantObjectsQuery()))
+ }
+
+ Query arrayFunctionArgumentNumberOfElementsQuery() {
+ //autogenerate `Query` type
+ result =
+ // `Query` type for `arrayFunctionArgumentNumberOfElements` query
+ TQueryC(TContracts6PackageQuery(TArrayFunctionArgumentNumberOfElementsQuery()))
+ }
+
+ Query valueReturnedByAFunctionNotUsedQuery() {
+ //autogenerate `Query` type
+ result =
+ // `Query` type for `valueReturnedByAFunctionNotUsed` query
+ TQueryC(TContracts6PackageQuery(TValueReturnedByAFunctionNotUsedQuery()))
+ }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
index 3f52afac5f..e427fdef5b 100644
--- a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
@@ -14,6 +14,7 @@ import Contracts2
import Contracts3
import Contracts4
import Contracts5
+import Contracts6
import DeadCode
import Declarations1
import Declarations2
@@ -62,6 +63,7 @@ newtype TCQuery =
TContracts3PackageQuery(Contracts3Query q) or
TContracts4PackageQuery(Contracts4Query q) or
TContracts5PackageQuery(Contracts5Query q) or
+ TContracts6PackageQuery(Contracts6Query q) or
TDeadCodePackageQuery(DeadCodeQuery q) or
TDeclarations1PackageQuery(Declarations1Query q) or
TDeclarations2PackageQuery(Declarations2Query q) or
@@ -110,6 +112,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
isContracts3QueryMetadata(query, queryId, ruleId, category) or
isContracts4QueryMetadata(query, queryId, ruleId, category) or
isContracts5QueryMetadata(query, queryId, ruleId, category) or
+ isContracts6QueryMetadata(query, queryId, ruleId, category) or
isDeadCodeQueryMetadata(query, queryId, ruleId, category) or
isDeclarations1QueryMetadata(query, queryId, ruleId, category) or
isDeclarations2QueryMetadata(query, queryId, ruleId, category) or
diff --git a/cpp/common/test/rules/deleteofpointertoincompleteclass/test.cpp b/cpp/common/test/rules/deleteofpointertoincompleteclass/test.cpp
index 2a5f002c67..c659a87740 100644
--- a/cpp/common/test/rules/deleteofpointertoincompleteclass/test.cpp
+++ b/cpp/common/test/rules/deleteofpointertoincompleteclass/test.cpp
@@ -1,7 +1,7 @@
class A {
class B *impl;
- void test() { delete impl; } // NON_COMPLAINT
+ void test() { delete impl; } // NON_COMPLIANT
};
class D {};
@@ -9,5 +9,5 @@ class D {};
class C {
class D *impl1;
- void test() { delete impl1; } // COMPLAINT
+ void test() { delete impl1; } // COMPLIANT
};
\ No newline at end of file
diff --git a/cpp/common/test/rules/validcontainerelementaccess/test.cpp b/cpp/common/test/rules/validcontainerelementaccess/test.cpp
index 45957ec141..55c94cf8f1 100644
--- a/cpp/common/test/rules/validcontainerelementaccess/test.cpp
+++ b/cpp/common/test/rules/validcontainerelementaccess/test.cpp
@@ -111,7 +111,7 @@ void f11(std::string cs) {
const char *cp = cs.c_str();
const char *cpe = cp + 2;
- while (cp < cpe) { // COMPLAINT
+ while (cp < cpe) { // COMPLIANT
std::string arg(cp); // COMPLIANT
cp += arg.size() + 1;
}
diff --git a/rule_packages/c/Contracts6.json b/rule_packages/c/Contracts6.json
new file mode 100644
index 0000000000..bc707f19f4
--- /dev/null
+++ b/rule_packages/c/Contracts6.json
@@ -0,0 +1,60 @@
+{
+ "CERT-C": {
+ "EXP40-C": {
+ "properties": {
+ "obligation": "rule"
+ },
+ "queries": [
+ {
+ "description": "Do not modify constant objects. This may result in undefined behavior.",
+ "kind": "path-problem",
+ "name": "Do not modify constant objects",
+ "precision": "high",
+ "severity": "error",
+ "short_name": "DoNotModifyConstantObjects",
+ "tags": ["correctness"],
+ "implementation_scope": {
+ "description": "The implementation does not consider pointer aliasing via multiple indirection."
+ }
+ }
+ ],
+ "title": "Do not modify constant objects"
+ }
+ },
+ "MISRA-C-2012": {
+ "RULE-17-5": {
+ "properties": {
+ "obligation": "advisory"
+ },
+ "queries": [
+ {
+ "description": "The function argument corresponding to an array parameter shall have an appropriate number of elements.",
+ "kind": "problem",
+ "name": "An array founction argument shall have an appropriate number of elements",
+ "precision": "high",
+ "severity": "error",
+ "short_name": "ArrayFunctionArgumentNumberOfElements",
+ "tags": ["correctness"]
+ }
+ ],
+ "title": "The function argument corresponding to an array parameter shall have an appropriate number of elements"
+ },
+ "RULE-17-7": {
+ "properties": {
+ "obligation": "required"
+ },
+ "queries": [
+ {
+ "description": "The value returned by a function having non-void return type shall be used or cast to void.",
+ "kind": "problem",
+ "name": "Return values should be used or cast to void",
+ "precision": "very-high",
+ "severity": "error",
+ "short_name": "ValueReturnedByAFunctionNotUsed",
+ "tags": ["correctness"]
+ }
+ ],
+ "title": "The value returned by a function having non-void return type shall be used or cast to void"
+ }
+ }
+}
\ No newline at end of file
diff --git a/rules.csv b/rules.csv
index ca615879f8..d9a3863928 100644
--- a/rules.csv
+++ b/rules.csv
@@ -523,7 +523,7 @@ c,CERT-C,EXP35-C,Yes,Rule,,,Do not modify objects with temporary lifetime,,Inval
c,CERT-C,EXP36-C,Yes,Rule,,,Do not cast pointers into more strictly aligned pointer types,,Pointers3,Medium,
c,CERT-C,EXP37-C,Yes,Rule,,,Call functions with the correct number and type of arguments,,Expressions,Easy,
c,CERT-C,EXP39-C,Yes,Rule,,,Do not access a variable through a pointer of an incompatible type,,Pointers3,Medium,
-c,CERT-C,EXP40-C,Yes,Rule,,,Do not modify constant objects,,Contracts,Medium,
+c,CERT-C,EXP40-C,Yes,Rule,,,Do not modify constant objects,,Contracts6,Hard,
c,CERT-C,EXP42-C,Yes,Rule,,,Do not compare padding data,,Memory2,Medium,
c,CERT-C,EXP43-C,Yes,Rule,,,Avoid undefined behavior when using restrict-qualified pointers,,Pointers3,Medium,
c,CERT-C,EXP44-C,Yes,Rule,,,"Do not rely on side effects in operands to sizeof, _Alignof, or _Generic",M5-3-4,SideEffects1,Medium,
@@ -683,7 +683,7 @@ c,MISRA-C-2012,RULE-11-7,Yes,Required,,,A cast shall not be performed between po
c,MISRA-C-2012,RULE-11-8,Yes,Required,,,A cast shall not remove any const or volatile qualification from the type pointed to by a pointer,,Pointers1,Easy,
c,MISRA-C-2012,RULE-11-9,Yes,Required,,,The macro NULL shall be the only permitted form of integer null pointer constant,,Pointers1,Easy,
c,MISRA-C-2012,RULE-12-1,Yes,Advisory,,,The precedence of operators within expressions should be made explicit,,SideEffects1,Medium,
-c,MISRA-C-2012,RULE-12-2,Yes,Required,,,The right hand operand of a shift operator shall lie in the range zero to one less than the width in bits of the essential type of the left hand operand,,Contracts,Hard,
+c,MISRA-C-2012,RULE-12-2,Yes,Required,,,The right hand operand of a shift operator shall lie in the range zero to one less than the width in bits of the essential type of the left hand operand,,Contracts,Medium,
c,MISRA-C-2012,RULE-12-3,Yes,Advisory,,,The comma operator should not be used,M5-18-1,Banned,Import,
c,MISRA-C-2012,RULE-12-4,Yes,Advisory,,,Evaluation of constant expressions should not lead to unsigned integer wrap-around,INT30-C,Types,Easy,
c,MISRA-C-2012,RULE-12-5,Yes,Mandatory,,,The sizeof operator shall not have an operand which is a function parameter declared as �array of type�,,Types,Medium,
@@ -715,9 +715,9 @@ c,MISRA-C-2012,RULE-17-1,Yes,Required,,,The features of shall not be
c,MISRA-C-2012,RULE-17-2,Yes,Required,,,"Functions shall not call themselves, either directly or indirectly",A7-5-2,Statements,Import,
c,MISRA-C-2012,RULE-17-3,Yes,Mandatory,,,A function shall not be declared implicitly,,Declarations6,Medium,
c,MISRA-C-2012,RULE-17-4,Yes,Mandatory,,,All exit paths from a function with non-void return type shall have an explicit return statement with an expression,MSC52-CPP,Statements,Medium,
-c,MISRA-C-2012,RULE-17-5,Yes,Advisory,,,The function argument corresponding to a parameter declared to have an array type shall have an appropriate number of elements,,Contracts,Hard,
+c,MISRA-C-2012,RULE-17-5,Yes,Advisory,,,The function argument corresponding to a parameter declared to have an array type shall have an appropriate number of elements,,Contracts6,Hard,
c,MISRA-C-2012,RULE-17-6,No,Mandatory,,,The declaration of an array parameter shall not contain the static keyword between the [ ],,,,
-c,MISRA-C-2012,RULE-17-7,Yes,Required,,,The value returned by a function having non-void return type shall be used,A0-1-2,Contracts,Import,
+c,MISRA-C-2012,RULE-17-7,Yes,Required,,,The value returned by a function having non-void return type shall be used,A0-1-2,Contracts6,Easy,
c,MISRA-C-2012,RULE-17-8,Yes,Advisory,,,A function parameter should not be modified,,SideEffects2,Medium,
c,MISRA-C-2012,RULE-18-1,Yes,Required,,,A pointer resulting from arithmetic on a pointer operand shall address an element of the same array as that pointer operand,M5-0-16,Pointers1,Import,
c,MISRA-C-2012,RULE-18-2,Yes,Required,,,Subtraction between pointers shall only be applied to pointers that address elements of the same array,M5-0-17,Pointers1,Import,