Contracts6

.vscode/tasks.json

@@ -193,6 +193,11 @@
                 "Classes",
                 "Comments",
                 "Contracts1",
+                "Contracts2",
+                "Contracts3",
+                "Contracts4",
+                "Contracts5",
+                "Contracts6",
                 "Concurrency",
                 "Concurrency",
                 "Concurrency1",

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).
+
+<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>
+
+
+## Automated Detection
+
+<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>
+
+
+## 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)
+
+<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>
+
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> Subclause 6.7.3, "Type Qualifiers" </td> </tr> </tbody> </table>
+
+
+## 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)

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."

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. |

c/cert/test/rules/EXP40-C/DoNotModifyConstantObjects.qlref

@@ -0,0 +1 @@
+rules/EXP40-C/DoNotModifyConstantObjects.ql

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 <string.h>
+
+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;
+}

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"

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`."