diff --git a/amendments.csv b/amendments.csv
index e4e5fa4144..64d2e2e858 100644
--- a/amendments.csv
+++ b/amendments.csv
@@ -28,23 +28,23 @@ c,MISRA-C-2012,Amendment4,RULE-1-4,Yes,Replace,No,Easy
 c,MISRA-C-2012,Amendment4,RULE-9-1,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Amendment4,RULE-9-2,Yes,Refine,No,Import
 c,MISRA-C-2012,Corrigendum2,DIR-4-10,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-7-4,Yes,Refine,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-7-4,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-8-2,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-8-3,Yes,Refine,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-8-3,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-8-7,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-10-1,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-10-2,Yes,Refine,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-10-2,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-10-3,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-11-3,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-11-6,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-13-2,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-13-6,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-14-3,Yes,Refine,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-14-3,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-15-7,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-17-4,Yes,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-17-5,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-18-1,Yes,Refine,No,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-18-1,Yes,Refine,Yes,Easy
 c,MISRA-C-2012,Corrigendum2,RULE-20-14,No,Clarification,Yes,Import
 c,MISRA-C-2012,Corrigendum2,RULE-21-19,Yes,Clarification,Yes,Import
-c,MISRA-C-2012,Corrigendum2,RULE-21-20,Yes,Refine,No,Easy
-c,MISRA-C-2012,Corrigendum2,RULE-22-9,Yes,Clarification,Yes,Import
\ No newline at end of file
+c,MISRA-C-2012,Corrigendum2,RULE-21-20,Yes,Refine,Yes,Easy
+c,MISRA-C-2012,Corrigendum2,RULE-22-9,Yes,Clarification,Yes,Import
diff --git a/c/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected b/c/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
index 1d487765df..bc471c0dc4 100644
--- a/c/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
+++ b/c/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
@@ -1,5 +1,5 @@
-| test.c:4:13:4:18 | ... + ... | Array pointer p2 points 1 element passed the end of $@. | test.c:2:7:2:8 | l1 | l1 |
-| test.c:5:13:5:18 | ... + ... | Array pointer p3 points 1 element passed the end of $@. | test.c:2:7:2:8 | l1 | l1 |
-| test.c:6:13:6:18 | & ... | Array pointer p4 points 1 element passed the end of $@. | test.c:2:7:2:8 | l1 | l1 |
-| test.c:11:8:11:11 | ... -- | Array pointer p7 points 1 element passed the end of $@. | test.c:2:7:2:8 | l1 | l1 |
-| test.c:12:8:12:9 | p3 | Array pointer p8 points 1 element passed the end of $@. | test.c:2:7:2:8 | l1 | l1 |
+| test.c:4:13:4:18 | ... + ... | Array pointer p2 points 1 element past the end of $@. | test.c:2:7:2:8 | l1 | l1 |
+| test.c:5:13:5:18 | ... + ... | Array pointer p3 points 1 element past the end of $@. | test.c:2:7:2:8 | l1 | l1 |
+| test.c:6:13:6:18 | & ... | Array pointer p4 points 1 element past the end of $@. | test.c:2:7:2:8 | l1 | l1 |
+| test.c:11:8:11:11 | ... -- | Array pointer p7 points 1 element past the end of $@. | test.c:2:7:2:8 | l1 | l1 |
+| test.c:12:8:12:9 | p3 | Array pointer p8 points 1 element past the end of $@. | test.c:2:7:2:8 | l1 | l1 |
diff --git a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll
index 02b8498ecb..de6d43e2c5 100644
--- a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll
+++ b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll
@@ -328,12 +328,14 @@ class EssentialBinaryOperationSubjectToUsualConversions extends EssentialExpr, B
     exists(
       Type leftEssentialType, Type rightEssentialType,
       EssentialTypeCategory leftEssentialTypeCategory,
-      EssentialTypeCategory rightEssentialTypeCategory
+      EssentialTypeCategory rightEssentialTypeCategory, int intTypeSize
     |
       leftEssentialType = getEssentialType(getLeftOperand()) and
       rightEssentialType = getEssentialType(getRightOperand()) and
       leftEssentialTypeCategory = getEssentialTypeCategory(leftEssentialType) and
-      rightEssentialTypeCategory = getEssentialTypeCategory(rightEssentialType)
+      rightEssentialTypeCategory = getEssentialTypeCategory(rightEssentialType) and
+      // For rules around addition/subtraction with char types:
+      intTypeSize = any(IntType i | i.isSigned()).getSize()
     |
       if
         leftEssentialTypeCategory = rightEssentialTypeCategory and
@@ -356,14 +358,18 @@ class EssentialBinaryOperationSubjectToUsualConversions extends EssentialExpr, B
 class EssentialAddExpr extends EssentialBinaryOperationSubjectToUsualConversions, AddExpr {
   override Type getEssentialType() {
     exists(
-      EssentialTypeCategory operandTypeCategory, EssentialTypeCategory otherOperandTypeCategory
+      Type otherOperandType, EssentialTypeCategory operandTypeCategory,
+      EssentialTypeCategory otherOperandTypeCategory, int intTypeSize
     |
       operandTypeCategory = getEssentialTypeCategory(getEssentialType(getAnOperand())) and
-      otherOperandTypeCategory = getEssentialTypeCategory(getEssentialType(getAnOperand()))
+      otherOperandType = getEssentialType(getAnOperand()) and
+      otherOperandTypeCategory = getEssentialTypeCategory(otherOperandType) and
+      intTypeSize = any(IntType i).getSize()
     |
       if
         operandTypeCategory = EssentiallyCharacterType() and
-        otherOperandTypeCategory instanceof EssentiallySignedOrUnsignedType
+        otherOperandTypeCategory instanceof EssentiallySignedOrUnsignedType and
+        otherOperandType.getSize() <= intTypeSize
       then result instanceof PlainCharType
       else result = super.getEssentialType()
     )
@@ -376,15 +382,18 @@ class EssentialAddExpr extends EssentialBinaryOperationSubjectToUsualConversions
 class EssentialSubExpr extends EssentialBinaryOperationSubjectToUsualConversions, SubExpr {
   override Type getEssentialType() {
     exists(
-      EssentialTypeCategory leftEssentialTypeCategory,
-      EssentialTypeCategory rightEssentialTypeCategory
+      EssentialTypeCategory leftEssentialTypeCategory, Type rightEssentialType,
+      EssentialTypeCategory rightEssentialTypeCategory, int intTypeSize
     |
       leftEssentialTypeCategory = getEssentialTypeCategory(getEssentialType(getLeftOperand())) and
-      rightEssentialTypeCategory = getEssentialTypeCategory(getEssentialType(getRightOperand()))
+      rightEssentialType = getEssentialType(getRightOperand()) and
+      rightEssentialTypeCategory = getEssentialTypeCategory(rightEssentialType) and
+      intTypeSize = any(IntType i).getSize()
     |
       if
         leftEssentialTypeCategory = EssentiallyCharacterType() and
-        rightEssentialTypeCategory instanceof EssentiallySignedOrUnsignedType
+        rightEssentialTypeCategory instanceof EssentiallySignedOrUnsignedType and
+        rightEssentialType.getSize() <= intTypeSize
       then result instanceof PlainCharType
       else result = super.getEssentialType()
     )
diff --git a/c/misra/src/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.ql b/c/misra/src/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.ql
index 750e589a1c..0e98c6c570 100644
--- a/c/misra/src/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.ql
+++ b/c/misra/src/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.ql
@@ -32,7 +32,7 @@ where
     // But the overall essential type is not essentially character type
     getEssentialTypeCategory(getEssentialType(addOrSub)) = EssentiallyCharacterType()
     or
-    // Or this is a subtration of one character with another, which is permitted, but produces an integral type
+    // Or this is a subtraction of one character with another, which is permitted, but produces an integral type
     getEssentialTypeCategory(getEssentialType(addOrSub.getLeftOperand())) =
       EssentiallyCharacterType() and
     getEssentialTypeCategory(getEssentialType(addOrSub.getRightOperand())) =
diff --git a/c/misra/test/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.expected b/c/misra/test/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.expected
index 0a5c7ae0bb..a1d3657a1e 100644
--- a/c/misra/test/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.expected
+++ b/c/misra/test/rules/RULE-10-2/AdditionSubtractionOnEssentiallyCharType.expected
@@ -1,15 +1,19 @@
-| test.c:15:3:15:11 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:16:3:16:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:17:3:17:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:18:3:18:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:19:3:19:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:20:3:20:10 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:21:3:21:10 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:27:3:27:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:28:3:28:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:29:3:29:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:30:3:30:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:31:3:31:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:32:3:32:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:33:3:33:10 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
-| test.c:34:3:34:10 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:19:3:19:11 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:20:3:20:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:21:3:21:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:22:3:22:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:23:3:23:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:24:3:24:10 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:25:3:25:10 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:28:3:28:9 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:29:3:29:10 | ... + ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:35:3:35:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:36:3:36:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:37:3:37:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:38:3:38:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:39:3:39:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:40:3:40:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:41:3:41:10 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:42:3:42:10 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:45:3:45:9 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
+| test.c:46:3:46:10 | ... - ... | Expressions of essentially character type shall not be used inappropriately in addition and subtraction operations |
diff --git a/c/misra/test/rules/RULE-10-2/test.c b/c/misra/test/rules/RULE-10-2/test.c
index 186c49226e..1d86013c07 100644
--- a/c/misra/test/rules/RULE-10-2/test.c
+++ b/c/misra/test/rules/RULE-10-2/test.c
@@ -5,6 +5,10 @@ void testRules() {
   enum E1 { A, B, C } e1 = A;
   signed int i = 100;
   unsigned int u = 100;
+  signed short s = 100;
+  unsigned short us = 100;
+  signed long l = 100L;
+  unsigned long ul = 100UL;
   float f = 10.0f;
 
   // Addition cases
@@ -19,8 +23,12 @@ void testRules() {
   b + 'a';   // NON_COMPLIANT
   'a' + e1;  // NON_COMPLIANT
   e1 + 'a';  // NON_COMPLIANT
+  'a' + s;   // COMPLIANT
+  'a' + us;  // COMPLIANT
+  'a' + l;   // NON_COMPLIANT
+  'a' + ul;  // NON_COMPLIANT
 
-  // Subtration cases
+  // Subtraction cases
   'a' - i;   // COMPLIANT
   'a' - u;   // COMPLIANT
   'a' - 'a'; // COMPLIANT
@@ -32,4 +40,8 @@ void testRules() {
   'a' - b;   // NON_COMPLIANT
   e1 - 'a';  // NON_COMPLIANT
   'a' - e1;  // NON_COMPLIANT
+  'a' - s;   // COMPLIANT
+  'a' - us;  // COMPLIANT
+  'a' - l;   // NON_COMPLIANT
+  'a' - ul;  // NON_COMPLIANT
 }
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-14-3/ControllingExprInvariant.expected b/c/misra/test/rules/RULE-14-3/ControllingExprInvariant.expected
index c03c04d6cc..3beb834f84 100644
--- a/c/misra/test/rules/RULE-14-3/ControllingExprInvariant.expected
+++ b/c/misra/test/rules/RULE-14-3/ControllingExprInvariant.expected
@@ -5,3 +5,4 @@
 | test.c:27:10:27:14 | ... < ... | Controlling expression in loop statement has an invariant value. |
 | test.c:37:3:37:6 | 1 | Controlling expression in conditional statement has an invariant value. |
 | test.c:38:3:38:3 | 1 | Controlling expression in conditional statement has an invariant value. |
+| test.c:45:10:45:26 | ... && ... | Controlling expression in loop statement has an invariant value. |
diff --git a/c/misra/test/rules/RULE-14-3/test.c b/c/misra/test/rules/RULE-14-3/test.c
index 38db3e1286..ed8854afd2 100644
--- a/c/misra/test/rules/RULE-14-3/test.c
+++ b/c/misra/test/rules/RULE-14-3/test.c
@@ -37,4 +37,11 @@ void f5(bool b1) {
   true ? 1 : 2; // NON_COMPLIANT
   1 ? 1 : 2;    // NON_COMPLIANT
   b1 ? 1 : 2;   // COMPLIANT
+}
+
+void f6(int p1) {
+  while (p1 < 10 && p1 > 12) { // NON_COMPLIANT[FALSE_NEGATIVE]
+  }
+  while (1 == 0 && p1 > 12) { // NON_COMPLIANT
+  }
 }
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-7-4/StringLiteralAssignedToNonConstChar.expected b/c/misra/test/rules/RULE-7-4/StringLiteralAssignedToNonConstChar.expected
index 46b8e5a47b..208e98f632 100644
--- a/c/misra/test/rules/RULE-7-4/StringLiteralAssignedToNonConstChar.expected
+++ b/c/misra/test/rules/RULE-7-4/StringLiteralAssignedToNonConstChar.expected
@@ -6,3 +6,4 @@
 | test.c:58:5:58:22 | return ... | wchar_t * function w_sample3 is returning a string literal. |
 | test.c:69:3:69:9 | call to sample4 | char * parameter of sample4 is passed a string literal. |
 | test.c:78:3:78:11 | call to w_sample4 | wchar_t * parameter of w_sample4 is passed a string literal. |
+| test.c:91:3:91:11 | call to w_sample7 | char * parameter of w_sample7 is passed a string literal. |
diff --git a/c/misra/test/rules/RULE-7-4/test.c b/c/misra/test/rules/RULE-7-4/test.c
index c178915200..ab7ea21ce9 100644
--- a/c/misra/test/rules/RULE-7-4/test.c
+++ b/c/misra/test/rules/RULE-7-4/test.c
@@ -79,4 +79,16 @@ void w_call45() {
   w_sample5(L"string9"); // COMPLIANT: passing string literal to const char*
 }
 
+void w_sample6(int x, ...) {}
+
+void w_call6() {
+  w_sample6(1, "string10"); // COMPLIANT by first (and only) exception
+}
+
+void w_sample7(char *x, ...) {}
+
+void w_call7() {
+  w_sample7("string11", 1); // NON_COMPLIANT, does not fit exceptional case
+}
+
 int main() { return 0; }
diff --git a/c/misra/test/rules/RULE-8-3/function1.c b/c/misra/test/rules/RULE-8-3/function1.c
index 2072748047..7f42f87f53 100644
--- a/c/misra/test/rules/RULE-8-3/function1.c
+++ b/c/misra/test/rules/RULE-8-3/function1.c
@@ -24,4 +24,8 @@ a f21(wi w, wi h) { // NON_COMPLIANT
 
 void f22(int f22b, int f22a) { // NON_COMPLIANT
   return;
+}
+
+void f23(int f23a) { // COMPLIANT
+  return;
 }
\ No newline at end of file
diff --git a/c/misra/test/rules/RULE-8-3/function2.c b/c/misra/test/rules/RULE-8-3/function2.c
index 979e002466..159dbe105d 100644
--- a/c/misra/test/rules/RULE-8-3/function2.c
+++ b/c/misra/test/rules/RULE-8-3/function2.c
@@ -16,4 +16,6 @@ typedef long a;
 
 extern a f21(wi w, hi h); // NON_COMPLIANT
 
-extern void f22(int f22a, int f22b); // NON_COMPLIANT
\ No newline at end of file
+extern void f22(int f22a, int f22b); // NON_COMPLIANT
+
+extern void f23(int); // COMPLIANT
\ No newline at end of file
diff --git a/change_notes/2025-1-04-misra-c-technical-corrigenda-2.md b/change_notes/2025-1-04-misra-c-technical-corrigenda-2.md
new file mode 100644
index 0000000000..6849951810
--- /dev/null
+++ b/change_notes/2025-1-04-misra-c-technical-corrigenda-2.md
@@ -0,0 +1,12 @@
+ - `RULE-8-3` - `DeclarationsOfAFunctionSameNameAndType.ql`:
+   - Implement new exception, unnamed parameters are not covered by this rule.
+ - `RULE-10-2` - `AdditionSubtractionOnEssentiallyCharType.ql`:
+   - Disallow `+` and `-` operations with an essentially char type and other types larger than int type.
+   - Note, this change affects the essential type of such expressions, which may affect other essential types rules.
+ - `RULE-18-1`, `M5-0-16` - `PointerAndDerivedPointerMustAddressSameArray.ql`, `PointerAndDerivedPointerAccessDifferentArray.ql`:
+   - Treat casts to byte pointers as pointers to arrays of the size of the pointed-to type.
+   - Fix typo in report message, "passed" replaced with "past."
+   - Suppress results where range analysis appears potentially unreliable.
+ - `RULE-21-10`, `RULE-25-5-3`, `ENV34-C` - `CallToSetlocaleInvalidatesOldPointers.ql`, `CallToSetlocaleInvalidatesOldPointersMisra.ql`, `DoNotStorePointersReturnedByEnvFunctions.ql`:
+   - Report usage of returned pointers from `asctime`, `ctime`, during a call to either of the former.
+   - Report usage of returned pointers from `gmtime`, `localtime`, during a call to either of the former.
\ No newline at end of file
diff --git a/cpp/common/src/codingstandards/cpp/Compatible.qll b/cpp/common/src/codingstandards/cpp/Compatible.qll
index 0f6e2108ff..d2dbc55778 100644
--- a/cpp/common/src/codingstandards/cpp/Compatible.qll
+++ b/cpp/common/src/codingstandards/cpp/Compatible.qll
@@ -21,10 +21,10 @@ predicate parameterTypesIncompatible(FunctionDeclarationEntry f1, FunctionDeclar
 
 predicate parameterNamesIncompatible(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
   f1.getDeclaration() = f2.getDeclaration() and
-  exists(ParameterDeclarationEntry p1, ParameterDeclarationEntry p2, int i |
-    p1 = f1.getParameterDeclarationEntry(i) and
-    p2 = f2.getParameterDeclarationEntry(i)
+  exists(string p1Name, string p2Name, int i |
+    p1Name = f1.getParameterDeclarationEntry(i).getName() and
+    p2Name = f2.getParameterDeclarationEntry(i).getName()
   |
-    not p1.getName() = p2.getName()
+    not p1Name = p2Name
   )
 }
diff --git a/cpp/common/src/codingstandards/cpp/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.qll b/cpp/common/src/codingstandards/cpp/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.qll
index 57b4eb0bfb..5d3a7e1cda 100644
--- a/cpp/common/src/codingstandards/cpp/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.qll
+++ b/cpp/common/src/codingstandards/cpp/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.qll
@@ -7,20 +7,133 @@
 import cpp
 import codingstandards.cpp.Customizations
 import codingstandards.cpp.Exclusions
-import semmle.code.cpp.dataflow.DataFlow
+import semmle.code.cpp.dataflow.new.DataFlow
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
+import codeql.util.Boolean
 
 abstract class DoNotUsePointerArithmeticToAddressDifferentArraysSharedQuery extends Query { }
 
 Query getQuery() { result instanceof DoNotUsePointerArithmeticToAddressDifferentArraysSharedQuery }
 
+/**
+ * A `VariableAccess` of a variable that is an array, or a pointer type casted to a byte pointer.
+ */
+abstract class ArrayLikeAccess extends Expr {
+  abstract Element getElement();
+
+  abstract string getName();
+
+  abstract int getSize();
+
+  abstract DataFlow::Node getNode();
+}
+
+/**
+ * A `VariableAccess` of a variable that is an array.
+ */
+class ArrayVariableAccess extends ArrayLikeAccess, VariableAccess {
+  int size;
+
+  ArrayVariableAccess() { size = getType().(ArrayType).getArraySize() }
+
+  override Variable getElement() { result = getTarget() }
+
+  override string getName() { result = getElement().getName() }
+
+  override int getSize() { result = size }
+
+  override DataFlow::Node getNode() { result.asExpr() = this }
+}
+
+/**
+ * Get the size of the object pointed to by a type (pointer or array).
+ *
+ * Depth of type unwrapping depends on the type. Pointer will be dereferenced only once: the element
+ * size of `T*` is `sizeof(T)` while the element size of `T**` is `sizeof(T*)`. However, array types
+ * will be deeply unwrapped, as the pointed to size of `T[][]` is `sizeof(T)`. These processes
+ * interact, so the element size of a pointer to an array of `T` has an element size of `sizeof(T)`
+ * and not `sizeof(T[length])`.
+ */
+int elementSize(Type type, Boolean deref) {
+  if type instanceof ArrayType
+  then result = elementSize(type.(ArrayType).getBaseType(), false)
+  else
+    if deref = true and type instanceof PointerType
+    then result = elementSize(type.(PointerType).getBaseType(), false)
+    else result = type.getSize()
+}
+
+/**
+ * A pointer type casted to a byte pointer, which is effectively a pointer to a byte array whose
+ * length depends on `elementSize()` of the original pointed-to type.
+ */
+class CastedToBytePointer extends ArrayLikeAccess, Conversion {
+  /** The sizeof() the pointed-to type */
+  int size;
+
+  CastedToBytePointer() {
+    getType().(PointerType).getBaseType().getSize() = 1 and
+    size = elementSize(getExpr().getType(), true) and
+    size > 1
+  }
+
+  override Element getElement() { result = this }
+
+  override string getName() { result = "cast to byte pointer" }
+
+  override int getSize() { result = size }
+
+  override DataFlow::Node getNode() {
+    // Carefully avoid use-use flow, which would mean any later usage of the original pointer value
+    // after the cast would be considered a usage of the byte pointer value.
+    //
+    // To fix this, we currently assume the value is assigned to a variable, and find that variable
+    // with `.asDefinition()` like so:
+    exists(DataFlow::Node conversion |
+      conversion.asConvertedExpr() = this and
+      result.asDefinition() = conversion.asExpr()
+    )
+  }
+}
+
+predicate pointerRecastBarrier(DataFlow::Node barrier) {
+  // Casting to a differently sized pointer
+  exists(CStyleCast cast, Expr casted |
+    cast.getExpr() = casted and casted = barrier.asConvertedExpr()
+  |
+    not casted.getType().(PointerType).getBaseType().getSize() =
+      cast.getType().(PointerType).getBaseType().getSize()
+  )
+}
+
+/**
+ * A data-flow configuration that tracks access to an array to type to an array index expression.
+ * This is used to determine possible pointer to array creations.
+ */
+module ByteArrayToArrayExprConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { exists(CastedToBytePointer a | a.getNode() = source) }
+
+  predicate isBarrier(DataFlow::Node barrier) {
+    // Casting to a differently sized pointer invalidates this analysis.
+    pointerRecastBarrier(barrier)
+  }
+
+  predicate isSink(DataFlow::Node sink) { exists(ArrayExpr c | c.getArrayBase() = sink.asExpr()) }
+}
+
+module BytePointerToArrayExprFlow = DataFlow::Global<ByteArrayToArrayExprConfig>;
+
 /**
  * A data-flow configuration that tracks access to an array to type to an array index expression.
  * This is used to determine possible pointer to array creations.
  */
 module ArrayToArrayExprConfig implements DataFlow::ConfigSig {
-  predicate isSource(DataFlow::Node source) {
-    source.asExpr().(VariableAccess).getType() instanceof ArrayType
+  predicate isSource(DataFlow::Node source) { exists(ArrayVariableAccess a | a.getNode() = source) }
+
+  predicate isBarrier(DataFlow::Node barrier) {
+    // Casting to a differently sized pointer invalidates this analysis.
+    pointerRecastBarrier(barrier)
   }
 
   predicate isSink(DataFlow::Node sink) { exists(ArrayExpr c | c.getArrayBase() = sink.asExpr()) }
@@ -28,32 +141,39 @@ module ArrayToArrayExprConfig implements DataFlow::ConfigSig {
 
 module ArrayToArrayExprFlow = DataFlow::Global<ArrayToArrayExprConfig>;
 
-/** Holds if the address taken expression `addressOf` takes the address of an array element at `index` of `array` with size `arraySize`. */
-predicate pointerOperandCreation(AddressOfExpr addressOf, Variable array, int arraySize, int index) {
-  arraySize = array.getType().(ArrayType).getArraySize() and
-  exists(ArrayExpr ae |
-    ArrayToArrayExprFlow::flow(DataFlow::exprNode(array.getAnAccess()),
-      DataFlow::exprNode(ae.getArrayBase())) and
-    index = lowerBound(ae.getArrayOffset().getFullyConverted()) and
+/** Holds if the address taken expression `addressOf` takes the address of an array element at `index` of `array`. */
+predicate pointerOperandCreation(AddressOfExpr addressOf, ArrayLikeAccess array, int index) {
+  exists(ArrayExpr ae, Expr arrayOffset |
+    (
+      ArrayToArrayExprFlow::flow(array.getNode(), DataFlow::exprNode(ae.getArrayBase())) and
+      array instanceof ArrayVariableAccess
+      or
+      // Since casts can occur in the middle of flow, barriers are not perfect for modeling the
+      // desired behavior. Handle casts to byte pointers as sources in a separate flow analysis.
+      BytePointerToArrayExprFlow::flow(array.getNode(), DataFlow::exprNode(ae.getArrayBase())) and
+      // flow() may hold for `ArrayVariableAccess` in the above, even though they aren't sources
+      array instanceof CastedToBytePointer
+    ) and
+    arrayOffset = ae.getArrayOffset().getFullyConverted() and
+    index = lowerBound(arrayOffset) and
+    // This case typically indicates range analysis has gone wrong:
+    not index = exprMaxVal(arrayOffset) and
     addressOf.getOperand() = ae
   )
 }
 
 /** A variable that points to an element of an array. */
 class PointerOperand extends Variable {
-  Variable array;
-  int arraySize;
+  ArrayLikeAccess array;
   int index;
   AddressOfExpr source;
 
   PointerOperand() {
-    pointerOperandCreation(source, array, arraySize, index) and
+    pointerOperandCreation(source, array, index) and
     this.getAnAssignedValue() = source
   }
 
-  Variable getArray() { result = array }
-
-  int getArraySize() { result = arraySize }
+  ArrayLikeAccess getArray() { result = array }
 
   int getIndex() { result = index }
 
@@ -111,9 +231,7 @@ class DerivedArrayPointer extends Variable {
 
   DerivedArrayPointer() { derivedPointer(this, source, operand, index) }
 
-  Variable getArray() { result = operand.getArray() }
-
-  int getArraySize() { result = operand.getArraySize() }
+  ArrayLikeAccess getArray() { result = operand.getArray() }
 
   int getIndex() { result = index }
 
@@ -131,15 +249,10 @@ class DerivedArrayPointerOrPointerOperand extends Variable {
     this instanceof PointerOperand
   }
 
-  Variable getArray() {
+  ArrayLikeAccess getArray() {
     result = this.(DerivedArrayPointer).getArray() or result = this.(PointerOperand).getArray()
   }
 
-  int getArraySize() {
-    result = this.(DerivedArrayPointer).getArraySize() or
-    result = this.(PointerOperand).getArraySize()
-  }
-
   int getIndex() {
     result = this.(DerivedArrayPointer).getIndex() or result = this.(PointerOperand).getIndex()
   }
@@ -149,14 +262,16 @@ class DerivedArrayPointerOrPointerOperand extends Variable {
   }
 }
 
-query predicate problems(Expr arrayPointerCreation, string message, Variable array, string arrayName) {
+query predicate problems(Expr arrayPointerCreation, string message, Element array, string arrayName) {
   not isExcluded(arrayPointerCreation, getQuery()) and
   exists(
     DerivedArrayPointerOrPointerOperand derivedArrayPointerOrPointerOperand, int index,
-    int arraySize, int difference, string denomination
+    ArrayLikeAccess arrayAccess, int arraySize, int difference, string denomination
   |
-    array = derivedArrayPointerOrPointerOperand.getArray() and
-    arraySize = derivedArrayPointerOrPointerOperand.getArraySize() and
+    arrayAccess = derivedArrayPointerOrPointerOperand.getArray() and
+    array = arrayAccess.getElement() and
+    arrayName = arrayAccess.getName() and
+    arraySize = arrayAccess.getSize() and
     index = derivedArrayPointerOrPointerOperand.getIndex() and
     arrayPointerCreation = derivedArrayPointerOrPointerOperand.getSource() and
     difference = index - arraySize and
@@ -173,7 +288,6 @@ query predicate problems(Expr arrayPointerCreation, string message, Variable arr
     ) and
     message =
       "Array pointer " + derivedArrayPointerOrPointerOperand.getName() + " points " +
-        (index - arraySize).toString() + " " + denomination + " passed the end of $@."
-  ) and
-  arrayName = array.getName()
+        difference.toString() + " " + denomination + " past the end of $@."
+  )
 }
diff --git a/cpp/common/src/codingstandards/cpp/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.qll b/cpp/common/src/codingstandards/cpp/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.qll
index 3949ff50a8..0f4a98cf6f 100644
--- a/cpp/common/src/codingstandards/cpp/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.qll
+++ b/cpp/common/src/codingstandards/cpp/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.qll
@@ -45,6 +45,12 @@ predicate incompatibleFunctions(GetenvFunction f1, GetenvFunction f2) {
   or
   f1.getName() = ["setlocale", "localeconv"] and
   f2.getName() = ["setlocale", "localeconv"]
+  or
+  f1.getName() = ["asctime", "ctime"] and
+  f2.getName() = ["asctime", "ctime"]
+  or
+  f1.getName() = ["gmtime", "localtime"] and
+  f2.getName() = ["gmtime", "localtime"]
 }
 
 query predicate problems(
diff --git a/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected b/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
index fa181755e8..31ff47e55c 100644
--- a/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
+++ b/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/DoNotUsePointerArithmeticToAddressDifferentArrays.expected
@@ -1,5 +1,8 @@
-| test.cpp:4:13:4:18 | ... + ... | Array pointer p2 points 1 element passed the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
-| test.cpp:5:13:5:18 | ... + ... | Array pointer p3 points 1 element passed the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
-| test.cpp:6:13:6:18 | & ... | Array pointer p4 points 1 element passed the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
-| test.cpp:11:8:11:11 | ... -- | Array pointer p7 points 1 element passed the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
-| test.cpp:12:8:12:9 | p3 | Array pointer p8 points 1 element passed the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:4:13:4:18 | ... + ... | Array pointer p2 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:5:13:5:18 | ... + ... | Array pointer p3 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:6:13:6:18 | & ... | Array pointer p4 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:11:8:11:11 | ... -- | Array pointer p7 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:12:8:12:9 | p3 | Array pointer p8 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:25:15:25:21 | & ... | Array pointer p14 points 1 element past the end of $@. | test.cpp:2:7:2:8 | l1 | l1 |
+| test.cpp:30:15:30:21 | & ... | Array pointer p17 points 1 element past the end of $@. | test.cpp:28:24:28:42 | (unsigned char *)... | cast to byte pointer |
+| test.cpp:35:15:35:21 | & ... | Array pointer p20 points 1 element past the end of $@. | test.cpp:33:24:33:43 | (unsigned char *)... | cast to byte pointer |
diff --git a/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/test.cpp b/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/test.cpp
index c1032ee735..d9874bfb29 100644
--- a/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/test.cpp
+++ b/cpp/common/test/rules/donotusepointerarithmetictoaddressdifferentarrays/test.cpp
@@ -17,4 +17,37 @@ void f1() {
       3 + p1; // COMPLIANT - points to an element on beyond the end of the array
   int *p11 =
       &l1[3]; // COMPLIANT - points to an element on beyond the end of the array
+
+  // Casting to a pointer to a type of the same size doesn't invalidate the
+  // analysis
+  unsigned int *p12 = (unsigned int *)l1;
+  void *p13 = &p12[3]; // COMPLIANT
+  void *p14 = &p12[4]; // NON_COMPLIANT
+
+  // Casting to a char* is effectively a new array of length sizeof(T)
+  unsigned char *p15 = (unsigned char *)l1;
+  void *p16 = &p15[4]; // COMPLIANT
+  void *p17 = &p15[5]; // NON_COMPLIANT
+
+  long l2[3];
+  unsigned char *p18 = (unsigned char *)&l2;
+  void *p19 = &p18[8]; // COMPLIANT
+  void *p20 = &p18[9]; // NON_COMPLIANT
+
+  // Casting to a pointer to a differently sized type that isn't char
+  // invalidates analysis
+  long *p21 = (long *)&l1;
+  void *p22 = &p21[0];   // COMPLIANT
+  void *p23 = &p21[100]; // NON_COMPLIANT[FALSE_NEGATIVE]
+
+  // Casting a byte pointer to a differently sized type that isn't char
+  // invalidates analysis
+  long *p24 = (long *)p15;
+  void *p25 = &p24[0];   // COMPLIANT
+  void *p26 = &p24[100]; // NON_COMPLIANT[FALSE_NEGATIVE]
+
+  // Void pointers have size zero and can't be analyzed.
+  void *p27 = 0;
+  unsigned char *p28 = (unsigned char *)p27;
+  void *p29 = &p28[100]; // COMPLIANT
 }
\ No newline at end of file
diff --git a/cpp/common/test/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.expected b/cpp/common/test/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.expected
index 9a39d3a88d..36c66a94fe 100644
--- a/cpp/common/test/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.expected
+++ b/cpp/common/test/rules/invalidatedenvstringpointers/InvalidatedEnvStringPointers.expected
@@ -4,3 +4,8 @@
 | test.cpp:165:14:165:26 | tmpvar_global | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:157:19:157:24 | call to getenv | call to getenv | test.cpp:161:20:161:25 | call to getenv | call to getenv |
 | test.cpp:188:18:188:18 | r | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:185:7:185:15 | call to setlocale | call to setlocale | test.cpp:187:8:187:17 | call to localeconv | call to localeconv |
 | test.cpp:208:10:208:15 | tmpvar | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:202:12:202:17 | call to getenv | call to getenv | test.cpp:206:3:206:8 | call to f11fun | call to f11fun |
+| test.cpp:216:16:216:17 | r1 | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:214:14:214:18 | call to ctime | call to ctime | test.cpp:215:3:215:9 | call to asctime | call to asctime |
+| test.cpp:226:16:226:17 | r1 | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:222:14:222:18 | call to ctime | call to ctime | test.cpp:225:14:225:20 | call to asctime | call to asctime |
+| test.cpp:231:16:231:17 | r2 | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:225:14:225:20 | call to asctime | call to asctime | test.cpp:229:8:229:12 | call to ctime | call to ctime |
+| test.cpp:240:16:240:17 | r1 | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:236:19:236:27 | call to localtime | call to localtime | test.cpp:239:19:239:24 | call to gmtime | call to gmtime |
+| test.cpp:245:16:245:17 | r2 | This pointer was returned by a $@ and may have been overwritten by the susequent $@. | test.cpp:239:19:239:24 | call to gmtime | call to gmtime | test.cpp:243:8:243:16 | call to localtime | call to localtime |
diff --git a/cpp/common/test/rules/invalidatedenvstringpointers/test.cpp b/cpp/common/test/rules/invalidatedenvstringpointers/test.cpp
index 74e3d1b8f5..920d97c657 100644
--- a/cpp/common/test/rules/invalidatedenvstringpointers/test.cpp
+++ b/cpp/common/test/rules/invalidatedenvstringpointers/test.cpp
@@ -207,3 +207,40 @@ void f11(void) {
 
   printf(tmpvar); // NON_COMPLIANT
 }
+
+void f12(void) {
+  time_t rawtime;
+  time(&rawtime);
+  char *r1 = ctime(&rawtime);
+  asctime(localtime(&rawtime));
+  printf("%s", r1); // NON_COMPLIANT
+}
+
+void f13(void) {
+  time_t rawtime;
+  time(&rawtime);
+  char *r1 = ctime(&rawtime);
+  printf("%s", r1); // COMPLIANT
+
+  char *r2 = asctime(localtime(&rawtime));
+  printf("%s", r1); // NON_COMPLIANT
+  printf("%s", r2); // COMPLIANT
+
+  r1 = ctime(&rawtime);
+  printf("%s", r1); // COMPLIANT
+  printf("%s", r2); // NON_COMPLIANT
+}
+
+void f14(void) {
+  time_t rawtime;
+  struct tm *r1 = localtime(&rawtime);
+  printf("%d", r1->tm_year); // COMPLIANT
+
+  struct tm *r2 = gmtime(&rawtime);
+  printf("%s", r1->tm_year); // NON_COMPLIANT
+  printf("%s", r2->tm_year); // COMPLIANT
+
+  r1 = localtime(&rawtime);
+  printf("%s", r1->tm_year); // COMPLIANT
+  printf("%s", r2->tm_year); // NON_COMPLIANT
+}
\ No newline at end of file
diff --git a/rule_packages/c/Statements5.json b/rule_packages/c/Statements5.json
index 329819b61f..03380f4897 100644
--- a/rule_packages/c/Statements5.json
+++ b/rule_packages/c/Statements5.json
@@ -20,6 +20,9 @@
           ]
         }
       ],
+      "implementation_scope": {
+        "description": "Not all invariant logical expressions which contain dynamic values are detected to be invariant, for instance, `x < 3 && x > 5` where x does not have a statically known value."
+      },
       "title": "Controlling expressions shall not be invariant"
     },
     "RULE-15-5": {