diff --git a/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.md b/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.md
new file mode 100644
index 0000000000..d57756b4b5
--- /dev/null
+++ b/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.md
@@ -0,0 +1,249 @@
+# INT30-C: Ensure that unsigned integer operations do not wrap
+
+This query implements the CERT-C rule INT30-C:
+
+> Ensure that unsigned integer operations do not wrap
+
+
+## Description
+
+The C Standard, 6.2.5, paragraph 9 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)\], states
+
+> A computation involving unsigned operands can never overflow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type.
+
+
+This behavior is more informally called [unsigned integer wrapping](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-unsignedintegerwrapping). Unsigned integer operations can wrap if the resulting value cannot be represented by the underlying representation of the integer. The following table indicates which operators can result in wrapping:
+
+<table> <tbody> <tr> <th> Operator </th> <th> Wrap </th> <th> Operator </th> <th> Wrap </th> <th> Operator </th> <th> Wrap </th> <th> Operator </th> <th> Wrap </th> </tr> <tr> <td> <code><a>+</a></code> </td> <td> Yes </td> <td> <code><a>-=</a></code> </td> <td> Yes </td> <td> <code><a>&lt;&lt;</a></code> </td> <td> Yes </td> <td> <code>&lt;</code> </td> <td> No </td> </tr> <tr> <td> <code><a>-</a></code> </td> <td> Yes </td> <td> <code><a>\*=</a></code> </td> <td> Yes </td> <td> <code>&gt;&gt;</code> </td> <td> No </td> <td> <code>&gt;</code> </td> <td> No </td> </tr> <tr> <td> <code><a>\*</a></code> </td> <td> Yes </td> <td> <code>/=</code> </td> <td> No </td> <td> <code>&amp;</code> </td> <td> No </td> <td> <code>&gt;=</code> </td> <td> No </td> </tr> <tr> <td> <code>/</code> </td> <td> No </td> <td> <code>%=</code> </td> <td> No </td> <td> <code>|</code> </td> <td> No </td> <td> <code>&lt;=</code> </td> <td> No </td> </tr> <tr> <td> <code>%</code> </td> <td> No </td> <td> <code><a>&lt;&lt;=</a></code> </td> <td> Yes </td> <td> <code>^</code> </td> <td> No </td> <td> <code>==</code> </td> <td> No </td> </tr> <tr> <td> <code>++</code> </td> <td> Yes </td> <td> <code>&gt;&gt;=</code> </td> <td> No </td> <td> <code>~</code> </td> <td> No </td> <td> <code>!=</code> </td> <td> No </td> </tr> <tr> <td> <code>--</code> </td> <td> Yes </td> <td> <code>&amp;=</code> </td> <td> No </td> <td> <code>!</code> </td> <td> No </td> <td> <code>&amp;&amp;</code> </td> <td> No </td> </tr> <tr> <td> <code>=</code> </td> <td> No </td> <td> <code>|=</code> </td> <td> No </td> <td> <code>un +</code> </td> <td> No </td> <td> <code>||</code> </td> <td> No </td> </tr> <tr> <td> <code><a>+=</a></code> </td> <td> Yes </td> <td> <code>^=</code> </td> <td> No </td> <td> <code>un -</code> </td> <td> Yes </td> <td> <code>?:</code> </td> <td> No </td> </tr> </tbody> </table>
+The following sections examine specific operations that are susceptible to unsigned integer wrap. When operating on integer types with less precision than `int`, integer promotions are applied. The usual arithmetic conversions may also be applied to (implicitly) convert operands to equivalent types before arithmetic operations are performed. Programmers should understand integer conversion rules before trying to implement secure arithmetic operations. (See [INT02-C. Understand integer conversion rules](https://wiki.sei.cmu.edu/confluence/display/c/INT02-C.+Understand+integer+conversion+rules).)
+
+
+Integer values must not be allowed to wrap, especially if they are used in any of the following ways:
+
+* Integer operands of any pointer arithmetic, including array indexing
+* The assignment expression for the declaration of a variable length array
+* The postfix expression preceding square brackets `[]` or the expression in square brackets `[]` of a subscripted designation of an element of an array object
+* Function arguments of type `size_t` or `rsize_t` (for example, an argument to a memory allocation function)
+* In security-critical code
+The C Standard defines arithmetic on atomic integer types as read-modify-write operations with the same representation as regular integer types. As a result, wrapping of atomic unsigned integers is identical to regular unsigned integers and should also be prevented or detected.
+
+## Addition
+
+Addition is between two operands of arithmetic type or between a pointer to an object type and an integer type. This rule applies only to addition between two operands of arithmetic type. (See [ARR37-C. Do not add or subtract an integer to a pointer to a non-array object](https://wiki.sei.cmu.edu/confluence/display/c/ARR37-C.+Do+not+add+or+subtract+an+integer+to+a+pointer+to+a+non-array+object) and [ARR30-C. Do not form or use out-of-bounds pointers or array subscripts](https://wiki.sei.cmu.edu/confluence/display/c/ARR30-C.+Do+not+form+or+use+out-of-bounds+pointers+or+array+subscripts).)
+
+Incrementing is equivalent to adding 1.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in an unsigned integer wrap during the addition of the unsigned operands `ui_a` and `ui_b`. If this behavior is [unexpected](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-unexpectedbehavior), the resulting value may be used to allocate insufficient memory for a subsequent operation or in some other manner that can lead to an exploitable [vulnerability](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability).
+
+```cpp
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int usum = ui_a + ui_b;
+  /* ... */
+}
+```
+**Compliant Solution (Precondition Test)**
+
+This compliant solution performs a precondition test of the operands of the addition to guarantee there is no possibility of unsigned wrap:
+
+```cpp
+#include <limits.h>
+ 
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int usum;
+  if (UINT_MAX - ui_a < ui_b) {
+    /* Handle error */
+  } else {
+    usum = ui_a + ui_b;
+  }
+  /* ... */
+}
+```
+**Compliant Solution (Postcondition Test)**
+
+This compliant solution performs a postcondition test to ensure that the result of the unsigned addition operation `usum` is not less than the first operand:
+
+```cpp
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int usum = ui_a + ui_b;
+  if (usum < ui_a) {
+    /* Handle error */
+  }
+  /* ... */
+}
+```
+
+## Subtraction
+
+Subtraction is between two operands of arithmetic type, two pointers to qualified or unqualified versions of compatible object types, or a pointer to an object type and an integer type. This rule applies only to subtraction between two operands of arithmetic type. (See [ARR36-C. Do not subtract or compare two pointers that do not refer to the same array](https://wiki.sei.cmu.edu/confluence/display/c/ARR36-C.+Do+not+subtract+or+compare+two+pointers+that+do+not+refer+to+the+same+array), [ARR37-C. Do not add or subtract an integer to a pointer to a non-array object](https://wiki.sei.cmu.edu/confluence/display/c/ARR37-C.+Do+not+add+or+subtract+an+integer+to+a+pointer+to+a+non-array+object), and [ARR30-C. Do not form or use out-of-bounds pointers or array subscripts](https://wiki.sei.cmu.edu/confluence/display/c/ARR30-C.+Do+not+form+or+use+out-of-bounds+pointers+or+array+subscripts) for information about pointer subtraction.)
+
+Decrementing is equivalent to subtracting 1.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in an unsigned integer wrap during the subtraction of the unsigned operands `ui_a` and `ui_b`. If this behavior is unanticipated, it may lead to an exploitable [vulnerability](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability).
+
+```cpp
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int udiff = ui_a - ui_b;
+  /* ... */
+}
+```
+**Compliant Solution (Precondition Test)**
+
+This compliant solution performs a precondition test of the unsigned operands of the subtraction operation to guarantee there is no possibility of unsigned wrap:
+
+```cpp
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int udiff;
+  if (ui_a < ui_b){
+    /* Handle error */
+  } else {
+    udiff = ui_a - ui_b;
+  }
+  /* ... */
+}
+```
+**Compliant Solution (Postcondition Test)**
+
+This compliant solution performs a postcondition test that the result of the unsigned subtraction operation `udiff` is not greater than the minuend:
+
+```cpp
+void func(unsigned int ui_a, unsigned int ui_b) {
+  unsigned int udiff = ui_a - ui_b;
+  if (udiff > ui_a) {
+    /* Handle error */
+  }
+  /* ... */
+}
+```
+
+## Multiplication
+
+Multiplication is between two operands of arithmetic type.
+
+**Noncompliant Code Example**
+
+The Mozilla Foundation Security Advisory 2007-01 describes a heap buffer overflow vulnerability in the Mozilla Scalable Vector Graphics (SVG) viewer resulting from an unsigned integer wrap during the multiplication of the `signed int` value `pen->num_vertices` and the `size_t` value `sizeof(cairo_pen_vertex_t)` \[[VU\#551436](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-VU551436)\]. The `signed int` operand is converted to `size_t` prior to the multiplication operation so that the multiplication takes place between two `size_t` integers, which are unsigned. (See [INT02-C. Understand integer conversion rules](https://wiki.sei.cmu.edu/confluence/display/c/INT02-C.+Understand+integer+conversion+rules).)
+
+```cpp
+pen->num_vertices = _cairo_pen_vertices_needed(
+  gstate->tolerance, radius, &gstate->ctm
+);
+pen->vertices = malloc(
+  pen->num_vertices * sizeof(cairo_pen_vertex_t)
+);
+
+```
+The unsigned integer wrap can result in allocating memory of insufficient size.
+
+**Compliant Solution**
+
+This compliant solution tests the operands of the multiplication to guarantee that there is no unsigned integer wrap:
+
+```cpp
+pen->num_vertices = _cairo_pen_vertices_needed(
+  gstate->tolerance, radius, &gstate->ctm
+);
+
+if (pen->num_vertices > SIZE_MAX / sizeof(cairo_pen_vertex_t)) {
+  /* Handle error */
+}
+pen->vertices = malloc(
+  pen->num_vertices * sizeof(cairo_pen_vertex_t)
+);
+
+```
+
+## Exceptions
+
+**INT30-C-EX1:** Unsigned integers can exhibit modulo behavior (wrapping) when necessary for the proper execution of the program. It is recommended that the variable declaration be clearly commented as supporting modulo behavior and that each operation on that integer also be clearly commented as supporting modulo behavior.
+
+**INT30-C-EX2:** Checks for wraparound can be omitted when it can be determined at compile time that wraparound will not occur. As such, the following operations on unsigned integers require no validation:
+
+* Operations on two compile-time constants
+* Operations on a variable and 0 (except division or remainder by 0)
+* Subtracting any variable from its type's maximum; for example, any `unsigned int` may safely be subtracted from `UINT_MAX`
+* Multiplying any variable by 1
+* Division or remainder, as long as the divisor is nonzero
+* Right-shifting any type maximum by any number no larger than the type precision; for example, `UINT_MAX >> x` is valid as long as `0 <= x < 32` (assuming that the precision of `unsigned int` is 32 bits)
+**INT30-C-EX3.** The left-shift operator takes two operands of integer type. Unsigned left shift `<<` can exhibit modulo behavior (wrapping). This exception is provided because of common usage, because this behavior is usually expected by the programmer, and because the behavior is well defined. For examples of usage of the left-shift operator, see [INT34-C. Do not shift an expression by a negative number of bits or by greater than or equal to the number of bits that exist in the operand](https://wiki.sei.cmu.edu/confluence/display/c/INT34-C.+Do+not+shift+an+expression+by+a+negative+number+of+bits+or+by+greater+than+or+equal+to+the+number+of+bits+that+exist+in+the+operand).
+
+## Risk Assessment
+
+Integer wrap can lead to buffer overflows and the execution of arbitrary code by an attacker.
+
+<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> INT30-C </td> <td> High </td> <td> Likely </td> <td> High </td> <td> <strong>P9</strong> </td> <td> <strong>L2</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>integer-overflow</strong> </td> <td> Fully checked </td> </tr> <tr> <td> <a> Axivion Bauhaus Suite </a> </td> <td> 7.2.0 </td> <td> <strong>CertC-INT30</strong> </td> <td> Implemented </td> </tr> <tr> <td> <a> CodeSonar </a> </td> <td> 7.2p0 </td> <td> <strong>ALLOC.SIZE.ADDOFLOW</strong> <strong>ALLOC.SIZE.IOFLOW</strong> <strong>ALLOC.SIZE.MULOFLOW</strong> <strong>ALLOC.SIZE.SUBUFLOW</strong> <strong>MISC.MEM.SIZE.ADDOFLOW</strong> <strong>MISC.MEM.SIZE.BAD</strong> <strong>MISC.MEM.SIZE.MULOFLOW</strong> <strong>MISC.MEM.SIZE.SUBUFLOW</strong> </td> <td> Addition overflow of allocation size Integer overflow of allocation size Multiplication overflow of allocation size Subtraction underflow of allocation size Addition overflow of size Unreasonable size argument Multiplication overflow of size Subtraction underflow of size </td> </tr> <tr> <td> <a> Compass/ROSE </a> </td> <td> </td> <td> </td> <td> Can detect violations of this rule by ensuring that operations are checked for overflow before being performed (Be mindful of exception INT30-EX2 because it excuses many operations from requiring <a> validation </a> , including all the operations that would validate a potentially dangerous operation. For instance, adding two <code>unsigned int</code> s together requires validation involving subtracting one of the numbers from <code>UINT_MAX</code> , which itself requires no validation because it cannot wrap.) </td> </tr> <tr> <td> <a> Coverity </a> </td> <td> 2017.07 </td> <td> <strong>INTEGER_OVERFLOW</strong> </td> <td> Implemented </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.4 </td> <td> <strong>C2910, C3383, C3384, C3385, C3386</strong> <strong>C++2910</strong> <strong>DF2911, DF2912, DF2913, </strong> </td> <td> </td> </tr> <tr> <td> <a> Klocwork </a> </td> <td> 2022.4 </td> <td> <strong>NUM.OVERFLOW</strong> <strong>CWARN.NOEFFECT.OUTOFRANGE</strong> <strong>NUM.OVERFLOW.DF</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>493 S, 494 S</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.2 </td> <td> <strong>CERT_C-INT30-a</strong> <strong>CERT_C-INT30-b</strong> <strong>CERT_C-INT30-c</strong> </td> <td> Avoid integer overflows Integer overflow or underflow in constant expression in '+', '-', '\*' operator Integer overflow or underflow in constant expression in '&lt;&lt;' operator </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule INT30-C </a> </td> <td> Checks for: Unsigned integer overflownsigned integer overflow, unsigned integer constant overflownsigned integer constant overflow. Rule partially covered. </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>2910 \[C\], 2911 \[D\], 2912 \[A\], </strong> <strong>2913 \[S\], 3383, 3384, 3385, 3386</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> PRQA QA-C++ </a> </td> <td> 4.4 </td> <td> <strong>2910, 2911, 2912, 2913</strong> </td> <td> </td> </tr> <tr> <td> <a> PVS-Studio </a> </td> <td> 7.23 </td> <td> <strong><a>V658</a>, <a>V1012</a>, <strong><a>V1028</a>, <a>V5005</a>, <a>V5011</a> </strong></strong> </td> <td> </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>unsigned overflow</strong> </td> <td> Exhaustively verified. </td> </tr> </tbody> </table>
+
+
+## Related Vulnerabilities
+
+[CVE-2009-1385](http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2009-1385) results from a violation of this rule. The value performs an unchecked subtraction on the `length` of a buffer and then adds those many bytes of data to another buffer \[[xorl 2009](http://xorl.wordpress.com/2009/06/10/cve-2009-1385-linux-kernel-e1000-integer-underflow/)\]. This can cause a buffer overflow, which allows an attacker to execute arbitrary code.
+
+A Linux Kernel vmsplice [exploit](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-exploit), described by Rafal Wojtczuk \[[Wojtczuk 2008](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-Wojtczuk08)\], documents a [vulnerability](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability) and exploit arising from a buffer overflow (caused by unsigned integer wrapping).
+
+Don Bailey \[[Bailey 2014](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-Bailey14)\] describes an unsigned integer wrap [vulnerability](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability) in the LZO compression algorithm, which can be exploited in some implementations.
+
+[CVE-2014-4377](https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2014-4377) describes a [vulnerability](http://blog.binamuse.com/2014/09/coregraphics-memory-corruption.html) in iOS 7.1 resulting from a multiplication operation that wraps, producing an insufficiently small value to pass to a memory allocation routine, which is subsequently overflowed.
+
+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+INT30-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 </a> </td> <td> <a> INT02-C. Understand integer conversion rules </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR30-C. Do not form or use out-of-bounds pointers or array subscripts </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR36-C. Do not subtract or compare two pointers that do not refer to the same array </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR37-C. Do not add or subtract an integer to a pointer to a non-array object </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> CON08-C. Do not assume that a group of calls to independently atomic methods is atomic </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> ISO/IEC TR 24772:2013 </a> </td> <td> Arithmetic Wrap-Around Error \[FIF\] </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-190 </a> , Integer Overflow or Wraparound </td> <td> 2016-12-02: CERT: Rule subset of CWE </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-131 </a> </td> <td> 2017-05-16: CERT: Partial overlap </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-191 </a> </td> <td> 2017-05-18: CERT: Partial overlap </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-680 </a> </td> <td> 2017-05-18: CERT: Partial overlap </td> </tr> </tbody> </table>
+
+
+## CERT-CWE Mapping Notes
+
+[Key here](https://wiki.sei.cmu.edu/confluence/pages/viewpage.action?pageId=87152408#HowthisCodingStandardisOrganized-CERT-CWEMappingNotes) for mapping notes
+
+**CWE-131 and INT30-C**
+
+* Intersection( INT30-C, MEM35-C) = Ø
+* Intersection( CWE-131, INT30-C) =
+* Calculating a buffer size such that the calculation wraps. This can happen, for example, when using malloc() or operator new\[\] to allocate an array, multiplying the array item size with the array dimension. An untrusted dimension could cause wrapping, resulting in a too-small buffer being allocated, and subsequently overflowed when the array is initialized.
+* CWE-131 – INT30-C =
+* Incorrect calculation of a buffer size that does not involve wrapping. This includes off-by-one errors, for example.
+INT30-C – CWE-131 =
+* Integer wrapping where the result is not used to allocate memory.
+**CWE-680 and INT30-C**
+
+Intersection( CWE-680, INT30-C) =
+
+* Unsigned integer overflows that lead to buffer overflows
+CWE-680 - INT30-C =
+* Signed integer overflows that lead to buffer overflows
+INT30-C – CWE-680 =
+* Unsigned integer overflows that do not lead to buffer overflows
+**CWE-191 and INT30-C**
+
+Union( CWE-190, CWE-191) = Union( INT30-C, INT32-C) Intersection( INT30-C, INT32-C) == Ø
+
+Intersection(CWE-191, INT30-C) =
+
+* Underflow of unsigned integer operation
+CWE-191 – INT30-C =
+* Underflow of signed integer operation
+INT30-C – CWE-191 =
+* Overflow of unsigned integer operation
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> Bailey 2014 </a> \] </td> <td> <a> Raising Lazarus - The 20 Year Old Bug that Went to Mars </a> </td> </tr> <tr> <td> \[ <a> Dowd 2006 </a> \] </td> <td> Chapter 6, "C Language Issues" ("Arithmetic Boundary Conditions," pp. 211–223) </td> </tr> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> Subclause 6.2.5, "Types" </td> </tr> <tr> <td> \[ <a> Seacord 2013b </a> \] </td> <td> Chapter 5, "Integer Security" </td> </tr> <tr> <td> \[ <a> Viega 2005 </a> \] </td> <td> Section 5.2.7, "Integer Overflow" </td> </tr> <tr> <td> \[ <a> VU\#551436 </a> \] </td> <td> </td> </tr> <tr> <td> \[ <a> Warren 2002 </a> \] </td> <td> Chapter 2, "Basics" </td> </tr> <tr> <td> \[ <a> Wojtczuk 2008 </a> \] </td> <td> </td> </tr> <tr> <td> \[ <a> xorl 2009 </a> \] </td> <td> <a> "CVE-2009-1385: Linux Kernel E1000 Integer Underflow" </a> </td> </tr> </tbody> </table>
+
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT30-C: Ensure that unsigned integer operations do not wrap](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql b/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql
new file mode 100644
index 0000000000..3d25313915
--- /dev/null
+++ b/c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql
@@ -0,0 +1,38 @@
+/**
+ * @id c/cert/unsigned-integer-operations-wrap-around
+ * @name INT30-C: Ensure that unsigned integer operations do not wrap
+ * @description Unsigned integer expressions do not strictly overflow, but instead wrap around in a
+ *              modular way. If the size of the type is not sufficient, this can happen
+ *              unexpectedly.
+ * @kind problem
+ * @precision medium
+ * @problem.severity error
+ * @tags external/cert/id/int30-c
+ *       correctness
+ *       security
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import codingstandards.cpp.Overflow
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+from InterestingOverflowingOperation op
+where
+  not isExcluded(op, IntegerOverflowPackage::unsignedIntegerOperationsWrapAroundQuery()) and
+  op.getType().getUnderlyingType().(IntegralType).isUnsigned() and
+  // Not within a guard condition
+  not exists(GuardCondition gc | gc.getAChild*() = op) and
+  // Not guarded by a check, where the check is not an invalid overflow check
+  not op.hasValidPreCheck() and
+  // Is not checked after the operation
+  not op.hasValidPostCheck() and
+  // Permitted by exception 3
+  not op instanceof LShiftExpr and
+  // Permitted by exception 2 - zero case is handled in separate query
+  not op instanceof DivExpr and
+  not op instanceof RemExpr
+select op,
+  "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() + " may wrap."
diff --git a/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.md b/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.md
new file mode 100644
index 0000000000..50e0bfdbe0
--- /dev/null
+++ b/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.md
@@ -0,0 +1,361 @@
+# INT31-C: Ensure that integer conversions do not result in lost or misinterpreted data
+
+This query implements the CERT-C rule INT31-C:
+
+> Ensure that integer conversions do not result in lost or misinterpreted data
+
+
+## Description
+
+Integer conversions, both implicit and explicit (using a cast), must be guaranteed not to result in lost or misinterpreted data. This rule is particularly true for integer values that originate from untrusted sources and are used in any of the following ways:
+
+* Integer operands of any pointer arithmetic, including array indexing
+* The assignment expression for the declaration of a variable length array
+* The postfix expression preceding square brackets `[]` or the expression in square brackets `[]` of a subscripted designation of an element of an array object
+* Function arguments of type `size_t` or `rsize_t` (for example, an argument to a memory allocation function)
+This rule also applies to arguments passed to the following library functions that are converted to `unsigned char`:
+* `memset()`
+* `memset_s()`
+* `fprintf()` and related functions (For the length modifier `c`, if no `l` length modifier is present, the `int` argument is converted to an `unsigned char`, and the resulting character is written.)
+* `fputc()`
+* `ungetc()`
+* `memchr()`
+and to arguments to the following library functions that are converted to `char`:
+* `strchr()`
+* `strrchr()`
+* All of the functions listed in `<ctype.h>`
+The only integer type conversions that are guaranteed to be safe for all data values and all possible conforming implementations are conversions of an integral value to a wider type of the same signedness. The C Standard, subclause 6.3.1.3 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IECTR24731-2-2010)\], says
+
+> When a value with integer type is converted to another integer type other than `_Bool`, if the value can be represented by the new type, it is unchanged.
+
+
+Otherwise, if the new type is unsigned, the value is converted by repeatedly adding or subtracting one more than the maximum value that can be represented in the new type until the value is in the range of the new type.
+
+Otherwise, the new type is signed and the value cannot be represented in it; either the result is [implementation-defined](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation-definedbehavior) or an implementation-defined signal is raised.
+
+Typically, converting an integer to a smaller type results in truncation of the high-order bits.
+
+## Noncompliant Code Example (Unsigned to Signed)
+
+Type range errors, including loss of data (truncation) and loss of sign (sign errors), can occur when converting from a value of an unsigned integer type to a value of a signed integer type. This noncompliant code example results in a truncation error on most [implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation):
+
+```cpp
+#include <limits.h>
+ 
+void func(void) {
+  unsigned long int u_a = ULONG_MAX;
+  signed char sc;
+  sc = (signed char)u_a; /* Cast eliminates warning */
+  /* ... */
+}
+```
+
+## Compliant Solution (Unsigned to Signed)
+
+Validate ranges when converting from an unsigned type to a signed type. This compliant solution can be used to convert a value of `unsigned long int` type to a value of `signed char `type:
+
+```cpp
+#include <limits.h>
+ 
+void func(void) {
+  unsigned long int u_a = ULONG_MAX;
+  signed char sc;
+  if (u_a <= SCHAR_MAX) {
+    sc = (signed char)u_a;  /* Cast eliminates warning */
+  } else {
+    /* Handle error */
+  }
+}
+```
+
+## Noncompliant Code Example (Signed to Unsigned)
+
+Type range errors, including loss of data (truncation) and loss of sign (sign errors), can occur when converting from a value of a signed type to a value of an unsigned type. This noncompliant code example results in a negative number being misinterpreted as a large positive number.
+
+```cpp
+#include <limits.h>
+
+void func(signed int si) {
+  /* Cast eliminates warning */
+  unsigned int ui = (unsigned int)si;
+
+  /* ... */
+}
+
+/* ... */
+
+func(INT_MIN);
+```
+
+## Compliant Solution (Signed to Unsigned)
+
+Validate ranges when converting from a signed type to an unsigned type. This compliant solution converts a value of a `signed int` type to a value of an `unsigned int` type:
+
+```cpp
+#include <limits.h>
+
+void func(signed int si) {
+  unsigned int ui;
+  if (si < 0) {
+    /* Handle error */
+  } else {
+    ui = (unsigned int)si;  /* Cast eliminates warning */
+  }
+  /* ... */
+}
+/* ... */
+
+func(INT_MIN + 1);
+```
+Subclause 6.2.5, paragraph 9, of the C Standard \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IECTR24731-2-2010)\] provides the necessary guarantees to ensure this solution works on a [conforming](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-conformingprogram) [implementation](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation):
+
+> The range of nonnegative values of a signed integer type is a subrange of the corresponding unsigned integer type, and the representation of the same value in each type is the same.
+
+
+## Noncompliant Code Example (Signed, Loss of Precision)
+
+A loss of data (truncation) can occur when converting from a value of a signed integer type to a value of a signed type with less precision. This noncompliant code example results in a truncation error on most [implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation):
+
+```cpp
+#include <limits.h>
+
+void func(void) {
+  signed long int s_a = LONG_MAX;
+  signed char sc = (signed char)s_a; /* Cast eliminates warning */
+  /* ... */
+}
+```
+
+## Compliant Solution (Signed, Loss of Precision)
+
+Validate ranges when converting from a signed type to a signed type with less precision. This compliant solution converts a value of a `signed long int` type to a value of a `signed char` type:
+
+```cpp
+#include <limits.h>
+
+void func(void) {
+  signed long int s_a = LONG_MAX;
+  signed char sc;
+  if ((s_a < SCHAR_MIN) || (s_a > SCHAR_MAX)) {
+    /* Handle error */
+  } else {
+    sc = (signed char)s_a; /* Use cast to eliminate warning */
+  }
+  /* ... */
+}
+
+```
+Conversions from a value of a signed integer type to a value of a signed integer type with less precision requires that both the upper and lower bounds are checked.
+
+## Noncompliant Code Example (Unsigned, Loss of Precision)
+
+A loss of data (truncation) can occur when converting from a value of an unsigned integer type to a value of an unsigned type with less precision. This noncompliant code example results in a truncation error on most [implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation):
+
+```cpp
+#include <limits.h>
+
+void func(void) {
+  unsigned long int u_a = ULONG_MAX;
+  unsigned char uc = (unsigned char)u_a; /* Cast eliminates warning */
+  /* ... */
+}
+```
+
+## Compliant Solution (Unsigned, Loss of Precision)
+
+Validate ranges when converting a value of an unsigned integer type to a value of an unsigned integer type with less precision. This compliant solution converts a value of an `unsigned long int` type to a value of an `unsigned char` type:
+
+```cpp
+#include <limits.h>
+
+void func(void) {
+  unsigned long int u_a = ULONG_MAX;
+  unsigned char uc;
+  if (u_a > UCHAR_MAX) {
+    /* Handle error */
+  } else {
+    uc = (unsigned char)u_a; /* Cast eliminates warning */
+  }
+  /* ... */
+}
+
+```
+Conversions from unsigned types with greater precision to unsigned types with less precision require only the upper bounds to be checked.
+
+## Noncompliant Code Example (time_t Return Value)
+
+The `time()` function returns the value `(time_t)(-1)` to indicate that the calendar time is not available. The C Standard requires that the `time_t` type is only a *real type* capable of representing time. (The integer and real floating types are collectively called real types.) It is left to the implementor to decide the best real type to use to represent time. If `time_t` is implemented as an unsigned integer type with less precision than a signed `int`, the return value of `time()` will never compare equal to the integer literal `-1`.
+
+```cpp
+#include <time.h>
+ 
+void func(void) {
+  time_t now = time(NULL);
+  if (now != -1) {
+    /* Continue processing */
+  }
+}
+```
+
+## Compliant Solution (time_t Return Value)
+
+To ensure the comparison is properly performed, the return value of `time()` should be compared against `-1` cast to type `time_t`:
+
+```cpp
+#include <time.h>
+ 
+void func(void) {
+  time_t now = time(NULL);
+  if (now != (time_t)-1) {
+    /* Continue processing */
+  }
+}
+```
+This solution is in accordance with [INT18-C. Evaluate integer expressions in a larger size before comparing or assigning to that size](https://wiki.sei.cmu.edu/confluence/display/c/INT18-C.+Evaluate+integer+expressions+in+a+larger+size+before+comparing+or+assigning+to+that+size). Note that `(time_+t)-1` also complies with **INT31-C-EX3**.
+
+## Noncompliant Code Example (memset())
+
+For historical reasons, certain C Standard functions accept an argument of type `int` and convert it to either `unsigned char` or plain `char`. This conversion can result in unexpected behavior if the value cannot be represented in the smaller type. The second argument to `memset()` is an example; it indicates what byte to store in the range of memory indicated by the first and third arguments. If the second argument is outside the range of a `signed char` or plain `char`, then its higher order bits will typically be truncated. Consequently, this noncompliant solution unexpectedly sets all elements in the array to 0, rather than 4096:
+
+```cpp
+#include <string.h>
+#include <stddef.h>
+ 
+int *init_memory(int *array, size_t n) {
+  return memset(array, 4096, n); 
+} 
+```
+
+## Compliant Solution (memset())
+
+In general, the `memset()` function should not be used to initialize an integer array unless it is to set or clear all the bits, as in this compliant solution:
+
+```cpp
+#include <string.h>
+#include <stddef.h>
+
+int *init_memory(int *array, size_t n) {
+  return memset(array, 0, n); 
+} 
+```
+
+## Exceptions
+
+**INT31-C-EX1:** The C Standard defines minimum ranges for standard integer types. For example, the minimum range for an object of type `unsigned short int` is 0 to 65,535, whereas the minimum range for `int` is −32,767 to +32,767. Consequently, it is not always possible to represent all possible values of an `unsigned short int` as an `int`. However, on the IA-32 architecture, for example, the actual integer range is from −2,147,483,648 to +2,147,483,647, meaning that it is quite possible to represent all the values of an `unsigned short int` as an `int` for this architecture. As a result, it is not necessary to provide a test for this conversion on IA-32. It is not possible to make assumptions about conversions without knowing the precision of the underlying types. If these tests are not provided, assumptions concerning precision must be clearly documented, as the resulting code cannot be safely ported to a system where these assumptions are invalid. A good way to document these assumptions is to use static assertions. (See [DCL03-C. Use a static assertion to test the value of a constant expression](https://wiki.sei.cmu.edu/confluence/display/c/DCL03-C.+Use+a+static+assertion+to+test+the+value+of+a+constant+expression).)
+
+**INT31-C-EX2:** Conversion from any integer type with a value between `SCHAR_MIN` and `UCHAR_MAX` to a character type is permitted provided the value represents a character and not an integer.
+
+Conversions to unsigned character types are well defined by C to have modular behavior. A character's value is not misinterpreted by the loss of sign or conversion to a negative number. For example, the Euro symbol `€` is sometimes represented by bit pattern `0x80` which can have the numerical value 128 or −127 depending on the signedness of the type.
+
+Conversions to signed character types are more problematic. The C Standard, subclause 6.3.1.3, paragraph 3 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IECTR24731-2-2010)\], says, regarding conversions
+
+> Otherwise, the new type is signed and the value cannot be represented in it; either the result is implementation-defined or an implementation-defined signal is raised.
+
+
+Furthermore, subclause 6.2.6.2, paragraph 2, says, regarding integer modifications
+
+> If the sign bit is one, the value shall be modified in one of the following ways:— the corresponding value with sign bit 0 is negated (sign and magnitude)— the sign bit has the value −(2M ) (two’s complement);— the sign bit has the value −(2M − 1) (ones’ complement).Which of these applies is implementation-defined, as is whether the value with sign bit 1 and all value bits zero (for the first two), or with sign bit and all value bits 1 (for ones’ complement), is a trap representation or a normal value. \[See note.\]
+
+
+NOTE: *Two's complement* is shorthand for "radix complement in radix 2." *Ones' complement* is shorthand for "diminished radix complement in radix 2."
+
+Consequently, the standard allows for this code to trap:
+
+```cpp
+int i = 128; /* 1000 0000 in binary */
+assert(SCHAR_MAX == 127);
+signed char c = i; /* can trap */
+
+```
+However, platforms where this code traps or produces an unexpected value are rare. According to *[The New C Standard: An Economic and Cultural Commentary](http://www.knosof.co.uk/cbook/cbook.html)* by Derek Jones \[[Jones 2008](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-Jones08)\],
+
+> Implementations with such trap representations are thought to have existed in the past. Your author was unable to locate any documents describing such processors.
+
+
+**INT31-C-EX3:** ISO C, section 7.27.2.4, paragraph 3 says:
+
+> The time function returns the implementation’s best approximation to the current calendar time.
+
+
+The value (time_t) (−1) is returned if the calendar time is not available.
+
+If `time_t` is an unsigned type, then the expression `((time_t) (-1))` is guaranteed to yield a large positive value.
+
+Therefore, conversion of a negative compile-time constant to an unsigned value with the same or larger width is permitted by this rule. This exception does not apply to conversion of unsigned to signed values, nor does it apply if the resulting value would undergo truncation.
+
+## Risk Assessment
+
+Integer truncation errors can lead to buffer overflows and the execution of arbitrary code by an attacker.
+
+<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> INT31-C </td> <td> High </td> <td> Probable </td> <td> High </td> <td> <strong>P6</strong> </td> <td> <strong>L2</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> </td> <td> Supported via MISRA C:2012 Rules 10.1, 10.3, 10.4, 10.6 and 10.7 </td> </tr> <tr> <td> <a> CodeSonar </a> </td> <td> 7.2p0 </td> <td> <strong>LANG.CAST.PC.AVLANG.CAST.PC.CONST2PTRLANG.CAST.PC.INT</strong> <strong>LANG.CAST.COERCELANG.CAST.VALUE</strong> <strong>ALLOC.SIZE.TRUNCMISC.MEM.SIZE.TRUNC</strong> <strong>LANG.MEM.TBA</strong> </td> <td> Cast: arithmetic type/void pointer Conversion: integer constant to pointer Conversion: pointer/integer Coercion alters value Cast alters value Truncation of allocation size Truncation of size Tainted buffer access </td> </tr> <tr> <td> <a> Compass/ROSE </a> </td> <td> </td> <td> </td> <td> Can detect violations of this rule. However, false warnings may be raised if <code>limits.h</code> is included </td> </tr> <tr> <td> <a> Coverity </a> \* </td> <td> 2017.07 </td> <td> <strong>NEGATIVE_RETURNS</strong> <strong>REVERSE_NEGATIVE</strong> <strong>MISRA_CAST</strong> </td> <td> Can find array accesses, loop bounds, and other expressions that may contain dangerous implied integer conversions that would result in unexpected behavior Can find instances where a negativity check occurs after the negative value has been used for something else Can find instances where an integer expression is implicitly converted to a narrower integer type, where the signedness of an integer value is implicitly converted, or where the type of a complex expression is implicitly converted </td> </tr> <tr> <td> <a> Cppcheck </a> </td> <td> 1.66 </td> <td> <strong>memsetValueOutOfRange</strong> </td> <td> The second argument to <code>memset()</code> cannot be represented as <code>unsigned char</code> </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.4 </td> <td> <strong>C2850, C2855, C2890, C2895, C2900, C2905, </strong> <strong>C++2850, C++2855, C++2890, </strong> <strong>C++2895, C++2900, </strong> <strong>C++2905, C++3000, C++3010</strong> <strong>DF2851, DF2852, DF2853, DF2856, DF2857, DF2858, DF2891, DF2892, DF2893, DF2896, DF2897, DF2898, DF2901, DF2902, DF2903, DF2906, DF2907, DF2908</strong> </td> <td> </td> </tr> <tr> <td> <a> Klocwork </a> </td> <td> 2022.4 </td> <td> <strong>PORTING.CAST.SIZE</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>93 S</strong> <strong>, 433 S</strong> <strong>, 434 S</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.2 </td> <td> <strong>CERT_C-INT31-a</strong> <strong>CERT_C-INT31-b</strong> <strong>CERT_C-INT31-c</strong> <strong>CERT_C-INT31-d</strong> <strong>CERT_C-INT31-e</strong> <strong>CERT_C-INT31-f</strong> <strong>CERT_C-INT31-g</strong> <strong>CERT_C-INT31-h</strong> <strong>CERT_C-INT31-i</strong> <strong>CERT_C-INT31-j</strong> <strong>CERT_C-INT31-k</strong> <strong>CERT_C-INT31-l</strong> <strong>CERT_C-INT31-m</strong> <strong>CERT_C-INT31-nCERT_C-INT31-o</strong> </td> <td> An expression of essentially Boolean type should always be used where an operand is interpreted as a Boolean value An operand of essentially Boolean type should not be used where an operand is interpreted as a numeric value An operand of essentially character type should not be used where an operand is interpreted as a numeric value An operand of essentially enum type should not be used in an arithmetic operation Shift and bitwise operations should not be performed on operands of essentially signed or enum type An operand of essentially signed or enum type should not be used as the right hand operand to the bitwise shifting operator An operand of essentially unsigned type should not be used as the operand to the unary minus operator The value of an expression shall not be assigned to an object with a narrower essential type The value of an expression shall not be assigned to an object of a different essential type category Both operands of an operator in which the usual arithmetic conversions are performed shall have the same essential type category The second and third operands of the ternary operator shall have the same essential type category The value of a composite expression shall not be assigned to an object with wider essential type If a composite expression is used as one operand of an operator in which the usual arithmetic conversions are performed then the other operand shall not have wider essential type If a composite expression is used as one (second or third) operand of a conditional operator then the other operand shall not have wider essential type Avoid integer overflows </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule INT31-C </a> </td> <td> Checks for: Integer conversion overflownteger conversion overflow, call to memset with unintended value all to memset with unintended value , sign change integer conversion overflowign change integer conversion overflow, tainted sign change conversionainted sign change conversion, unsigned integer conversion overflownsigned integer conversion overflow. Rule partially covered. </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>2850, 2851, 2852, 2853, </strong> <strong><strong>2855, 2856, 2857, 2858,</strong></strong> <strong><strong>2890, 2891, 2892, 2893, </strong></strong> <strong><strong>2895, 2896, 2897, 2898</strong></strong> <strong>2900, 2901, 2902, 2903, </strong> <strong>2905, 2906, 2907, 2908</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> PRQA QA-C++ </a> </td> <td> 4.4 </td> <td> <strong>2850, 2851, 2852, 2853, 2855, 2856, 2857, 2858, </strong> <strong>2890, 2891, 2892, 2893, 2895, 2896, 2897, 2898, </strong> <strong>2900, 2901, 2902, 2903, 2905, 2906, 2907, 2908, </strong> <strong>3000, 3010</strong> </td> <td> </td> </tr> <tr> <td> <a> PVS-Studio </a> </td> <td> 7.23 </td> <td> <strong>V562<a></a></strong> , <strong>V569<a></a></strong> , <strong>V642<a></a></strong> , <strong><a>V676</a></strong> , <strong><a>V716</a></strong> , <strong><a>V721</a></strong> , <strong>V724<a></a></strong> , <strong><a>V732</a></strong> , <strong><a>V739</a></strong> , <strong><a>V784</a></strong> , <strong><a>V793</a></strong> , <strong><a>V1019</a></strong> , <strong><a>V1029</a></strong> , <strong> <a>V1046</a></strong> </td> <td> </td> </tr> <tr> <td> <a> RuleChecker </a> </td> <td> 22.04 </td> <td> </td> <td> Supported via MISRA C:2012 Rules 10.1, 10.3, 10.4, 10.6 and 10.7 </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>signed_downcast</strong> </td> <td> Exhaustively verified. </td> </tr> </tbody> </table>
+\* Coverity Prevent cannot discover all violations of this rule, so further [verification](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-verification) is necessary.
+
+
+## Related Vulnerabilities
+
+[CVE-2009-1376](http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2009-1376) results from a violation of this rule. In version 2.5.5 of Pidgin, a `size_t` offset is set to the value of a 64-bit unsigned integer, which can lead to truncation \[[xorl 2009](http://xorl.wordpress.com/2009/05/28/cve-2009-1376-pidgin-msn-slp-integer-truncation/)\] on platforms where a `size_t` is implemented as a 32-bit unsigned integer. An attacker can execute arbitrary code by carefully choosing this value and causing a buffer overflow.
+
+Search for [vulnerabilities](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerabi) resulting from the violation of this rule on the [CERT website](https://www.kb.cert.org/vulnotes/bymetric?searchview&query=FIELD+KEYWORDS+contains+INT31-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 </a> </td> <td> <a> DCL03-C. Use a static assertion to test the value of a constant expression </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> INT18-C. Evaluate integer expressions in a larger size before comparing or assigning to that size </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> FIO34-C. Distinguish between characters read from a file and EOF or WEOF </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT Oracle Secure Coding Standard for Java </a> </td> <td> <a> NUM12-J. Ensure conversions of numeric types to narrower types do not result in lost or misinterpreted data </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> ISO/IEC TR 24772:2013 </a> </td> <td> Numeric Conversion Errors \[FLC\] </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> MISRA C:2012 </a> </td> <td> Rule 10.1 (required) </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> MISRA C:2012 </a> </td> <td> Rule 10.3 (required) </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> MISRA C:2012 </a> </td> <td> Rule 10.4 (required) </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> MISRA C:2012 </a> </td> <td> Rule 10.6 (required) </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> MISRA C:2012 </a> </td> <td> Rule 10.7 (required) </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-192 </a> , Integer Coercion Error </td> <td> 2017-07-17: CERT: Exact </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-197 </a> , Numeric Truncation Error </td> <td> 2017-06-14: CERT: Rule subset of CWE </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-681 </a> , Incorrect Conversion between Numeric Types </td> <td> 2017-07-17: CERT: Rule subset of CWE </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-704 </a> </td> <td> 2017-07-17: CERT: Rule subset of CWE </td> </tr> </tbody> </table>
+
+
+## CERT-CWE Mapping Notes
+
+[Key here](https://wiki.sei.cmu.edu/confluence/pages/viewpage.action?pageId=87152408#HowthisCodingStandardisOrganized-CERT-CWEMappingNotes) for mapping notes
+
+**CWE-195 and INT31-C**
+
+CWE-195 = Subset( CWE-192)
+
+INT31-C = Union( CWE-195, list) where list =
+
+* Unsigned-to-signed conversion error
+* Truncation that does not change sign
+**CWE-197 and INT31-C**
+
+See CWE-197 and FLP34-C
+
+**CWE-194 and INT31-C**
+
+CWE-194 = Subset( CWE-192)
+
+INT31-C = Union( CWE-194, list) where list =
+
+* Integer conversion that truncates significant data, but without loss of sign
+**CWE-20 and INT31-C**
+
+See CWE-20 and ERR34-C
+
+**CWE-704 and INT31-C**
+
+CWE-704 = Union( INT31-C, list) where list =
+
+* Improper type casts where either the source or target type is not an integral type
+**CWE-681 and INT31-C**
+
+CWE-681 = Union( INT31-C, FLP34-C)
+
+Intersection( INT31-C, FLP34-C) = Ø
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> Dowd 2006 </a> \] </td> <td> Chapter 6, "C Language Issues" ("Type Conversions," pp. 223–270) </td> </tr> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> 6.3.1.3, "Signed and Unsigned Integers" </td> </tr> <tr> <td> \[ <a> Jones 2008 </a> \] </td> <td> Section 6.2.6.2, "Integer Types" </td> </tr> <tr> <td> \[ <a> Seacord 2013b </a> \] </td> <td> Chapter 5, "Integer Security" </td> </tr> <tr> <td> \[ <a> Viega 2005 </a> \] </td> <td> Section 5.2.9, "Truncation Error" Section 5.2.10, "Sign Extension Error" Section 5.2.11, "Signed to Unsigned Conversion Error" Section 5.2.12, "Unsigned to Signed Conversion Error" </td> </tr> <tr> <td> \[ <a> Warren 2002 </a> \] </td> <td> Chapter 2, "Basics" </td> </tr> <tr> <td> \[ <a> xorl 2009 </a> \] </td> <td> <a> "CVE-2009-1376: Pidgin MSN SLP Integer Truncation" </a> </td> </tr> </tbody> </table>
+
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT31-C: Ensure that integer conversions do not result in lost or misinterpreted data](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.ql b/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.ql
new file mode 100644
index 0000000000..51ae704461
--- /dev/null
+++ b/c/cert/src/rules/INT31-C/IntegerConversionCausesDataLoss.ql
@@ -0,0 +1,107 @@
+/**
+ * @id c/cert/integer-conversion-causes-data-loss
+ * @name INT31-C: Ensure that integer conversions do not result in lost or misinterpreted data
+ * @description Converting an integer value to another integer type with a different sign or size
+ *              can lead to data loss or misinterpretation of the value.
+ * @kind problem
+ * @precision medium
+ * @problem.severity error
+ * @tags external/cert/id/int31-c
+ *       correctness
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+
+class IntegerConversion extends Expr {
+  private IntegralType castedToType;
+  private Expr preConversionExpr;
+
+  IntegerConversion() {
+    // This is an explicit cast
+    castedToType = this.(Cast).getType().getUnspecifiedType() and
+    preConversionExpr = this.(Cast).getExpr()
+    or
+    // Functions that internally cast an argument to unsigned char
+    castedToType instanceof UnsignedCharType and
+    this = preConversionExpr and
+    exists(FunctionCall call, string name | call.getTarget().hasGlobalOrStdName(name) |
+      name = ["ungetc", "fputc"] and
+      this = call.getArgument(0)
+      or
+      name = ["memset", "memchr"] and
+      this = call.getArgument(1)
+      or
+      name = "memset_s" and
+      this = call.getArgument(2)
+    )
+  }
+
+  Expr getPreConversionExpr() { result = preConversionExpr }
+
+  Type getCastedToType() { result = castedToType }
+}
+
+bindingset[value]
+predicate withinIntegralRange(IntegralType typ, float value) {
+  exists(float lb, float ub, float limit |
+    limit = 2.pow(8 * typ.getSize()) and
+    (
+      if typ.isUnsigned()
+      then (
+        lb = 0 and ub = limit - 1
+      ) else (
+        lb = -limit / 2 and
+        ub = (limit / 2) - 1
+      )
+    ) and
+    value >= lb and
+    value <= ub
+  )
+}
+
+from
+  IntegerConversion c, Expr preConversionExpr, Type castedToType, Type castedFromType,
+  IntegralType unspecifiedCastedFromType, string typeFromMessage, float preConversionLowerBound,
+  float preConversionUpperBound, float typeLowerBound, float typeUpperBound
+where
+  not isExcluded(c, IntegerOverflowPackage::integerConversionCausesDataLossQuery()) and
+  preConversionExpr = c.getPreConversionExpr() and
+  castedFromType = preConversionExpr.getType() and
+  // Casting from an integral type
+  unspecifiedCastedFromType = castedFromType.getUnspecifiedType() and
+  // Casting to an integral type
+  castedToType = c.getCastedToType() and
+  // Get the upper/lower bound of the pre-conversion expression
+  preConversionLowerBound = lowerBound(preConversionExpr) and
+  preConversionUpperBound = upperBound(preConversionExpr) and
+  // Get the upper/lower bound of the target type
+  typeLowerBound = typeLowerBound(castedToType) and
+  typeUpperBound = typeUpperBound(castedToType) and
+  // Where the result is not within the range of the target type
+  (
+    not withinIntegralRange(castedToType, preConversionLowerBound) or
+    not withinIntegralRange(castedToType, preConversionUpperBound)
+  ) and
+  // A conversion of `-1` to `time_t` is permitted by the standard
+  not (
+    c.getType().getUnspecifiedType().hasName("time_t") and
+    preConversionExpr.getValue() = "-1"
+  ) and
+  // Conversion to unsigned char is permitted from the range [SCHAR_MIN..UCHAR_MAX], as those can
+  // legitimately represent characters
+  not (
+    c.getType().getUnspecifiedType() instanceof UnsignedCharType and
+    lowerBound(preConversionExpr) >= typeLowerBound(any(SignedCharType s)) and
+    upperBound(preConversionExpr) <= typeUpperBound(any(UnsignedCharType s))
+  ) and
+  not castedToType instanceof BoolType and
+  // Create a helpful message
+  if castedFromType = unspecifiedCastedFromType
+  then typeFromMessage = castedFromType.toString()
+  else typeFromMessage = castedFromType + " (" + unspecifiedCastedFromType + ")"
+select c,
+  "Conversion from " + typeFromMessage + " to " + castedToType +
+    " may cause data loss (casting from range " + preConversionLowerBound + "..." +
+    preConversionUpperBound + " to range " + typeLowerBound + "..." + typeUpperBound + ")."
diff --git a/c/cert/src/rules/INT32-C/SignedIntegerOverflow.md b/c/cert/src/rules/INT32-C/SignedIntegerOverflow.md
new file mode 100644
index 0000000000..dbe36775bf
--- /dev/null
+++ b/c/cert/src/rules/INT32-C/SignedIntegerOverflow.md
@@ -0,0 +1,481 @@
+# INT32-C: Ensure that operations on signed integers do not result in overflow
+
+This query implements the CERT-C rule INT32-C:
+
+> Ensure that operations on signed integers do not result in overflow
+
+
+## Description
+
+Signed integer overflow is [undefined behavior 36](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-undefinedbehavior). Consequently, [implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation) have considerable latitude in how they deal with signed integer overflow. (See [MSC15-C. Do not depend on undefined behavior](https://wiki.sei.cmu.edu/confluence/display/c/MSC15-C.+Do+not+depend+on+undefined+behavior).) An implementation that defines signed integer types as being modulo, for example, need not detect integer overflow. Implementations may also trap on signed arithmetic overflows, or simply assume that overflows will never happen and generate object code accordingly. It is also possible for the same conforming implementation to emit code that exhibits different behavior in different contexts. For example, an implementation may determine that a signed integer loop control variable declared in a local scope cannot overflow and may emit efficient code on the basis of that determination, while the same implementation may determine that a global variable used in a similar context will wrap.
+
+For these reasons, it is important to ensure that operations on signed integers do not result in overflow. Of particular importance are operations on signed integer values that originate from a [tainted source](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-taintedsource) and are used as
+
+* Integer operands of any pointer arithmetic, including array indexing
+* The assignment expression for the declaration of a variable length array
+* The postfix expression preceding square brackets `[]` or the expression in square brackets `[]` of a subscripted designation of an element of an array object
+* Function arguments of type `size_t` or `rsize_t` (for example, an argument to a memory allocation function)
+Integer operations will overflow if the resulting value cannot be represented by the underlying representation of the integer. The following table indicates which operations can result in overflow.
+
+<table> <tbody> <tr> <th> Operator </th> <th> Overflow </th> <th> Operator </th> <th> Overflow </th> <th> Operator </th> <th> Overflow </th> <th> Operator </th> <th> Overflow </th> </tr> <tr> <td> <code>+</code> </td> <td> Yes </td> <td> <code>-=</code> </td> <td> Yes </td> <td> <code>&lt;&lt;</code> </td> <td> Yes </td> <td> <code>&lt;</code> </td> <td> No </td> </tr> <tr> <td> <code>-</code> </td> <td> Yes </td> <td> <code>\*=</code> </td> <td> Yes </td> <td> <code>&gt;&gt;</code> </td> <td> No </td> <td> <code>&gt;</code> </td> <td> No </td> </tr> <tr> <td> <code>\*</code> </td> <td> Yes </td> <td> <code>/=</code> </td> <td> Yes </td> <td> <code>&amp;</code> </td> <td> No </td> <td> <code>&gt;=</code> </td> <td> No </td> </tr> <tr> <td> <code>/</code> </td> <td> Yes </td> <td> <code>%=</code> </td> <td> Yes </td> <td> <code>|</code> </td> <td> No </td> <td> <code>&lt;=</code> </td> <td> No </td> </tr> <tr> <td> <code>%</code> </td> <td> Yes </td> <td> <code>&lt;&lt;=</code> </td> <td> Yes </td> <td> <code>^</code> </td> <td> No </td> <td> <code>==</code> </td> <td> No </td> </tr> <tr> <td> <code>++</code> </td> <td> Yes </td> <td> <code>&gt;&gt;=</code> </td> <td> No </td> <td> <code>~</code> </td> <td> No </td> <td> <code>!=</code> </td> <td> No </td> </tr> <tr> <td> <code>--</code> </td> <td> Yes </td> <td> <code>&amp;=</code> </td> <td> No </td> <td> <code>!</code> </td> <td> No </td> <td> <code>&amp;&amp;</code> </td> <td> No </td> </tr> <tr> <td> <code>=</code> </td> <td> No </td> <td> <code>|=</code> </td> <td> No </td> <td> <code>unary +</code> </td> <td> No </td> <td> <code>||</code> </td> <td> No </td> </tr> <tr> <td> <code>+=</code> </td> <td> Yes </td> <td> <code>^=</code> </td> <td> No </td> <td> <code>unary -</code> </td> <td> Yes </td> <td> <code>?:</code> </td> <td> No </td> </tr> </tbody> </table>
+The following sections examine specific operations that are susceptible to integer overflow. When operating on integer types with less precision than `int`, integer promotions are applied. The usual arithmetic conversions may also be applied to (implicitly) convert operands to equivalent types before arithmetic operations are performed. Programmers should understand integer conversion rules before trying to implement secure arithmetic operations. (See [INT02-C. Understand integer conversion rules](https://wiki.sei.cmu.edu/confluence/display/c/INT02-C.+Understand+integer+conversion+rules).)
+
+
+## Implementation Details
+
+GNU GCC invoked with the `[-fwrapv](http://gcc.gnu.org/onlinedocs/gcc-4.5.2/gcc/Code-Gen-Options.html#index-fwrapv-2088)` command-line option defines the same modulo arithmetic for both unsigned and signed integers.
+
+GNU GCC invoked with the `[-ftrapv](http://gcc.gnu.org/onlinedocs/gcc-4.5.2/gcc/Code-Gen-Options.html#index-ftrapv-2088)` command-line option causes a trap to be generated when a signed integer overflows, which will most likely abnormally exit. On a UNIX system, the result of such an event may be a signal sent to the process.
+
+GNU GCC invoked without either the `-fwrapv` or the `-ftrapv` option may simply assume that signed integers never overflow and may generate object code accordingly.
+
+## Atomic Integers
+
+The C Standard defines the behavior of arithmetic on atomic signed integer types to use two's complement representation with silent wraparound on overflow; there are no undefined results. Although defined, these results may be unexpected and therefore carry similar risks to [unsigned integer wrapping](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-unsignedintegerwrapping). (See [INT30-C. Ensure that unsigned integer operations do not wrap](https://wiki.sei.cmu.edu/confluence/display/c/INT30-C.+Ensure+that+unsigned+integer+operations+do+not+wrap).) Consequently, signed integer overflow of atomic integer types should also be prevented or detected.
+
+## Addition
+
+Addition is between two operands of arithmetic type or between a pointer to an object type and an integer type. This rule applies only to addition between two operands of arithmetic type. (See [ARR37-C. Do not add or subtract an integer to a pointer to a non-array object](https://wiki.sei.cmu.edu/confluence/display/c/ARR37-C.+Do+not+add+or+subtract+an+integer+to+a+pointer+to+a+non-array+object) and [ARR30-C. Do not form or use out-of-bounds pointers or array subscripts](https://wiki.sei.cmu.edu/confluence/display/c/ARR30-C.+Do+not+form+or+use+out-of-bounds+pointers+or+array+subscripts).)
+
+Incrementing is equivalent to adding 1.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in a signed integer overflow during the addition of the signed operands `si_a` and `si_b`:
+
+```cpp
+void func(signed int si_a, signed int si_b) {
+  signed int sum = si_a + si_b;
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution ensures that the addition operation cannot overflow, regardless of representation:
+
+```cpp
+#include <limits.h>
+ 
+void f(signed int si_a, signed int si_b) {
+  signed int sum;
+  if (((si_b > 0) && (si_a > (INT_MAX - si_b))) ||
+      ((si_b < 0) && (si_a < (INT_MIN - si_b)))) {
+    /* Handle error */
+  } else {
+    sum = si_a + si_b;
+  }
+  /* ... */
+}
+```
+**Compliant Solution (GNU)**
+
+This compliant solution uses the GNU extension `__builtin_sadd_overflow`, available with GCC, Clang, and ICC:
+
+```cpp
+void f(signed int si_a, signed int si_b) {
+  signed int sum;
+  if (__builtin_sadd_overflow(si_a, si_b, &sum)) {
+    /* Handle error */
+  }
+  /* ... */
+}
+```
+
+## Subtraction
+
+Subtraction is between two operands of arithmetic type, two pointers to qualified or unqualified versions of compatible object types, or a pointer to an object type and an integer type. This rule applies only to subtraction between two operands of arithmetic type. (See [ARR36-C. Do not subtract or compare two pointers that do not refer to the same array](https://wiki.sei.cmu.edu/confluence/display/c/ARR36-C.+Do+not+subtract+or+compare+two+pointers+that+do+not+refer+to+the+same+array), [ARR37-C. Do not add or subtract an integer to a pointer to a non-array object](https://wiki.sei.cmu.edu/confluence/display/c/ARR37-C.+Do+not+add+or+subtract+an+integer+to+a+pointer+to+a+non-array+object), and [ARR30-C. Do not form or use out-of-bounds pointers or array subscripts](https://wiki.sei.cmu.edu/confluence/display/c/ARR30-C.+Do+not+form+or+use+out-of-bounds+pointers+or+array+subscripts) for information about pointer subtraction.)
+
+Decrementing is equivalent to subtracting 1.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in a signed integer overflow during the subtraction of the signed operands `si_a` and `si_b`:
+
+```cpp
+void func(signed int si_a, signed int si_b) {
+  signed int diff = si_a - si_b;
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution tests the operands of the subtraction to guarantee there is no possibility of signed overflow, regardless of representation:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed int si_a, signed int si_b) {
+  signed int diff;
+  if ((si_b > 0 && si_a < INT_MIN + si_b) ||
+      (si_b < 0 && si_a > INT_MAX + si_b)) {
+    /* Handle error */
+  } else {
+    diff = si_a - si_b;
+  }
+
+  /* ... */
+}
+```
+**Compliant Solution (GNU)**
+
+This compliant solution uses the GNU extension `__builtin_ssub_overflow`, available with GCC, Clang, and ICC:
+
+```cpp
+void func(signed int si_a, signed int si_b) {
+  signed int diff;
+  if (__builtin_ssub_overflow(si_a, si_b, &diff)) {
+    /* Handle error */
+  }
+
+  /* ... */
+}
+```
+
+## Multiplication
+
+Multiplication is between two operands of arithmetic type.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in a signed integer overflow during the multiplication of the signed operands `si_a` and `si_b`:
+
+```cpp
+void func(signed int si_a, signed int si_b) {
+  signed int result = si_a * si_b;
+  /* ... */
+}
+```
+**Compliant Solution**
+
+The product of two operands can always be represented using twice the number of bits than exist in the precision of the larger of the two operands. This compliant solution eliminates signed overflow on systems where `long long` is at least twice the precision of `int`:
+
+```cpp
+#include <stddef.h>
+#include <assert.h>
+#include <limits.h>
+#include <inttypes.h>
+ 
+extern size_t popcount(uintmax_t);
+#define PRECISION(umax_value) popcount(umax_value) 
+  
+void func(signed int si_a, signed int si_b) {
+  signed int result;
+  signed long long tmp;
+  assert(PRECISION(ULLONG_MAX) >= 2 * PRECISION(UINT_MAX));
+  tmp = (signed long long)si_a * (signed long long)si_b;
+ 
+  /*
+   * If the product cannot be represented as a 32-bit integer,
+   * handle as an error condition.
+   */
+  if ((tmp > INT_MAX) || (tmp < INT_MIN)) {
+    /* Handle error */
+  } else {
+    result = (int)tmp;
+  }
+  /* ... */
+}
+```
+The assertion fails if `long long` has less than twice the precision of `int`. The `PRECISION()` macro and `popcount()` function provide the correct precision for any integer type. (See [INT35-C. Use correct integer precisions](https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions).)
+
+**Compliant Solution**
+
+The following portable compliant solution can be used with any conforming implementation, including those that do not have an integer type that is at least twice the precision of `int`:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed int si_a, signed int si_b) {
+  signed int result;  
+  if (si_a > 0) {  /* si_a is positive */
+    if (si_b > 0) {  /* si_a and si_b are positive */
+      if (si_a > (INT_MAX / si_b)) {
+        /* Handle error */
+      }
+    } else { /* si_a positive, si_b nonpositive */
+      if (si_b < (INT_MIN / si_a)) {
+        /* Handle error */
+      }
+    } /* si_a positive, si_b nonpositive */
+  } else { /* si_a is nonpositive */
+    if (si_b > 0) { /* si_a is nonpositive, si_b is positive */
+      if (si_a < (INT_MIN / si_b)) {
+        /* Handle error */
+      }
+    } else { /* si_a and si_b are nonpositive */
+      if ( (si_a != 0) && (si_b < (INT_MAX / si_a))) {
+        /* Handle error */
+      }
+    } /* End if si_a and si_b are nonpositive */
+  } /* End if si_a is nonpositive */
+
+  result = si_a * si_b;
+}
+```
+**Compliant Solution (GNU)**
+
+This compliant solution uses the GNU extension `__builtin_smul_overflow`, available with GCC, Clang, and ICC:
+
+```cpp
+void func(signed int si_a, signed int si_b) {
+  signed int result;
+  if (__builtin_smul_overflow(si_a, si_b, &result)) {
+    /* Handle error */
+  }
+}
+```
+
+## Division
+
+Division is between two operands of arithmetic type. Overflow can occur during two's complement signed integer division when the dividend is equal to the minimum (negative) value for the signed integer type and the divisor is equal to `−1`. Division operations are also susceptible to divide-by-zero errors. (See [INT33-C. Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c/INT33-C.+Ensure+that+division+and+remainder+operations+do+not+result+in+divide-by-zero+errors).)
+
+**Noncompliant Code Example**
+
+This noncompliant code example prevents divide-by-zero errors in compliance with [INT33-C. Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c/INT33-C.+Ensure+that+division+and+remainder+operations+do+not+result+in+divide-by-zero+errors) but does not prevent a signed integer overflow error in two's-complement.
+
+```cpp
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if (s_b == 0) {
+    /* Handle error */
+  } else {
+    result = s_a / s_b;
+  }
+  /* ... */
+}
+```
+**Implementation Details**
+
+On the x86-32 architecture, overflow results in a fault, which can be exploited as a [denial-of-service attack](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-denial-of-service).
+
+**Compliant Solution**
+
+This compliant solution eliminates the possibility of divide-by-zero errors or signed overflow:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_b == 0) || ((s_a == LONG_MIN) && (s_b == -1))) {
+    /* Handle error */
+  } else {
+    result = s_a / s_b;
+  }
+  /* ... */
+}
+```
+
+## Remainder
+
+The remainder operator provides the remainder when two operands of integer type are divided. Because many platforms implement remainder and division in the same instruction, the remainder operator is also susceptible to arithmetic overflow and division by zero. (See [INT33-C. Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c/INT33-C.+Ensure+that+division+and+remainder+operations+do+not+result+in+divide-by-zero+errors).)
+
+**Noncompliant Code Example**
+
+Many hardware architectures implement remainder as part of the division operator, which can overflow. Overflow can occur during a remainder operation when the dividend is equal to the minimum (negative) value for the signed integer type and the divisor is equal to −1. It occurs even though the result of such a remainder operation is mathematically 0. This noncompliant code example prevents divide-by-zero errors in compliance with [INT33-C. Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c/INT33-C.+Ensure+that+division+and+remainder+operations+do+not+result+in+divide-by-zero+errors) but does not prevent integer overflow:
+
+```cpp
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if (s_b == 0) {
+    /* Handle error */
+  } else {
+    result = s_a % s_b;
+  }
+  /* ... */
+}
+```
+**Implementation Details**
+
+On x86-32 platforms, the remainder operator for signed integers is implemented by the `idiv` instruction code, along with the divide operator. Because `LONG_MIN / −1` overflows, it results in a software exception with `LONG_MIN % −1` as well.
+
+**Compliant Solution**
+
+This compliant solution also tests the remainder operands to guarantee there is no possibility of an overflow:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_b == 0 ) || ((s_a == LONG_MIN) && (s_b == -1))) {
+    /* Handle error */
+  } else {
+    result = s_a % s_b;
+  }  
+  /* ... */
+}
+```
+
+## Left-Shift Operator
+
+The left-shift operator takes two integer operands. The result of `E1 << E2` is `E1` left-shifted `E2` bit positions; vacated bits are filled with zeros.
+
+The C Standard, 6.5.7, paragraph 4 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)\], states
+
+> If `E1` has a signed type and nonnegative value, and `E1 × 2<sup>E2</sup>` is representable in the result type, then that is the resulting value; otherwise, the behavior is undefined.
+
+
+In almost every case, an attempt to shift by a negative number of bits or by more bits than exist in the operand indicates a logic error. These issues are covered by [INT34-C. Do not shift an expression by a negative number of bits or by greater than or equal to the number of bits that exist in the operand](https://wiki.sei.cmu.edu/confluence/display/c/INT34-C.+Do+not+shift+an+expression+by+a+negative+number+of+bits+or+by+greater+than+or+equal+to+the+number+of+bits+that+exist+in+the+operand).
+
+**Noncompliant Code Example**
+
+This noncompliant code example performs a left shift, after verifying that the number being shifted is not negative, and the number of bits to shift is valid. The `PRECISION()` macro and `popcount()` function provide the correct precision for any integer type. (See [INT35-C. Use correct integer precisions](https://wiki.sei.cmu.edu/confluence/display/c/INT35-C.+Use+correct+integer+precisions).) However, because this code does no overflow check, it can result in an unrepresentable value.
+
+```cpp
+#include <limits.h>
+#include <stddef.h>
+#include <inttypes.h>
+ 
+extern size_t popcount(uintmax_t);
+#define PRECISION(umax_value) popcount(umax_value) 
+
+void func(signed long si_a, signed long si_b) {
+  signed long result;
+  if ((si_a < 0) || (si_b < 0) ||
+      (si_b >= PRECISION(ULONG_MAX)) {
+    /* Handle error */
+  } else {
+    result = si_a << si_b;
+  } 
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution eliminates the possibility of overflow resulting from a left-shift operation:
+
+```cpp
+#include <limits.h>
+#include <stddef.h>
+#include <inttypes.h>
+ 
+extern size_t popcount(uintmax_t);
+#define PRECISION(umax_value) popcount(umax_value) 
+
+void func(signed long si_a, signed long si_b) {
+  signed long result;
+  if ((si_a < 0) || (si_b < 0) ||
+      (si_b >= PRECISION(ULONG_MAX)) ||
+      (si_a > (LONG_MAX >> si_b))) {
+    /* Handle error */
+  } else {
+    result = si_a << si_b;
+  } 
+  /* ... */
+}
+```
+
+## Unary Negation
+
+The unary negation operator takes an operand of arithmetic type. Overflow can occur during two's complement unary negation when the operand is equal to the minimum (negative) value for the signed integer type.
+
+**Noncompliant Code Example**
+
+This noncompliant code example can result in a signed integer overflow during the unary negation of the signed operand `s_a`:
+
+```cpp
+void func(signed long s_a) {
+  signed long result = -s_a;
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution tests the negation operation to guarantee there is no possibility of signed overflow:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a) {
+  signed long result;
+  if (s_a == LONG_MIN) {
+    /* Handle error */
+  } else {
+    result = -s_a;
+  }
+  /* ... */
+}
+
+```
+Risk Assessment
+
+Integer overflow can lead to buffer overflows and the execution of arbitrary code by an attacker.
+
+<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> INT32-C </td> <td> High </td> <td> Likely </td> <td> High </td> <td> <strong>P9</strong> </td> <td> <strong>L2</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>integer-overflow</strong> </td> <td> Fully checked </td> </tr> <tr> <td> <a> CodeSonar </a> </td> <td> 7.2p0 </td> <td> <strong>ALLOC.SIZE.ADDOFLOW</strong> <strong>ALLOC.SIZE.IOFLOW</strong> <strong>ALLOC.SIZE.MULOFLOW</strong> <strong>ALLOC.SIZE.SUBUFLOW</strong> <strong>MISC.MEM.SIZE.ADDOFLOW</strong> <strong>MISC.MEM.SIZE.BAD</strong> <strong>MISC.MEM.SIZE.MULOFLOW</strong> <strong>MISC.MEM.SIZE.SUBUFLOW</strong> </td> <td> Addition overflow of allocation size Integer overflow of allocation size Multiplication overflow of allocation size Subtraction underflow of allocation size Addition overflow of size Unreasonable size argument Multiplication overflow of size Subtraction underflow of size </td> </tr> <tr> <td> <a> Coverity </a> </td> <td> 2017.07 </td> <td> <strong>TAINTED_SCALAR</strong> <strong>BAD_SHIFT</strong> </td> <td> Implemented </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.4 </td> <td> <strong>C2800, C2860</strong> <strong>C++2800, C++2860</strong> <strong>DF2801, DF2802, DF2803, DF2861, DF2862, DF2863</strong> </td> <td> </td> </tr> <tr> <td> <a> Klocwork </a> </td> <td> 2022.4 </td> <td> <strong>NUM.OVERFLOW</strong> <strong>CWARN.NOEFFECT.OUTOFRANGE</strong> <strong>NUM.OVERFLOW.DF</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>493 S,</strong> <strong> 494 S</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.2 </td> <td> <strong>CERT_C-INT32-a</strong> <strong>CERT_C-INT32-b</strong> <strong>CERT_C-INT32-c</strong> </td> <td> Avoid integer overflows Integer overflow or underflow in constant expression in '+', '-', '\*' operator Integer overflow or underflow in constant expression in '&lt;&lt;' operator </td> </tr> <tr> <td> <a> Parasoft Insure++ </a> </td> <td> </td> <td> </td> <td> Runtime analysis </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule INT32-C </a> </td> <td> Checks for: Integer overflownteger overflow, tainted division operandainted division operand, tainted modulo operandainted modulo operand. Rule partially covered. </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>2800, 2801, 2802, 2803,</strong> <strong>2860, 2861, 2862, 2863</strong> </td> <td> Fully implemented </td> </tr> <tr> <td> <a> PRQA QA-C++ </a> </td> <td> 4.4 </td> <td> <strong>2800, 2801, 2802, 2803,</strong> <strong> 2860, 2861, 2862, 2863</strong> </td> <td> </td> </tr> <tr> <td> <a> PVS-Studio </a> </td> <td> 7.23 </td> <td> <strong><a>V1026</a>, <a>V1070</a>, <a>V1081</a>, <a>V1083</a>, <a>V1085</a>, <a>V5010</a></strong> </td> <td> </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>signed_overflow</strong> </td> <td> Exhaustively verified (see <a> one compliant and one 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+INT32-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 </a> </td> <td> <a> INT02-C. Understand integer conversion rules </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> INT35-C. Use correct integer precisions </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> INT33-C. Ensure that division and remainder operations do not result in divide-by-zero errors </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> INT34-C. Do not shift an expression by a negative number of bits or by greater than or equal to the number of bits that exist in the operand </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR30-C. Do not form or use out-of-bounds pointers or array subscripts </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR36-C. Do not subtract or compare two pointers that do not refer to the same array </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> ARR37-C. Do not add or subtract an integer to a pointer to a non-array object </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> MSC15-C. Do not depend on undefined behavior </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C </a> </td> <td> <a> CON08-C. Do not assume that a group of calls to independently atomic methods is atomic </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT Oracle Secure Coding Standard for Java </a> </td> <td> <a> INT00-J. Perform explicit range checking to avoid integer overflow </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> ISO/IEC TR 24772:2013 </a> </td> <td> Arithmetic Wrap-Around Error \[FIF\] </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> ISO/IEC TS 17961 </a> </td> <td> Overflowing signed integers \[intoflow\] </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-190 </a> , Integer Overflow or Wraparound </td> <td> 2017-05-18: CERT: Partial overlap </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-191 </a> </td> <td> 2017-05-18: CERT: Partial overlap </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-680 </a> </td> <td> 2017-05-18: CERT: Partial overlap </td> </tr> </tbody> </table>
+
+
+## CERT-CWE Mapping Notes
+
+[Key here](https://wiki.sei.cmu.edu/confluence/pages/viewpage.action?pageId=87152408#HowthisCodingStandardisOrganized-CERT-CWEMappingNotes) for mapping notes
+
+**CWE-20 and INT32-C**
+
+See CWE-20 and ERR34-C
+
+**CWE-680 and INT32-C**
+
+Intersection( INT32-C, MEM35-C) = Ø
+
+Intersection( CWE-680, INT32-C) =
+
+* Signed integer overflows that lead to buffer overflows
+CWE-680 - INT32-C =
+* Unsigned integer overflows that lead to buffer overflows
+INT32-C – CWE-680 =
+* Signed integer overflows that do not lead to buffer overflows
+**CWE-191 and INT32-C**
+
+Union( CWE-190, CWE-191) = Union( INT30-C, INT32-C)
+
+Intersection( INT30-C, INT32-C) == Ø
+
+Intersection(CWE-191, INT32-C) =
+
+* Underflow of signed integer operation
+CWE-191 – INT32-C =
+* Underflow of unsigned integer operation
+INT32-C – CWE-191 =
+* Overflow of signed integer operation
+**CWE-190 and INT32-C**
+
+Union( CWE-190, CWE-191) = Union( INT30-C, INT32-C)
+
+Intersection( INT30-C, INT32-C) == Ø
+
+Intersection(CWE-190, INT32-C) =
+
+* Overflow (wraparound) of signed integer operation
+CWE-190 – INT32-C =
+* Overflow of unsigned integer operation
+INT32-C – CWE-190 =
+* Underflow of signed integer operation
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> Dowd 2006 </a> \] </td> <td> Chapter 6, "C Language Issues" ("Arithmetic Boundary Conditions," pp. 211–223) </td> </tr> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> Subclause 6.5.5, "Multiplicative Operators" </td> </tr> <tr> <td> \[ <a> Seacord 2013b </a> \] </td> <td> Chapter 5, "Integer Security" </td> </tr> <tr> <td> \[ <a> Viega 2005 </a> \] </td> <td> Section 5.2.7, "Integer Overflow" </td> </tr> <tr> <td> \[ <a> Warren 2002 </a> \] </td> <td> Chapter 2, "Basics" </td> </tr> </tbody> </table>
+
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT32-C: Ensure that operations on signed integers do not result in overflow](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql b/c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql
new file mode 100644
index 0000000000..4c781c4e50
--- /dev/null
+++ b/c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql
@@ -0,0 +1,37 @@
+/**
+ * @id c/cert/signed-integer-overflow
+ * @name INT32-C: Ensure that operations on signed integers do not result in overflow
+ * @description The multiplication of two signed integers can lead to underflow or overflow and
+ *              therefore undefined behavior.
+ * @kind problem
+ * @precision medium
+ * @problem.severity error
+ * @tags external/cert/id/int32-c
+ *       correctness
+ *       security
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import codingstandards.cpp.Overflow
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+from InterestingOverflowingOperation op
+where
+  not isExcluded(op, IntegerOverflowPackage::signedIntegerOverflowQuery()) and
+  (
+    // An operation that returns a signed integer type
+    op.getType().getUnderlyingType().(IntegralType).isSigned()
+    or
+    // The divide or rem expression on a signed integer
+    op.(DivOrRemOperation).getDividend().getType().getUnderlyingType().(IntegralType).isSigned()
+  ) and
+  // Not checked before the operation
+  not op.hasValidPreCheck() and
+  // Covered by INT34-C
+  not op instanceof LShiftExpr
+select op,
+  "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() +
+    " may overflow or underflow."
diff --git a/c/cert/src/rules/INT33-C/DivOrRemByZero.md b/c/cert/src/rules/INT33-C/DivOrRemByZero.md
new file mode 100644
index 0000000000..0810ee078c
--- /dev/null
+++ b/c/cert/src/rules/INT33-C/DivOrRemByZero.md
@@ -0,0 +1,138 @@
+# INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors
+
+This query implements the CERT-C rule INT33-C:
+
+> Ensure that division and remainder operations do not result in divide-by-zero errors
+
+
+## Description
+
+The C Standard identifies the following condition under which division and remainder operations result in [undefined behavior (UB)](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-undefinedbehavior):
+
+<table> <tbody> <tr> <td> UB </td> <td> Description </td> </tr> <tr> <td> <a> 45 </a> </td> <td> The value of the second operand of the <code>/</code> or <code>%</code> operator is zero (6.5.5). </td> </tr> </tbody> </table>
+Ensure that division and remainder operations do not result in divide-by-zero errors.
+
+
+## Division
+
+The result of the `/` operator is the quotient from the division of the first arithmetic operand by the second arithmetic operand. Division operations are susceptible to divide-by-zero errors. Overflow can also occur during two's complement signed integer division when the dividend is equal to the minimum (most negative) value for the signed integer type and the divisor is equal to `−1.` (See [INT32-C. Ensure that operations on signed integers do not result in overflow](https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow).)
+
+**Noncompliant Code Example**
+
+This noncompliant code example prevents signed integer overflow in compliance with [INT32-C. Ensure that operations on signed integers do not result in overflow](https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow) but fails to prevent a divide-by-zero error during the division of the signed operands `s_a` and `s_b`:` `
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_a == LONG_MIN) && (s_b == -1)) {
+    /* Handle error */
+  } else {
+    result = s_a / s_b;
+  }
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution tests the division operation to guarantee there is no possibility of divide-by-zero errors or signed overflow:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_b == 0) || ((s_a == LONG_MIN) && (s_b == -1))) {
+    /* Handle error */
+  } else {
+    result = s_a / s_b;
+  }
+  /* ... */
+}
+```
+
+## Remainder
+
+The remainder operator provides the remainder when two operands of integer type are divided.
+
+**Noncompliant Code Example**
+
+This noncompliant code example prevents signed integer overflow in compliance with [INT32-C. Ensure that operations on signed integers do not result in overflow](https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow) but fails to prevent a divide-by-zero error during the remainder operation on the signed operands `s_a` and `s_b`:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_a == LONG_MIN) && (s_b == -1)) {
+    /* Handle error */
+  } else {
+    result = s_a % s_b;
+  }
+  /* ... */
+}
+```
+**Compliant Solution**
+
+This compliant solution tests the remainder operand to guarantee there is no possibility of a divide-by-zero error or an overflow error:
+
+```cpp
+#include <limits.h>
+ 
+void func(signed long s_a, signed long s_b) {
+  signed long result;
+  if ((s_b == 0 ) || ((s_a == LONG_MIN) && (s_b == -1))) {
+    /* Handle error */
+  } else {
+    result = s_a % s_b;
+  }
+  /* ... */
+}
+```
+
+## Risk Assessment
+
+A divide-by-zero error can result in [abnormal program termination](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-abnormaltermination) and denial of service.
+
+<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> INT33-C </td> <td> Low </td> <td> Likely </td> <td> Medium </td> <td> <strong>P6</strong> </td> <td> <strong>L2</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>int-division-by-zero</strong> <strong>int-modulo-by-zero</strong> </td> <td> Fully checked </td> </tr> <tr> <td> <a> Axivion Bauhaus Suite </a> </td> <td> 7.2.0 </td> <td> <strong>CertC-INT33</strong> </td> <td> </td> </tr> <tr> <td> <a> CodeSonar </a> </td> <td> 7.2p0 </td> <td> <strong>LANG.ARITH.DIVZEROLANG.ARITH.FDIVZERO</strong> </td> <td> Division by zero Float Division By Zero </td> </tr> <tr> <td> <a> Compass/ROSE </a> </td> <td> </td> <td> </td> <td> Can detect some violations of this rule (In particular, it ensures that all operations involving division or modulo are preceded by a check ensuring that the second operand is nonzero.) </td> </tr> <tr> <td> <a> Coverity </a> </td> <td> 2017.07 </td> <td> <strong>DIVIDE_BY_ZERO</strong> </td> <td> Fully implemented </td> </tr> <tr> <td> <a> Cppcheck </a> </td> <td> 1.66 </td> <td> <strong>zerodivzerodivcond</strong> </td> <td> Context sensitive analysis of division by zero Not detected for division by struct member / array element / pointer data that is 0 Detected when there is unsafe division by variable before/after test if variable is zero </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.4 </td> <td> <strong>C2830</strong> <strong>C++2830</strong> <strong>DF2831, DF2832, DF2833</strong> </td> <td> </td> </tr> <tr> <td> <a> Klocwork </a> </td> <td> 2022.4 </td> <td> <strong>DBZ.CONST</strong> <strong>DBZ.CONST.CALL</strong> <strong>DBZ.GENERAL</strong> <strong>DBZ.ITERATOR</strong> <strong>DBZ.ITERATOR.CALL</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>43 D, 127 D, 248 S, 629 S, 80 X</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.2 </td> <td> <strong>CERT_C-INT33-a</strong> </td> <td> Avoid division by zero </td> </tr> <tr> <td> <a> Parasoft Insure++ </a> </td> <td> </td> <td> </td> <td> Runtime analysis </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule INT33-C </a> </td> <td> Checks for: Integer division by zeronteger division by zero, tainted division operandainted division operand, tainted modulo operandainted modulo operand. Rule fully covered. </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>2830 \[C\], 2831 \[D\], 2832 \[A\]</strong> <strong>2833 \[S\]</strong> </td> <td> Fully implemented </td> </tr> <tr> <td> <a> PRQA QA-C++ </a> </td> <td> 4.4 </td> <td> <strong>2831, 2832, 2833</strong> </td> <td> </td> </tr> <tr> <td> <a> SonarQube C/C++ Plugin </a> </td> <td> 3.11 </td> <td> <strong><a>S3518</a></strong> </td> <td> </td> </tr> <tr> <td> <a> PVS-Studio </a> </td> <td> 7.23 </td> <td> <strong><a>V609</a></strong> </td> <td> </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>division_by_zero</strong> </td> <td> Exhaustively verified (see <a> one compliant and one 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+INT33-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 </a> </td> <td> <a> INT32-C. Ensure that operations on signed integers do not result in overflow </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT Oracle Secure Coding Standard for Java </a> </td> <td> <a> NUM02-J. Ensure that division and remainder operations do not result in divide-by-zero errors </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> ISO/IEC TS 17961 </a> </td> <td> Integer division errors \[diverr\] </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CWE 2.11 </a> </td> <td> <a> CWE-369 </a> , Divide By Zero </td> <td> 2017-07-07: CERT: Exact </td> </tr> </tbody> </table>
+
+
+## CERT-CWE Mapping Notes
+
+[Key here](https://wiki.sei.cmu.edu/confluence/pages/viewpage.action?pageId=87152408#HowthisCodingStandardisOrganized-CERT-CWEMappingNotes) for mapping notes
+
+**CWE-682 and INT33-C**
+
+CWE-682 = Union( INT33-C, list) where list =
+
+* Incorrect calculations that do not involve division by zero
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> Seacord 2013b </a> \] </td> <td> Chapter 5, "Integer Security" </td> </tr> <tr> <td> \[ <a> Warren 2002 </a> \] </td> <td> Chapter 2, "Basics" </td> </tr> </tbody> </table>
+
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/INT33-C/DivOrRemByZero.ql b/c/cert/src/rules/INT33-C/DivOrRemByZero.ql
new file mode 100644
index 0000000000..a5e34f13c4
--- /dev/null
+++ b/c/cert/src/rules/INT33-C/DivOrRemByZero.ql
@@ -0,0 +1,37 @@
+/**
+ * @id c/cert/div-or-rem-by-zero
+ * @name INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors
+ * @description Dividing or taking the remainder by zero is undefined behavior.
+ * @kind problem
+ * @precision medium
+ * @problem.severity error
+ * @tags external/cert/id/int33-c
+ *       correctness
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import codingstandards.cpp.Overflow
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+from DivOrRemOperation divOrMod, Expr divisor
+where
+  not isExcluded(divOrMod, IntegerOverflowPackage::divOrRemByZeroQuery()) and
+  divisor = divOrMod.getDivisor() and
+  divisor.getType() instanceof IntegralType and
+  // Range includes 0
+  upperBound(divisor) >= 0 and
+  lowerBound(divisor) <= 0 and
+  // And an explicit check for 0 does not exist
+  not exists(GuardCondition gc, Expr left, Expr right |
+    gc.ensuresEq(left, right, 0, divOrMod.getBasicBlock(), false) and
+    globalValueNumber(left) = globalValueNumber(divisor) and
+    right.getValue().toInt() = 0
+  ) and
+  // Uninstantiated templates may not have an accurate reflection of the range
+  not divOrMod.getEnclosingFunction().isFromUninstantiatedTemplate(_)
+select divOrMod,
+  "Division or remainder expression with divisor that may be zero (divisor range " +
+    lowerBound(divisor) + "..." + upperBound(divisor) + ")."
diff --git a/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.md b/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.md
new file mode 100644
index 0000000000..7cf3875831
--- /dev/null
+++ b/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.md
@@ -0,0 +1,142 @@
+# INT35-C: Use correct integer precisions
+
+This query implements the CERT-C rule INT35-C:
+
+> Use correct integer precisions
+
+
+## Description
+
+Integer types in C have both a *size* and a *precision*. The size indicates the number of bytes used by an object and can be retrieved for any object or type using the `sizeof` operator. The precision of an integer type is the number of bits it uses to represent values, excluding any sign and padding bits.
+
+Padding bits contribute to the integer's size, but not to its precision. Consequently, inferring the precision of an integer type from its size may result in too large a value, which can then lead to incorrect assumptions about the numeric range of these types. Programmers should use correct integer precisions in their code, and in particular, should not use the `sizeof` operator to compute the precision of an integer type on architectures that use padding bits or in strictly conforming (that is, portable) programs.
+
+## Noncompliant Code Example
+
+This noncompliant code example illustrates a function that produces 2 raised to the power of the function argument. To prevent undefined behavior in compliance with [INT34-C. Do not shift an expression by a negative number of bits or by greater than or equal to the number of bits that exist in the operand](https://wiki.sei.cmu.edu/confluence/display/c/INT34-C.+Do+not+shift+an+expression+by+a+negative+number+of+bits+or+by+greater+than+or+equal+to+the+number+of+bits+that+exist+in+the+operand), the function ensures that the argument is less than the number of bits used to store a value of type `unsigned int`.
+
+```cpp
+#include <limits.h>
+ 
+unsigned int pow2(unsigned int exp) {
+  if (exp >= sizeof(unsigned int) * CHAR_BIT) {
+    /* Handle error */
+  }
+  return 1 << exp;
+}
+```
+However, if this code runs on a platform where `unsigned int` has one or more padding bits, it can still result in values for `exp` that are too large. For example, on a platform that stores `unsigned int` in 64 bits, but uses only 48 bits to represent the value, a left shift of 56 bits would result in undefined behavior.
+
+## Compliant Solution
+
+This compliant solution uses a `popcount()` function, which counts the number of bits set on any unsigned integer, allowing this code to determine the precision of any integer type, signed or unsigned.
+
+```cpp
+#include <stddef.h>
+#include <stdint.h>
+ 
+/* Returns the number of set bits */
+size_t popcount(uintmax_t num) {
+  size_t precision = 0;
+  while (num != 0) {
+    if (num % 2 == 1) {
+      precision++;
+    }
+    num >>= 1;
+  }
+  return precision;
+}
+#define PRECISION(umax_value) popcount(umax_value) 
+```
+Implementations can replace the `PRECISION()` macro with a type-generic macro that returns an integer constant expression that is the precision of the specified type for that implementation. This return value can then be used anywhere an integer constant expression can be used, such as in a static assertion. (See [DCL03-C. Use a static assertion to test the value of a constant expression](https://wiki.sei.cmu.edu/confluence/display/c/DCL03-C.+Use+a+static+assertion+to+test+the+value+of+a+constant+expression).) The following type generic macro, for example, might be used for a specific implementation targeting the IA-32 architecture:
+
+```cpp
+#define PRECISION(value)  _Generic(value, \
+  unsigned char : 8, \
+  unsigned short: 16, \
+  unsigned int : 32, \
+  unsigned long : 32, \
+  unsigned long long : 64, \
+  signed char : 7, \
+  signed short : 15, \
+  signed int : 31, \
+  signed long : 31, \
+  signed long long : 63)
+```
+The revised version of the `pow2()` function uses the `PRECISION()` macro to determine the precision of the unsigned type:
+
+```cpp
+#include <stddef.h>
+#include <stdint.h>
+#include <limits.h>
+extern size_t popcount(uintmax_t);
+#define PRECISION(umax_value) popcount(umax_value)  
+unsigned int pow2(unsigned int exp) {
+  if (exp >= PRECISION(UINT_MAX)) {
+    /* Handle error */
+  }
+  return 1 << exp;
+}
+```
+**Implementation Details**
+
+Some platforms, such as the Cray Linux Environment (CLE; supported on Cray XT CNL compute nodes), provide `a _popcnt` instruction that can substitute for the `popcount()` function.
+
+```cpp
+#define PRECISION(umax_value) _popcnt(umax_value)
+
+```
+
+## Risk Assessment
+
+Mistaking an integer's size for its precision can permit invalid precision arguments to operations such as bitwise shifts, resulting in undefined behavior.
+
+<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> INT35-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> </td> <td> Supported: Astrée reports overflows due to insufficient precision. </td> </tr> <tr> <td> <a> CodeSonar </a> </td> <td> 7.2p0 </td> <td> <strong>LANG.ARITH.BIGSHIFT</strong> </td> <td> Shift Amount Exceeds Bit Width </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.4 </td> <td> <strong>C0582</strong> <strong>C++3115</strong> </td> <td> </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.2 </td> <td> <strong>CERT_C-INT35-a</strong> </td> <td> Use correct integer precisions when checking the right hand operand of the shift operator </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule INT35-C </a> </td> <td> Checks for situations when integer precisions are exceeded (rule fully covered) </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>0582</strong> </td> <td> </td> </tr> </tbody> </table>
+
+
+## 
+
+## 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> CWE 2.11 </a> </td> <td> <a> CWE-681 </a> , Incorrect Conversion between Numeric Types </td> <td> 2017-10-30:MITRE: Unspecified Relationship 2018-10-18:CERT:Partial Overlap </td> </tr> </tbody> </table>
+
+
+## CERT-CWE Mapping Notes
+
+[Key here](https://wiki.sei.cmu.edu/confluence/pages/viewpage.action?pageId=87152408#HowthisCodingStandardisOrganized-CERT-CWEMappingNotes) for mapping notes
+
+**CWE-190 and INT35-C**
+
+Intersection( INT35-C, CWE-190) = Ø
+
+INT35-C used to map to CWE-190 but has been replaced with a new rule that has no overlap with CWE-190.
+
+**CWE-681 and INT35-C**
+
+Intersection(INT35-C, CWE-681) = due to incorrect use of integer precision, conversion from one data type to another causing data to be omitted or translated in a way that produces unexpected values
+
+CWE-681 - INT35-C = list2, where list2 =
+
+* conversion from one data type to another causing data to be omitted or translated in a way that produces unexpected values, not involving incorrect use of integer precision
+INT35-C - CWE-681 = list1, where list1 =
+* incorrect use of integer precision not related to conversion from one data type to another
+
+## Bibliography
+
+<table> <tbody> <tr> <td> \[ <a> Dowd 2006 </a> \] </td> <td> Chapter 6, "C Language Issues" </td> </tr> <tr> <td> \[ <a> C99 Rationale 2003 </a> \] </td> <td> 6.5.7, "Bitwise Shift Operators" </td> </tr> </tbody> </table>
+
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT35-C: Use correct integer precisions](https://wiki.sei.cmu.edu/confluence/display/c)
diff --git a/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.ql b/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.ql
new file mode 100644
index 0000000000..cf510bf999
--- /dev/null
+++ b/c/cert/src/rules/INT35-C/UseCorrectIntegerPrecisions.ql
@@ -0,0 +1,35 @@
+/**
+ * @id c/cert/use-correct-integer-precisions
+ * @name INT35-C: Use correct integer precisions
+ * @description The precision of integer types in C cannot be deduced from the size of the type (due
+ *              to padding and sign bits) otherwise a loss of data may occur.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/int35-c
+ *       correctness
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+
+class CharBitMacroInvocation extends MacroInvocation {
+  CharBitMacroInvocation() { this.getMacroName() = "CHAR_BIT" }
+}
+
+from SizeofOperator so, RelationalOperation comparison, MulExpr m, Expr charSize
+where
+  not isExcluded(so, IntegerOverflowPackage::useCorrectIntegerPrecisionsQuery()) and
+  // Multiplication of a sizeof operator and a constant that's probably a char size
+  m.getAnOperand() = so and
+  m.getAnOperand() = charSize and
+  not so = charSize and
+  (
+    charSize.getValue().toInt() = 8
+    or
+    charSize = any(CharBitMacroInvocation c).getExpr()
+  ) and
+  // The result is compared against something, which is probably related to the number of bits
+  comparison.getAnOperand() = m
+select so, "sizeof operator used to determine the precision of an integer type."
diff --git a/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.expected b/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.expected
new file mode 100644
index 0000000000..76594d944b
--- /dev/null
+++ b/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.expected
@@ -0,0 +1,4 @@
+| test.c:4:3:4:9 | ... + ... | Operation + of type unsigned int may wrap. |
+| test.c:5:3:5:10 | ... += ... | Operation += of type unsigned int may wrap. |
+| test.c:58:3:58:9 | ... - ... | Operation - of type unsigned int may wrap. |
+| test.c:59:3:59:10 | ... -= ... | Operation -= of type unsigned int may wrap. |
diff --git a/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.qlref b/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.qlref
new file mode 100644
index 0000000000..045890904c
--- /dev/null
+++ b/c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.qlref
@@ -0,0 +1 @@
+rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/INT30-C/test.c b/c/cert/test/rules/INT30-C/test.c
new file mode 100644
index 0000000000..433cf534f4
--- /dev/null
+++ b/c/cert/test/rules/INT30-C/test.c
@@ -0,0 +1,80 @@
+#include <limits.h>
+
+void test_add_simple(unsigned int i1, unsigned int i2) {
+  i1 + i2;  // NON_COMPLIANT - not bounds checked
+  i1 += i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_add_precheck(unsigned int i1, unsigned int i2) {
+  if (UINT_MAX - i1 < i2) {
+    // handle error
+  } else {
+    i1 + i2;  // COMPLIANT - bounds checked
+    i1 += i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_add_precheck_2(unsigned int i1, unsigned int i2) {
+  if (i1 + i2 < i1) {
+    // handle error
+  } else {
+    i1 + i2;  // COMPLIANT - bounds checked
+    i1 += i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_add_postcheck(unsigned int i1, unsigned int i2) {
+  unsigned int i3 = i1 + i2; // COMPLIANT - checked for overflow afterwards
+  if (i3 < i1) {
+    // handle error
+  }
+  i1 += i2; // COMPLIANT - checked for overflow afterwards
+  if (i1 < i2) {
+    // handle error
+  }
+}
+
+void test_ex2(unsigned int i1, unsigned int i2) {
+  unsigned int ci1 = 2;
+  unsigned int ci2 = 3;
+  ci1 + ci2;     // COMPLIANT, compile time constants
+  i1 + 0;        // COMPLIANT
+  i1 += 0;       // COMPLIANT
+  i1 - 0;        // COMPLIANT
+  i1 -= 0;       // COMPLIANT
+  UINT_MAX - i1; // COMPLIANT - cannot be smaller than 0
+  i1 * 1;        // COMPLIANT
+  i1 *= 1;       // COMPLIANT
+  if (0 <= i1 && i1 < 32) {
+    UINT_MAX >> i1; // COMPLIANT
+  }
+}
+
+void test_ex3(unsigned int i1, unsigned int i2) {
+  i1 << i2; // COMPLIANT - by EX3
+}
+
+void test_sub_simple(unsigned int i1, unsigned int i2) {
+  i1 - i2;  // NON_COMPLIANT - not bounds checked
+  i1 -= i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_sub_precheck(unsigned int i1, unsigned int i2) {
+  if (i1 < i2) {
+    // handle error
+  } else {
+    i1 - i2;  // COMPLIANT - bounds checked
+    i1 -= i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_sub_postcheck(unsigned int i1, unsigned int i2) {
+  unsigned int i3 = i1 - i2; // COMPLIANT - checked for wrap afterwards
+  if (i3 > i1) {
+    // handle error
+  }
+  i1 -= i2; // COMPLIANT - checked for wrap afterwards
+  if (i1 > i2) {
+    // handle error
+  }
+}
\ No newline at end of file
diff --git a/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.expected b/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.expected
new file mode 100644
index 0000000000..ee18410a48
--- /dev/null
+++ b/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.expected
@@ -0,0 +1,11 @@
+| test.c:7:3:7:15 | (signed int)... | Conversion from unsigned int to signed int may cause data loss (casting from range 0...4294967295 to range -2147483648...2147483647). |
+| test.c:17:3:17:17 | (unsigned int)... | Conversion from signed int to unsigned int may cause data loss (casting from range -2147483648...2147483647 to range 0...4294967295). |
+| test.c:34:3:34:17 | (signed short)... | Conversion from signed int to signed short may cause data loss (casting from range -2147483648...2147483647 to range -32768...32767). |
+| test.c:51:3:51:19 | (unsigned short)... | Conversion from unsigned int to unsigned short may cause data loss (casting from range 0...4294967295 to range 0...65535). |
+| test.c:89:3:89:19 | (unsigned char)... | Conversion from signed int to unsigned char may cause data loss (casting from range 100000...100000 to range 0...255). |
+| test.c:92:3:92:19 | (unsigned char)... | Conversion from signed int to unsigned char may cause data loss (casting from range -129...-129 to range 0...255). |
+| test.c:93:3:93:19 | (unsigned char)... | Conversion from signed int to unsigned char may cause data loss (casting from range 256...256 to range 0...255). |
+| test.c:97:9:97:12 | 4096 | Conversion from int to unsigned char may cause data loss (casting from range 4096...4096 to range 0...255). |
+| test.c:99:10:99:13 | 4096 | Conversion from int to unsigned char may cause data loss (casting from range 4096...4096 to range 0...255). |
+| test.c:101:13:101:16 | 4096 | Conversion from int to unsigned char may cause data loss (casting from range 4096...4096 to range 0...255). |
+| test.c:103:13:103:16 | 4096 | Conversion from int to unsigned char may cause data loss (casting from range 4096...4096 to range 0...255). |
diff --git a/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.qlref b/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.qlref
new file mode 100644
index 0000000000..277a450807
--- /dev/null
+++ b/c/cert/test/rules/INT31-C/IntegerConversionCausesDataLoss.qlref
@@ -0,0 +1 @@
+rules/INT31-C/IntegerConversionCausesDataLoss.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/INT31-C/test.c b/c/cert/test/rules/INT31-C/test.c
new file mode 100644
index 0000000000..08b09cf6b8
--- /dev/null
+++ b/c/cert/test/rules/INT31-C/test.c
@@ -0,0 +1,112 @@
+#include <limits.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdio.h>
+#include <string.h>
+void test_unsigned_to_signed(unsigned int x) {
+  (signed int)x; // NON_COMPLIANT - not larger enough to represent all
+}
+
+void test_unsigned_to_signed_check(unsigned int x) {
+  if (x <= INT_MAX) {
+    (signed int)x; // COMPLIANT
+  }
+}
+
+void test_signed_to_unsigned(signed int x) {
+  (unsigned int)x; // NON_COMPLIANT - not large enough to represent all
+}
+
+void test_signed_to_unsigned_check(signed int x) {
+  if (x >= 0) {
+    (unsigned int)x; // COMPLIANT
+  }
+}
+
+void test_signed_to_unsigned_check2(signed int x) {
+  if (x < 0) {
+  } else {
+    (unsigned int)x; // COMPLIANT
+  }
+}
+
+void test_signed_loss_of_precision(signed int x) {
+  (signed short)x; // NON_COMPLIANT - not large enough to represent all
+}
+
+void test_signed_loss_of_precision_check(signed int x) {
+  if (x >= SHRT_MIN && x <= SHRT_MAX) {
+    (signed short)x; // COMPLIANT
+  }
+}
+
+void test_signed_loss_of_precision_check2(signed int x) {
+  if (x < SHRT_MIN || x > SHRT_MAX) {
+  } else {
+    (signed short)x; // COMPLIANT
+  }
+}
+
+void test_unsigned_loss_of_precision(unsigned int x) {
+  (unsigned short)x; // NON_COMPLIANT - not large enough to represent all
+}
+
+void test_unsigned_loss_of_precision_check(unsigned int x) {
+  if (x <= USHRT_MAX) {
+    (unsigned short)x; // COMPLIANT
+  }
+}
+
+void test_unsigned_loss_of_precision_check2(unsigned int x) {
+  if (x > USHRT_MAX) {
+  } else {
+    (unsigned short)x; // COMPLIANT
+  }
+}
+
+// We create a fake stub here to test the case
+// that time_t is an unsigned type.
+typedef unsigned int time_t;
+time_t time(time_t *seconds);
+
+void test_time_t_check_against_zero(time_t x) {
+  time_t now = time(0);
+  if (now != -1) { // NON_COMPLIANT[FALSE_NEGATIVE] - there is no conversion
+                   // here in our model
+  }
+  if (now != (time_t)-1) { // COMPLIANT
+  }
+}
+
+void test_chars() {
+  signed int i1 = 'A';
+  signed int i2 = 100000;
+  signed int i3 = -128;
+  signed int i4 = 255;
+  signed int i5 = -129;
+  signed int i6 = 256;
+  (unsigned char)i1; // COMPLIANT
+  (unsigned char)i2; // NON_COMPLIANT
+  (unsigned char)i3; // COMPLIANT
+  (unsigned char)i4; // COMPLIANT
+  (unsigned char)i5; // NON_COMPLIANT
+  (unsigned char)i6; // NON_COMPLIANT
+}
+
+void test_funcs(int *a, size_t n) {
+  fputc(4096, stdout); // NON_COMPLIANT
+  fputc('A', stdout);  // COMPLIANT
+  ungetc(4096, stdin); // NON_COMPLIANT
+  ungetc('A', stdin);  // COMPLIANT
+  memchr(a, 4096, n);  // NON_COMPLIANT
+  memchr(a, 'A', n);   // COMPLIANT
+  memset(a, 4096, n);  // NON_COMPLIANT
+  memset(a, 0, n);     // COMPLIANT
+  // not supported in our stdlib, or in any of the compilers
+  // memset_s(a, rn, 4096, n); // NON_COMPLIANT
+  // memset_s(a, rn, 0, n);    // COMPLIANT
+}
+
+void test_bool(signed int s) {
+  (bool)s; // COMPLIANT
+}
\ No newline at end of file
diff --git a/c/cert/test/rules/INT32-C/SignedIntegerOverflow.expected b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.expected
new file mode 100644
index 0000000000..0e107bcafa
--- /dev/null
+++ b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.expected
@@ -0,0 +1,24 @@
+| test.c:6:3:6:9 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.c:7:3:7:10 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.c:22:7:22:13 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.c:25:5:25:11 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.c:26:5:26:12 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.c:31:19:31:25 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.c:36:3:36:10 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.c:43:3:43:9 | ... - ... | Operation - of type int may overflow or underflow. |
+| test.c:44:3:44:10 | ... -= ... | Operation -= of type signed int may overflow or underflow. |
+| test.c:58:19:58:25 | ... - ... | Operation - of type int may overflow or underflow. |
+| test.c:62:3:62:10 | ... -= ... | Operation -= of type signed int may overflow or underflow. |
+| test.c:69:3:69:8 | ... * ... | Operation * of type int may overflow or underflow. |
+| test.c:70:3:70:10 | ... *= ... | Operation *= of type signed int may overflow or underflow. |
+| test.c:115:3:115:9 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.c:116:3:116:10 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.c:123:5:123:11 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.c:124:5:124:12 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.c:138:3:138:9 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.c:139:3:139:10 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.c:146:5:146:11 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.c:147:5:147:12 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.c:161:3:161:5 | - ... | Operation - of type signed int may overflow or underflow. |
+| test.c:173:3:173:6 | ... ++ | Operation ++ of type signed int may overflow or underflow. |
+| test.c:189:3:189:6 | ... -- | Operation -- of type signed int may overflow or underflow. |
diff --git a/c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref
new file mode 100644
index 0000000000..dcb26795eb
--- /dev/null
+++ b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref
@@ -0,0 +1 @@
+rules/INT32-C/SignedIntegerOverflow.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/INT32-C/test.c b/c/cert/test/rules/INT32-C/test.c
new file mode 100644
index 0000000000..cde579123b
--- /dev/null
+++ b/c/cert/test/rules/INT32-C/test.c
@@ -0,0 +1,202 @@
+#include <limits.h>
+#include <stddef.h>
+#include <stdint.h>
+
+void test_add_simple(signed int i1, signed int i2) {
+  i1 + i2;  // NON_COMPLIANT - not bounds checked
+  i1 += i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_add_precheck(signed int i1, signed int i2) {
+  // Style recommended by CERT
+  if (((i2 > 0) && (i1 > (INT_MAX - i2))) ||
+      ((i2 < 0) && (i1 < (INT_MIN - i2)))) {
+    // handle error
+  } else {
+    i1 + i2;  // COMPLIANT - bounds appropriately checked
+    i1 += i2; // COMPLIANT - bounds appropriately checked
+  }
+}
+
+void test_add_precheck_2(signed int i1, signed int i2) {
+  if (i1 + i2 < i1) { // NON_COMPLIANT - bad overflow check - undefined behavior
+    // handle error
+  } else {
+    i1 + i2;  // NON_COMPLIANT
+    i1 += i2; // NON_COMPLIANT
+  }
+}
+
+void test_add_postcheck(signed int i1, signed int i2) {
+  signed int i3 = i1 + i2; // NON_COMPLIANT - signed overflow is undefined
+                           // behavior, so checking afterwards is not sufficient
+  if (i3 < i1) {
+    // handle error
+  }
+  i1 += i2; // NON_COMPLIANT
+  if (i1 < i2) {
+    // handle error
+  }
+}
+
+void test_sub_simple(signed int i1, signed int i2) {
+  i1 - i2;  // NON_COMPLIANT - not bounds checked
+  i1 -= i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_sub_precheck(signed int i1, signed int i2) {
+  // Style recomended by CERT
+  if ((i2 > 0 && i1 < INT_MIN + i2) || (i2 < 0 && i1 > INT_MAX + i2)) {
+    // handle error
+  } else {
+    i1 - i2;  // COMPLIANT - bounds checked
+    i1 -= i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_sub_postcheck(signed int i1, signed int i2) {
+  signed int i3 = i1 - i2; // NON_COMPLIANT - underflow is undefined behavior.
+  if (i3 > i1) {
+    // handle error
+  }
+  i1 -= i2; // NON_COMPLIANT - underflow is undefined behavior.
+  if (i1 > i2) {
+    // handle error
+  }
+}
+
+void test_mul_simple(signed int i1, signed int i2) {
+  i1 *i2;   // NON_COMPLIANT
+  i1 *= i2; // NON_COMPLIANT
+}
+
+void test_mul_precheck(signed int i1, signed int i2) {
+  signed long long tmp =
+      (signed long long)i1 * (signed long long)i2; // COMPLIANT
+  signed int result;
+
+  if (tmp > INT_MAX || tmp < INT_MIN) {
+    // handle error
+  } else {
+    result = (signed int)tmp;
+  }
+}
+
+void test_mul_precheck_2(signed int i1, signed int i2) {
+  if (i1 > 0) {
+    if (i2 > 0) {
+      if (i1 > (INT_MAX / i2)) {
+        return; // handle error
+      }
+    } else {
+      if (i2 < (INT_MIN / i1)) {
+        // handle error
+        return; // handle error
+      }
+    }
+  } else {
+    if (i2 > 0) {
+      if (i1 < (INT_MIN / i2)) {
+        // handle error
+        return; // handle error
+      }
+    } else {
+      if ((i1 != 0) && (i2 < (INT_MAX / i1))) {
+        // handle error
+        return; // handle error
+      }
+    }
+  }
+  i1 *i2;   // COMPLIANT
+  i1 *= i2; // COMPLIANT
+}
+
+void test_simple_div(signed int i1, signed int i2) {
+  i1 / i2;  // NON_COMPLIANT
+  i1 /= i2; // NON_COMPLIANT
+}
+
+void test_simple_div_no_zero(signed int i1, signed int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 / i2;  // NON_COMPLIANT
+    i1 /= i2; // NON_COMPLIANT
+  }
+}
+
+void test_div_precheck(signed int i1, signed int i2) {
+  if ((i2 == 0) || ((i1 == INT_MIN) && (i2 == -1))) {
+    /* Handle error */
+  } else {
+    i1 / i2;  // COMPLIANT
+    i1 /= i2; // COMPLIANT
+  }
+}
+
+void test_simple_rem(signed int i1, signed int i2) {
+  i1 % i2;  // NON_COMPLIANT
+  i1 %= i2; // NON_COMPLIANT
+}
+
+void test_simple_rem_no_zero(signed int i1, signed int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 % i2;  // NON_COMPLIANT
+    i1 %= i2; // NON_COMPLIANT
+  }
+}
+
+void test_rem_precheck(signed int i1, signed int i2) {
+  if ((i2 == 0) || ((i1 == INT_MIN) && (i2 == -1))) {
+    /* Handle error */
+  } else {
+    i1 % i2;  // COMPLIANT
+    i1 %= i2; // COMPLIANT
+  }
+}
+
+void test_simple_negate(signed int i1) {
+  -i1; // NON_COMPLIANT
+}
+
+void test_negate_precheck(signed int i1) {
+  if (i1 == INT_MIN) {
+    // handle error
+  } else {
+    -i1; // COMPLIANT
+  }
+}
+
+void test_inc(signed int i1) {
+  i1++; // NON_COMPLIANT
+}
+
+void test_inc_guard(signed int i1) {
+  if (i1 < INT_MAX) {
+    i1++; // COMPLIANT
+  }
+}
+
+void test_inc_loop_guard() {
+  for (signed int i1 = 0; i1 < 10; i1++) { // COMPLIANT
+    // ...
+  }
+}
+
+void test_dec(signed int i1) {
+  i1--; // NON_COMPLIANT
+}
+
+void test_dec_guard(signed int i1) {
+  if (i1 > INT_MIN) {
+    i1--; // COMPLIANT
+  }
+}
+
+void test_dec_loop_guard() {
+  for (signed int i1 = 10; i1 > 0; i1--) { // COMPLIANT
+    // ...
+  }
+}
\ No newline at end of file
diff --git a/c/cert/test/rules/INT33-C/DivOrRemByZero.expected b/c/cert/test/rules/INT33-C/DivOrRemByZero.expected
new file mode 100644
index 0000000000..66911a2ad6
--- /dev/null
+++ b/c/cert/test/rules/INT33-C/DivOrRemByZero.expected
@@ -0,0 +1,4 @@
+| test.c:4:3:4:9 | ... / ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:5:3:5:9 | ... % ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:12:5:12:11 | ... / ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:13:5:13:11 | ... % ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
diff --git a/c/cert/test/rules/INT33-C/DivOrRemByZero.qlref b/c/cert/test/rules/INT33-C/DivOrRemByZero.qlref
new file mode 100644
index 0000000000..c3144339c8
--- /dev/null
+++ b/c/cert/test/rules/INT33-C/DivOrRemByZero.qlref
@@ -0,0 +1 @@
+rules/INT33-C/DivOrRemByZero.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/INT33-C/test.c b/c/cert/test/rules/INT33-C/test.c
new file mode 100644
index 0000000000..2dd76580f0
--- /dev/null
+++ b/c/cert/test/rules/INT33-C/test.c
@@ -0,0 +1,33 @@
+#include <limits.h>
+
+void test_simple(signed int i1, signed int i2) {
+  i1 / i2; // NON_COMPLIANT
+  i1 % i2; // NON_COMPLIANT
+}
+
+void test_incomplete_check(signed int i1, signed int i2) {
+  if (i1 == INT_MIN && i2 == -1) {
+    // handle error
+  } else {
+    i1 / i2; // NON_COMPLIANT
+    i1 % i2; // NON_COMPLIANT
+  }
+}
+
+void test_complete_check(signed int i1, signed int i2) {
+  if (i2 == 0 || (i1 == INT_MIN && i2 == -1)) {
+    // handle error
+  } else {
+    i1 / i2; // COMPLIANT
+    i1 % i2; // COMPLIANT
+  }
+}
+
+void test_unsigned(unsigned int i1, unsigned int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 / i2; // COMPLIANT
+    i1 % i2; // COMPLIANT
+  }
+}
\ No newline at end of file
diff --git a/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.expected b/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.expected
new file mode 100644
index 0000000000..e43dc19077
--- /dev/null
+++ b/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.expected
@@ -0,0 +1,2 @@
+| test.c:11:12:11:31 | sizeof(unsigned int) | sizeof operator used to determine the precision of an integer type. |
+| test.c:27:25:27:42 | sizeof(signed int) | sizeof operator used to determine the precision of an integer type. |
diff --git a/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.qlref b/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.qlref
new file mode 100644
index 0000000000..c408baf78d
--- /dev/null
+++ b/c/cert/test/rules/INT35-C/UseCorrectIntegerPrecisions.qlref
@@ -0,0 +1 @@
+rules/INT35-C/UseCorrectIntegerPrecisions.ql
\ No newline at end of file
diff --git a/c/cert/test/rules/INT35-C/test.c b/c/cert/test/rules/INT35-C/test.c
new file mode 100644
index 0000000000..72bca5f8d8
--- /dev/null
+++ b/c/cert/test/rules/INT35-C/test.c
@@ -0,0 +1,40 @@
+#include <limits.h>
+#include <math.h>
+#include <stddef.h>
+#include <stdint.h>
+
+size_t popcount(uintmax_t num);
+
+#define PRECISION(umax_value) popcount(umax_value)
+
+void test_incorrect_precision_check(int e) {
+  if (e >= sizeof(unsigned int) * CHAR_BIT) { // NON_COMPLIANT
+    // handle error
+  } else {
+    1 << e;
+  }
+}
+
+void test_correct_precision_check(int e) {
+  if (e >= PRECISION(UINT_MAX)) { // COMPLIANT
+    /* Handle error */
+  } else {
+    1 << e;
+  }
+}
+
+void test_incorrect_precision_check_cast(float f) {
+  if (log2f(fabsf(f)) > sizeof(signed int) * CHAR_BIT) { // NON_COMPLIANT
+    // handle error
+  } else {
+    (signed int)f;
+  }
+}
+
+void test_correct_precision_check_cast(float f) {
+  if (log2f(fabsf(f)) > PRECISION(INT_MAX)) { // COMPLIANT
+    /* Handle error */
+  } else {
+    (signed int)f;
+  }
+}
\ No newline at end of file
diff --git a/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected b/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected
new file mode 100644
index 0000000000..614ad8a9de
--- /dev/null
+++ b/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected
@@ -0,0 +1,13 @@
+| test.c:11:7:11:18 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:12:7:12:18 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:18:7:18:19 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:19:7:19:19 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:25:7:25:18 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:26:7:26:17 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:33:7:33:20 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:34:7:34:20 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:40:7:40:19 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:41:7:41:19 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:47:7:47:18 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:48:7:48:17 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.c:53:20:53:31 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
diff --git a/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql b/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
new file mode 100644
index 0000000000..9fcc41c831
--- /dev/null
+++ b/c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
@@ -0,0 +1,2 @@
+// GENERATED FILE - DO NOT MODIFY
+import codingstandards.cpp.rules.constantunsignedintegerexpressionswraparound.ConstantUnsignedIntegerExpressionsWrapAround
diff --git a/c/common/test/rules/constantunsignedintegerexpressionswraparound/test.c b/c/common/test/rules/constantunsignedintegerexpressionswraparound/test.c
new file mode 100644
index 0000000000..a779b86b94
--- /dev/null
+++ b/c/common/test/rules/constantunsignedintegerexpressionswraparound/test.c
@@ -0,0 +1,55 @@
+#include <limits.h>
+
+// UINT_MIN and UULONG_MIN isn't defined, but it's going to be zero
+#define UINT_MIN ((unsigned int)0)
+#define UULONG_MIN ((unsigned long long)0)
+
+void test_unsigned_int() {
+  unsigned int a;
+  a = 1 + 1;        // COMPLIANT - signed integer
+  a = 0 - 1;        // COMPLIANT - signed integer
+  a = UINT_MIN - 1; // NON_COMPLIANT
+  a = UINT_MAX + 1; // NON_COMPLIANT
+
+  const unsigned int const_min = UINT_MIN;
+  const unsigned int const_max = UINT_MAX;
+  a = const_min + 1; // COMPLIANT
+  a = const_max - 1; // COMPLIANT
+  a = const_min - 1; // NON_COMPLIANT
+  a = const_max + 1; // NON_COMPLIANT
+
+#define UNDERFLOW(x) (UINT_MIN - (x))
+#define OVERFLOW(x) (UINT_MAX + (x))
+  a = UNDERFLOW(0); // COMPLIANT
+  a = OVERFLOW(0);  // COMPLIANT
+  a = UNDERFLOW(1); // NON_COMPLIANT
+  a = OVERFLOW(1);  // NON_COMPLIANT
+}
+
+void test_long_long() {
+  unsigned long long a;
+  a = 1 + 1;          // COMPLIANT
+  a = 0 - 1;          // COMPLIANT
+  a = UULONG_MIN - 1; // NON_COMPLIANT
+  a = ULLONG_MAX + 1; // NON_COMPLIANT
+
+  const unsigned long long const_min = UULONG_MIN;
+  const unsigned long long const_max = ULLONG_MAX;
+  a = const_min + 1; // COMPLIANT
+  a = const_max - 1; // COMPLIANT
+  a = const_min - 1; // NON_COMPLIANT
+  a = const_max + 1; // NON_COMPLIANT
+
+#define UNDERFLOW(x) (UULONG_MIN - (x))
+#define OVERFLOW(x) (ULLONG_MAX + (x))
+  a = UNDERFLOW(0); // COMPLIANT
+  a = OVERFLOW(0);  // COMPLIANT
+  a = UNDERFLOW(1); // NON_COMPLIANT
+  a = OVERFLOW(1);  // NON_COMPLIANT
+}
+
+void test_conversion() {
+  signed int a =
+      (signed int)(UINT_MAX + 1); // NON_COMPLIANT - still an unsigned integer
+                                  // constant expression
+}
\ No newline at end of file
diff --git a/c/misra/src/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.ql b/c/misra/src/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.ql
new file mode 100644
index 0000000000..b5d508dfe1
--- /dev/null
+++ b/c/misra/src/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.ql
@@ -0,0 +1,28 @@
+/**
+ * @id c/misra/constant-unsigned-integer-expressions-wrap-around
+ * @name RULE-12-4: Evaluation of constant expressions should not lead to unsigned integer wrap-around
+ * @description Unsigned integer expressions do not strictly overflow, but instead wrap around in a
+ *              modular way. Any constant unsigned integer expressions that in effect "overflow"
+ *              will not be detected by the compiler. Although there may be good reasons at run-time
+ *              to rely on the modular arithmetic provided by unsigned integer types, the reasons
+ *              for using it at compile-time to evaluate a constant expression are less obvious. Any
+ *              instance of an unsigned integer constant expression wrapping around is therefore
+ *              likely to indicate a programming error.
+ * @kind problem
+ * @precision very-high
+ * @problem.severity error
+ * @tags external/misra/id/rule-12-4
+ *       correctness
+ *       security
+ *       external/misra/obligation/advisory
+ */
+
+import cpp
+import codingstandards.c.misra
+import codingstandards.cpp.rules.constantunsignedintegerexpressionswraparound.ConstantUnsignedIntegerExpressionsWrapAround
+
+class ConstantUnsignedIntegerExpressionsWrapAroundQuery extends ConstantUnsignedIntegerExpressionsWrapAroundSharedQuery {
+  ConstantUnsignedIntegerExpressionsWrapAroundQuery() {
+    this = IntegerOverflowPackage::constantUnsignedIntegerExpressionsWrapAroundQuery()
+  }
+}
diff --git a/c/misra/test/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.testref b/c/misra/test/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.testref
new file mode 100644
index 0000000000..7e97e39764
--- /dev/null
+++ b/c/misra/test/rules/RULE-12-4/ConstantUnsignedIntegerExpressionsWrapAround.testref
@@ -0,0 +1 @@
+c/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
\ No newline at end of file
diff --git a/change_notes/2023-03-20-constant-integer-expression-wrap-casted.md b/change_notes/2023-03-20-constant-integer-expression-wrap-casted.md
new file mode 100644
index 0000000000..321fff714f
--- /dev/null
+++ b/change_notes/2023-03-20-constant-integer-expression-wrap-casted.md
@@ -0,0 +1,2 @@
+ * `M5-19-1`:
+   - Reduce false negatives by fixing a bug where a constant expression was immediately casted to a signed type.
\ No newline at end of file
diff --git a/change_notes/2023-03-27-integer-overflow.md b/change_notes/2023-03-27-integer-overflow.md
new file mode 100644
index 0000000000..8c86bae307
--- /dev/null
+++ b/change_notes/2023-03-27-integer-overflow.md
@@ -0,0 +1,4 @@
+ * `A4-7-1` - `IntegerExpressionLeadToDataLoss.ql` - reduce false positives and false negatives by:
+   - Identifying additional categories of valid guard.
+   - Excluding guards which were not proven to prevent overflow or underflow.
+   - Expand coverage to include unary operations and arithmetic assignment operations.
\ No newline at end of file
diff --git a/cpp/autosar/src/rules/A4-7-1/IntegerExpressionLeadToDataLoss.ql b/cpp/autosar/src/rules/A4-7-1/IntegerExpressionLeadToDataLoss.ql
index 242283d716..aae951351a 100644
--- a/cpp/autosar/src/rules/A4-7-1/IntegerExpressionLeadToDataLoss.ql
+++ b/cpp/autosar/src/rules/A4-7-1/IntegerExpressionLeadToDataLoss.ql
@@ -15,74 +15,20 @@
 
 import cpp
 import codingstandards.cpp.autosar
-import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import codingstandards.cpp.Overflow
 import semmle.code.cpp.controlflow.Guards
-import semmle.code.cpp.dataflow.TaintTracking
 import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 
-/**
- * A `BinaryArithmeticOperation` which may overflow and is a potentially interesting case to review
- * that is not covered by other queries for this rule.
- */
-class InterestingBinaryOverflowingExpr extends BinaryArithmeticOperation {
-  InterestingBinaryOverflowingExpr() {
-    // Might overflow or underflow
-    (
-      exprMightOverflowNegatively(this)
-      or
-      exprMightOverflowPositively(this)
-    ) and
-    not this.isAffectedByMacro() and
-    // Ignore pointer arithmetic
-    not this instanceof PointerArithmeticOperation and
-    // Covered by `IntMultToLong.ql` instead
-    not this instanceof MulExpr and
-    // Not covered by this query - overflow/underflow in division is rare
-    not this instanceof DivExpr
-  }
-
-  /**
-   * Get a `GVN` which guards this expression which may overflow.
-   */
-  GVN getAGuardingGVN() {
-    exists(GuardCondition gc, Expr e |
-      not gc = getABadOverflowCheck() and
-      TaintTracking::localTaint(DataFlow::exprNode(e), DataFlow::exprNode(gc.getAChild*())) and
-      gc.controls(this.getBasicBlock(), _) and
-      result = globalValueNumber(e)
-    )
-  }
-
-  /**
-   * Identifies a bad overflow check for this overflow expression.
-   */
-  GuardCondition getABadOverflowCheck() {
-    exists(AddExpr ae, RelationalOperation relOp |
-      this = ae and
-      result = relOp and
-      // Looking for this pattern:
-      // if (x + y > x)
-      //  use(x + y)
-      //
-      globalValueNumber(relOp.getAnOperand()) = globalValueNumber(ae) and
-      globalValueNumber(relOp.getAnOperand()) = globalValueNumber(ae.getAnOperand())
-    |
-      // Signed overflow checks are insufficient
-      ae.getUnspecifiedType().(IntegralType).isSigned()
-      or
-      // Unsigned overflow checks can still be bad, if the result is promoted.
-      forall(Expr op | op = ae.getAnOperand() | op.getType().getSize() < any(IntType i).getSize()) and
-      // Not explicitly converted to a smaller type before the comparison
-      not ae.getExplicitlyConverted().getType().getSize() < any(IntType i).getSize()
-    )
-  }
-}
-
-from InterestingBinaryOverflowingExpr e
+from InterestingOverflowingOperation e
 where
   not isExcluded(e, IntegerConversionPackage::integerExpressionLeadToDataLossQuery()) and
   // Not within a guard condition
   not exists(GuardCondition gc | gc.getAChild*() = e) and
   // Not guarded by a check, where the check is not an invalid overflow check
-  not e.getAGuardingGVN() = globalValueNumber(e.getAChild*())
+  not e.hasValidPreCheck() and
+  // Covered by `IntMultToLong.ql` instead
+  not e instanceof MulExpr and
+  // Not covered by this query - overflow/underflow in division is rare
+  not e instanceof DivExpr and
+  not e instanceof RemExpr
 select e, "Binary expression ..." + e.getOperator() + "... may overflow."
diff --git a/cpp/autosar/src/rules/A5-2-2/TraditionalCStyleCastsUsed.ql b/cpp/autosar/src/rules/A5-2-2/TraditionalCStyleCastsUsed.ql
index c769339d65..66a289dfe0 100644
--- a/cpp/autosar/src/rules/A5-2-2/TraditionalCStyleCastsUsed.ql
+++ b/cpp/autosar/src/rules/A5-2-2/TraditionalCStyleCastsUsed.ql
@@ -15,6 +15,7 @@
 
 import cpp
 import codingstandards.cpp.autosar
+import codingstandards.cpp.Macro
 
 /**
  * Gets the macro (if any) that generated the given `CStyleCast`.
@@ -34,16 +35,6 @@ Macro getGeneratedFrom(CStyleCast c) {
   )
 }
 
-/** A macro within the source location of this project. */
-class UserProvidedMacro extends Macro {
-  UserProvidedMacro() { exists(this.getFile().getRelativePath()) }
-}
-
-/** A macro defined within a library used by this project. */
-class LibraryMacro extends Macro {
-  LibraryMacro() { not this instanceof UserProvidedMacro }
-}
-
 /*
  * In theory this query should exclude casts using the "functional notation" syntax, e.g.
  * ```
diff --git a/cpp/autosar/src/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.ql b/cpp/autosar/src/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.ql
index 2ce54f07e1..221651b9b4 100644
--- a/cpp/autosar/src/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.ql
+++ b/cpp/autosar/src/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.ql
@@ -21,12 +21,10 @@
 
 import cpp
 import codingstandards.cpp.autosar
-import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import codingstandards.cpp.rules.constantunsignedintegerexpressionswraparound.ConstantUnsignedIntegerExpressionsWrapAround
 
-from BinaryArithmeticOperation bao
-where
-  not isExcluded(bao, ExpressionsPackage::constantUnsignedIntegerExpressionsWrapAroundQuery()) and
-  bao.isConstant() and
-  bao.getFullyConverted().getUnderlyingType().(IntegralType).isUnsigned() and
-  convertedExprMightOverflow(bao)
-select bao, "Use of a constant, unsigned, integer expression that over- or under-flows."
+class ConstantUnsignedIntegerExpressionsWrapAroundQuery extends ConstantUnsignedIntegerExpressionsWrapAroundSharedQuery {
+  ConstantUnsignedIntegerExpressionsWrapAroundQuery() {
+    this = ExpressionsPackage::constantUnsignedIntegerExpressionsWrapAroundQuery()
+  }
+}
diff --git a/cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected b/cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected
index d9c69bad90..17153b5a5b 100644
--- a/cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected
+++ b/cpp/autosar/test/rules/A4-7-1/IntegerExpressionLeadToDataLoss.expected
@@ -8,4 +8,5 @@
 | IntMultToLongc.cpp:109:13:109:28 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:2:10:2:14 | ... + ... | Binary expression ...+... may overflow. |
 | test.cpp:22:12:22:16 | ... + ... | Binary expression ...+... may overflow. |
-| test.cpp:52:7:52:14 | ... + ... | Binary expression ...+... may overflow. |
+| test.cpp:50:7:50:14 | ... + ... | Binary expression ...+... may overflow. |
+| test.cpp:62:8:62:10 | ... ++ | Binary expression ...++... may overflow. |
diff --git a/cpp/autosar/test/rules/A4-7-1/test.cpp b/cpp/autosar/test/rules/A4-7-1/test.cpp
index 9527155618..7f6cbb7abe 100644
--- a/cpp/autosar/test/rules/A4-7-1/test.cpp
+++ b/cpp/autosar/test/rules/A4-7-1/test.cpp
@@ -35,21 +35,31 @@ short test_addition_invalid_overflow_check(short x, short y) {
   return 0;
 }
 
-void test_addition_loop_bound(unsigned int base, unsigned int size) {
-  if (size > 0) {
-    int n = size - 1;
-    for (int i = 0; i < n; i++) {
-      base + i; // COMPLIANT - `i` is bounded
+void test_addition_loop_bound(unsigned short base, unsigned int n) {
+  if (n < 1000) {
+    for (unsigned int i = 0; i < n; i++) { // COMPLIANT
+      base + i;                            // COMPLIANT - `i` is bounded
     }
   }
 }
 
-void test_addition_invalid_loop_bound(unsigned int base, unsigned int j,
-                                      unsigned int size) {
-  if (size > 0) {
-    int n = size - 1;
-    for (int i = 0; i < n; i++) {
+void test_addition_invalid_loop_bound(unsigned short base, unsigned int j,
+                                      unsigned int n) {
+  if (n < 1000) {
+    for (unsigned int i = 0; i < n; i++) { // COMPLIANT
       base + j; // NON_COMPLIANT - guards are not related
     }
   }
+}
+
+void test_loop_bound(unsigned int n) {
+  for (unsigned int i = 0; i < n; i++) { // COMPLIANT
+  }
+}
+
+void test_loop_bound_bad(unsigned int n) {
+  for (unsigned short i = 0; i < n;
+       i++) { // NON_COMPLIANT - crement will overflow before loop bound is
+              // reached
+  }
 }
\ No newline at end of file
diff --git a/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.qlref b/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.qlref
deleted file mode 100644
index 5531830cbc..0000000000
--- a/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.qlref
+++ /dev/null
@@ -1 +0,0 @@
-rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.ql
\ No newline at end of file
diff --git a/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.testref b/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.testref
new file mode 100644
index 0000000000..9d56f5d242
--- /dev/null
+++ b/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.testref
@@ -0,0 +1 @@
+cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
\ No newline at end of file
diff --git a/cpp/common/src/codingstandards/cpp/Macro.qll b/cpp/common/src/codingstandards/cpp/Macro.qll
index cb1231e04f..65d0321271 100644
--- a/cpp/common/src/codingstandards/cpp/Macro.qll
+++ b/cpp/common/src/codingstandards/cpp/Macro.qll
@@ -68,3 +68,22 @@ pragma[noinline]
 predicate isMacroInvocationLocation(MacroInvocation mi, File f, int startChar, int endChar) {
   mi.getActualLocation().charLoc(f, startChar, endChar)
 }
+
+/** A macro within the source location of this project. */
+class UserProvidedMacro extends Macro {
+  UserProvidedMacro() {
+    exists(this.getFile().getRelativePath()) and
+    // Exclude macros in our standard library header stubs for tests, because qltest sets the source
+    // root to the qlpack root, which means our stubs all look like source files.
+    //
+    // This may affect "real" code as well, if it happens to be at this path, but given the name
+    // I think it's likely that we'd want that to be the case anyway.
+    not this.getFile().getRelativePath().substring(0, "includes/standard-library".length()) =
+      "includes/standard-library"
+  }
+}
+
+/** A macro defined within a library used by this project. */
+class LibraryMacro extends Macro {
+  LibraryMacro() { not this instanceof UserProvidedMacro }
+}
diff --git a/cpp/common/src/codingstandards/cpp/Overflow.qll b/cpp/common/src/codingstandards/cpp/Overflow.qll
new file mode 100644
index 0000000000..c5461eb8ab
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/Overflow.qll
@@ -0,0 +1,422 @@
+/**
+ * This module provides predicates for checking whether an operation overflows or wraps.
+ */
+
+import cpp
+import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import SimpleRangeAnalysisCustomizations
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.dataflow.TaintTracking
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+/**
+ * An operation that may overflow or underflow.
+ */
+class InterestingOverflowingOperation extends Operation {
+  InterestingOverflowingOperation() {
+    // Might overflow or underflow
+    (
+      exprMightOverflowNegatively(this)
+      or
+      exprMightOverflowPositively(this)
+      or
+      // Division and remainder are not handled by the library
+      exists(DivOrRemOperation divOrRem | divOrRem = this |
+        // The right hand side could be -1
+        upperBound(divOrRem.getDivisor()) >= -1.0 and
+        lowerBound(divOrRem.getDivisor()) <= -1.0 and
+        // The left hand side could be the smallest possible integer value
+        lowerBound(divOrRem.getDividend()) <=
+          typeLowerBound(divOrRem.getDividend().getType().getUnderlyingType())
+      )
+    ) and
+    // Multiplication is not covered by the standard range analysis library, so implement our own
+    // mini analysis.
+    (this instanceof MulExpr implies MulExprAnalysis::overflows(this)) and
+    // This shouldn't be a "safe" crement operation
+    not LoopCounterAnalysis::isCrementSafeFromOverflow(this) and
+    // Not within a macro
+    not this.isAffectedByMacro() and
+    // Ignore pointer arithmetic
+    not this instanceof PointerArithmeticOperation
+  }
+
+  /**
+   * Holds if there is a correct validity check after this expression which may overflow.
+   */
+  predicate hasValidPreCheck() {
+    // For binary operations (both arithmetic operations and arithmetic assignment operations)
+    exists(GVN i1, GVN i2, Expr op1, Expr op2 |
+      op1 = getAnOperand() and
+      op2 = getAnOperand() and
+      not op1 = op2 and
+      i1 = globalValueNumber(op1) and
+      i2 = globalValueNumber(op2)
+    |
+      // For unsigned integer addition, look for this pattern:
+      // if (x + y > x)
+      //  use(x + y)
+      // Ensuring it is not a bad overflow check
+      (this instanceof AddExpr or this instanceof AssignAddExpr) and
+      this.getType().getUnspecifiedType().(IntegralType).isUnsigned() and
+      exists(AddExpr ae, RelationalOperation relOp |
+        globalValueNumber(relOp.getAnOperand()) = i1 and
+        relOp.getAnOperand() = ae and
+        globalValueNumber(ae.getAnOperand()) = i1 and
+        globalValueNumber(ae.getAnOperand()) = i2
+      |
+        // At least one operand is not smaller than int
+        exists(Expr op | op = ae.getAnOperand() |
+          op.getType().getSize() >= any(IntType i).getSize()
+        )
+        or
+        // The result of the addition is explicitly converted to a smaller type before the comparison
+        ae.getExplicitlyConverted().getType().getSize() < any(IntType i).getSize()
+      )
+      or
+      // Match this pattern for checking for unsigned integer overflow on add
+      // if (UINT_MAX - i1 < i2)
+      (this instanceof AddExpr or this instanceof AssignAddExpr) and
+      this.getType().getUnspecifiedType().(IntegralType).isUnsigned() and
+      exists(SubExpr se, RelationalOperation relOp |
+        globalValueNumber(relOp.getGreaterOperand()) = i2 and
+        relOp.getAnOperand() = se and
+        globalValueNumber(se.getRightOperand()) = i1 and
+        se.getLeftOperand().getValue().toFloat() = typeUpperBound(getType())
+      )
+      or
+      // Match this pattern for checking for unsigned integer underflow on subtract
+      // if (i1 < i2)
+      (this instanceof SubExpr or this instanceof AssignSubExpr) and
+      this.getType().getUnspecifiedType().(IntegralType).isUnsigned() and
+      exists(RelationalOperation relOp |
+        globalValueNumber(relOp.getGreaterOperand()) = i2 and
+        globalValueNumber(relOp.getLesserOperand()) = i1
+      )
+      or
+      // The CERT rule for signed integer overflow has a very specific pattern it recommends
+      // for checking for overflow. We try to match the pattern here.
+      //   ((i2 > 0 && i1 > (INT_MAX - i2)) || (i2 < 0 && i1 < (INT_MIN - i2)))
+      (this instanceof AddExpr or this instanceof AssignAddExpr) and
+      exists(LogicalOrExpr orExpr |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        bbDominates(orExpr.getBasicBlock(), this.getBasicBlock()) and
+        exists(LogicalAndExpr andExpr |
+          andExpr = orExpr.getAnOperand() and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getLesserOperand().getValue() = "0" and
+            globalValueNumber(gt.getGreaterOperand()) = i2
+          ) and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getLesserOperand() =
+              any(SubExpr se |
+                se.getLeftOperand().getValue().toFloat() = typeUpperBound(getType()) and
+                globalValueNumber(se.getRightOperand()) = i2
+              ) and
+            globalValueNumber(gt.getGreaterOperand()) = i1
+          )
+        ) and
+        exists(LogicalAndExpr andExpr |
+          andExpr = orExpr.getAnOperand() and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getGreaterOperand().getValue() = "0" and
+            globalValueNumber(gt.getLesserOperand()) = i2
+          ) and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getGreaterOperand() =
+              any(SubExpr se |
+                se.getLeftOperand().getValue().toFloat() = typeLowerBound(getType()) and
+                globalValueNumber(se.getRightOperand()) = i2
+              ) and
+            globalValueNumber(gt.getLesserOperand()) = i1
+          )
+        )
+      )
+      or
+      // The CERT rule for signed integer overflow has a very specific pattern it recommends
+      // for checking for underflow. We try to match the pattern here.
+      //   ((i2 > 0 && i1 > (INT_MIN + i2)) || (i2 < 0 && i1 < (INT_MAX + i2)))
+      (this instanceof SubExpr or this instanceof AssignSubExpr) and
+      exists(LogicalOrExpr orExpr |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        bbDominates(orExpr.getBasicBlock(), this.getBasicBlock()) and
+        exists(LogicalAndExpr andExpr |
+          andExpr = orExpr.getAnOperand() and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getLesserOperand().getValue() = "0" and
+            globalValueNumber(gt.getGreaterOperand()) = i2
+          ) and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getGreaterOperand() =
+              any(AddExpr se |
+                se.getLeftOperand().getValue().toFloat() = typeLowerBound(getType()) and
+                globalValueNumber(se.getRightOperand()) = i2
+              ) and
+            globalValueNumber(gt.getLesserOperand()) = i1
+          )
+        ) and
+        exists(LogicalAndExpr andExpr |
+          andExpr = orExpr.getAnOperand() and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getGreaterOperand().getValue() = "0" and
+            globalValueNumber(gt.getLesserOperand()) = i2
+          ) and
+          exists(StrictRelationalOperation gt |
+            gt = andExpr.getAnOperand() and
+            gt.getLesserOperand() =
+              any(AddExpr se |
+                se.getLeftOperand().getValue().toFloat() = typeUpperBound(getType()) and
+                globalValueNumber(se.getRightOperand()) = i2
+              ) and
+            globalValueNumber(gt.getGreaterOperand()) = i1
+          )
+        )
+      )
+      or
+      // CERT recommends checking for divisor != -1 and dividor != INT_MIN
+      this instanceof DivOrRemOperation and
+      exists(EqualityOperation eop |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        globalValueNumber(eop.getAnOperand()) = i1 and
+        eop.getAnOperand().getValue().toFloat() =
+          typeLowerBound(this.(DivOrRemOperation).getDividend().getType().getUnderlyingType())
+      ) and
+      exists(EqualityOperation eop |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        globalValueNumber(eop.getAnOperand()) = i2 and
+        eop.getAnOperand().getValue().toInt() = -1
+      )
+      or
+      // The CERT rule for signed integer overflow has a very specific pattern it recommends
+      // for checking for multiplication underflow/overflow. We just use a heuristic here,
+      // which determines if at least 4 checks of the sort `a < INT_MAX / b` are present in the code.
+      (this instanceof MulExpr or this instanceof AssignMulExpr) and
+      count(StrictRelationalOperation rel |
+        globalValueNumber(rel.getAnOperand()) = i1 and
+        globalValueNumber(rel.getAnOperand().(DivExpr).getRightOperand()) = i2
+        or
+        globalValueNumber(rel.getAnOperand()) = i2 and
+        globalValueNumber(rel.getAnOperand().(DivExpr).getRightOperand()) = i1
+      ) >= 4
+    )
+  }
+
+  /**
+   * Holds if there is a correct validity check after this expression which may overflow.
+   *
+   * Only holds for unsigned expressions, as signed overflow/underflow are undefined behavior.
+   */
+  predicate hasValidPostCheck() { exists(getAValidPostCheck()) }
+
+  /**
+   * Gets a correct validity check, `gc`, after this expression which may overflow.
+   */
+  GuardCondition getAValidPostCheck() {
+    this.getType().(IntegralType).isUnsigned() and
+    (
+      exists(RelationalOperation ro |
+        DataFlow::localExprFlow(this, ro.getLesserOperand()) and
+        globalValueNumber(ro.getGreaterOperand()) = globalValueNumber(this.getAnOperand()) and
+        (this instanceof AddExpr or this instanceof AssignAddExpr) and
+        result = ro
+      )
+      or
+      exists(RelationalOperation ro |
+        DataFlow::localExprFlow(this, ro.getGreaterOperand()) and
+        globalValueNumber(ro.getLesserOperand()) = globalValueNumber(this.getAnOperand()) and
+        (this instanceof SubExpr or this instanceof AssignSubExpr) and
+        result = ro
+      )
+    )
+  }
+}
+
+private class StrictRelationalOperation extends RelationalOperation {
+  StrictRelationalOperation() { this.getOperator() = [">", "<"] }
+}
+
+class DivOrRemOperation extends Operation {
+  DivOrRemOperation() {
+    this instanceof DivExpr or
+    this instanceof RemExpr or
+    this instanceof AssignDivExpr or
+    this instanceof AssignRemExpr
+  }
+
+  Expr getDividend() {
+    result = this.(BinaryOperation).getLeftOperand() or
+    result = this.(AssignArithmeticOperation).getLValue()
+  }
+
+  Expr getDivisor() {
+    result = this.(BinaryOperation).getRightOperand() or
+    result = this.(AssignArithmeticOperation).getRValue()
+  }
+}
+
+/**
+ * Module inspired by the IntMultToLong.ql query.
+ */
+private module MulExprAnalysis {
+  /**
+   * As SimpleRangeAnalysis does not support reasoning about multiplication
+   * we create a tiny abstract interpreter for handling multiplication, which
+   * we invoke only after weeding out of all of trivial cases that we do
+   * not care about. By default, the maximum and minimum values are computed
+   * using SimpleRangeAnalysis.
+   */
+  class AnalyzableExpr extends Expr {
+    AnalyzableExpr() {
+      // A integer multiplication, or an expression within an integral expression
+      this.(MulExpr).getType().getUnspecifiedType() instanceof IntegralType or
+      this.getParent() instanceof AnalyzableExpr or
+      this.(Conversion).getExpr() instanceof AnalyzableExpr
+    }
+
+    float maxValue() { result = upperBound(this.getFullyConverted()) }
+
+    float minValue() { result = lowerBound(this.getFullyConverted()) }
+  }
+
+  class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr {
+    override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
+
+    override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
+  }
+
+  class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
+    override float maxValue() {
+      exists(float x1, float y1, float x2, float y2 |
+        x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+        x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+        y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+        y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+        result = (x1 * y1).maximum(x1 * y2).maximum(x2 * y1).maximum(x2 * y2)
+      )
+    }
+
+    override float minValue() {
+      exists(float x1, float x2, float y1, float y2 |
+        x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+        x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+        y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
+        y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
+        result = (x1 * y1).minimum(x1 * y2).minimum(x2 * y1).minimum(x2 * y2)
+      )
+    }
+  }
+
+  /**
+   * Analyze add expressions directly. This handles the case where an add expression is contributed to
+   * by a multiplication.
+   */
+  class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
+    override float maxValue() {
+      result =
+        this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() +
+          this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
+    }
+
+    override float minValue() {
+      result =
+        this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() +
+          this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
+    }
+  }
+
+  /**
+   * Analyze sub expressions directly. This handles the case where a sub expression is contributed to
+   * by a multiplication.
+   */
+  class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
+    override float maxValue() {
+      result =
+        this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() -
+          this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
+    }
+
+    override float minValue() {
+      result =
+        this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() -
+          this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
+    }
+  }
+
+  predicate overflows(MulExpr me) {
+    me.(MulAnalyzableExpr).maxValue() > exprMaxVal(me)
+    or
+    me.(MulAnalyzableExpr).minValue() < exprMinVal(me)
+  }
+}
+
+/**
+ * An analysis on safe loop counters.
+ */
+module LoopCounterAnalysis {
+  newtype LoopBound =
+    LoopUpperBound() or
+    LoopLowerBound()
+
+  predicate isLoopBounded(
+    CrementOperation cop, ForStmt fs, Variable loopCounter, Expr initializer, Expr counterBound,
+    LoopBound boundKind, boolean equals
+  ) {
+    // Initialization sets the loop counter
+    (
+      loopCounter = fs.getInitialization().(DeclStmt).getADeclaration() and
+      initializer = loopCounter.getInitializer().getExpr()
+      or
+      loopCounter.getAnAssignment() = initializer and
+      initializer = fs.getInitialization().(ExprStmt).getExpr()
+    ) and
+    // Condition is a relation operation on the loop counter
+    exists(RelationalOperation relOp |
+      fs.getCondition() = relOp and
+      (if relOp.getOperator().charAt(1) = "=" then equals = true else equals = false)
+    |
+      relOp.getGreaterOperand() = loopCounter.getAnAccess() and
+      relOp.getLesserOperand() = counterBound and
+      cop instanceof DecrementOperation and
+      boundKind = LoopLowerBound()
+      or
+      relOp.getLesserOperand() = loopCounter.getAnAccess() and
+      relOp.getGreaterOperand() = counterBound and
+      cop instanceof IncrementOperation and
+      boundKind = LoopUpperBound()
+    ) and
+    // Update is a crement operation with the loop counter
+    fs.getUpdate() = cop and
+    cop.getOperand() = loopCounter.getAnAccess()
+  }
+
+  /**
+   * Holds if the crement operation is safe from under/overflow.
+   */
+  predicate isCrementSafeFromOverflow(CrementOperation op) {
+    exists(
+      Expr initializer, Expr counterBound, LoopBound boundKind, boolean equals, int equalsOffset
+    |
+      isLoopBounded(op, _, _, initializer, counterBound, boundKind, equals) and
+      (
+        equals = true and equalsOffset = 1
+        or
+        equals = false and equalsOffset = 0
+      )
+    |
+      boundKind = LoopUpperBound() and
+      // upper bound of the inccrement is smaller than the maximum value representable in the type
+      upperBound(counterBound) + equalsOffset <= typeUpperBound(op.getType().getUnspecifiedType())
+      or
+      // the lower bound of the decrement is larger than the smal
+      boundKind = LoopLowerBound() and
+      lowerBound(counterBound) - equalsOffset >= typeLowerBound(op.getType().getUnspecifiedType())
+    )
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/IntegerOverflow.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/IntegerOverflow.qll
new file mode 100644
index 0000000000..9a74132a55
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/IntegerOverflow.qll
@@ -0,0 +1,112 @@
+//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY.  **/
+import cpp
+import RuleMetadata
+import codingstandards.cpp.exclusions.RuleMetadata
+
+newtype IntegerOverflowQuery =
+  TUnsignedIntegerOperationsWrapAroundQuery() or
+  TIntegerConversionCausesDataLossQuery() or
+  TSignedIntegerOverflowQuery() or
+  TDivOrRemByZeroQuery() or
+  TUseCorrectIntegerPrecisionsQuery() or
+  TConstantUnsignedIntegerExpressionsWrapAroundQuery()
+
+predicate isIntegerOverflowQueryMetadata(Query query, string queryId, string ruleId, string category) {
+  query =
+    // `Query` instance for the `unsignedIntegerOperationsWrapAround` query
+    IntegerOverflowPackage::unsignedIntegerOperationsWrapAroundQuery() and
+  queryId =
+    // `@id` for the `unsignedIntegerOperationsWrapAround` query
+    "c/cert/unsigned-integer-operations-wrap-around" and
+  ruleId = "INT30-C" and
+  category = "rule"
+  or
+  query =
+    // `Query` instance for the `integerConversionCausesDataLoss` query
+    IntegerOverflowPackage::integerConversionCausesDataLossQuery() and
+  queryId =
+    // `@id` for the `integerConversionCausesDataLoss` query
+    "c/cert/integer-conversion-causes-data-loss" and
+  ruleId = "INT31-C" and
+  category = "rule"
+  or
+  query =
+    // `Query` instance for the `signedIntegerOverflow` query
+    IntegerOverflowPackage::signedIntegerOverflowQuery() and
+  queryId =
+    // `@id` for the `signedIntegerOverflow` query
+    "c/cert/signed-integer-overflow" and
+  ruleId = "INT32-C" and
+  category = "rule"
+  or
+  query =
+    // `Query` instance for the `divOrRemByZero` query
+    IntegerOverflowPackage::divOrRemByZeroQuery() and
+  queryId =
+    // `@id` for the `divOrRemByZero` query
+    "c/cert/div-or-rem-by-zero" and
+  ruleId = "INT33-C" and
+  category = "rule"
+  or
+  query =
+    // `Query` instance for the `useCorrectIntegerPrecisions` query
+    IntegerOverflowPackage::useCorrectIntegerPrecisionsQuery() and
+  queryId =
+    // `@id` for the `useCorrectIntegerPrecisions` query
+    "c/cert/use-correct-integer-precisions" and
+  ruleId = "INT35-C" and
+  category = "rule"
+  or
+  query =
+    // `Query` instance for the `constantUnsignedIntegerExpressionsWrapAround` query
+    IntegerOverflowPackage::constantUnsignedIntegerExpressionsWrapAroundQuery() and
+  queryId =
+    // `@id` for the `constantUnsignedIntegerExpressionsWrapAround` query
+    "c/misra/constant-unsigned-integer-expressions-wrap-around" and
+  ruleId = "RULE-12-4" and
+  category = "advisory"
+}
+
+module IntegerOverflowPackage {
+  Query unsignedIntegerOperationsWrapAroundQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `unsignedIntegerOperationsWrapAround` query
+      TQueryC(TIntegerOverflowPackageQuery(TUnsignedIntegerOperationsWrapAroundQuery()))
+  }
+
+  Query integerConversionCausesDataLossQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `integerConversionCausesDataLoss` query
+      TQueryC(TIntegerOverflowPackageQuery(TIntegerConversionCausesDataLossQuery()))
+  }
+
+  Query signedIntegerOverflowQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `signedIntegerOverflow` query
+      TQueryC(TIntegerOverflowPackageQuery(TSignedIntegerOverflowQuery()))
+  }
+
+  Query divOrRemByZeroQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `divOrRemByZero` query
+      TQueryC(TIntegerOverflowPackageQuery(TDivOrRemByZeroQuery()))
+  }
+
+  Query useCorrectIntegerPrecisionsQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `useCorrectIntegerPrecisions` query
+      TQueryC(TIntegerOverflowPackageQuery(TUseCorrectIntegerPrecisionsQuery()))
+  }
+
+  Query constantUnsignedIntegerExpressionsWrapAroundQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `constantUnsignedIntegerExpressionsWrapAround` query
+      TQueryC(TIntegerOverflowPackageQuery(TConstantUnsignedIntegerExpressionsWrapAroundQuery()))
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
index d3c2f271a4..dc5e9aa34b 100644
--- a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
@@ -31,6 +31,7 @@ import IO1
 import IO2
 import IO3
 import IO4
+import IntegerOverflow
 import InvalidMemory1
 import Language1
 import Language2
@@ -92,6 +93,7 @@ newtype TCQuery =
   TIO2PackageQuery(IO2Query q) or
   TIO3PackageQuery(IO3Query q) or
   TIO4PackageQuery(IO4Query q) or
+  TIntegerOverflowPackageQuery(IntegerOverflowQuery q) or
   TInvalidMemory1PackageQuery(InvalidMemory1Query q) or
   TLanguage1PackageQuery(Language1Query q) or
   TLanguage2PackageQuery(Language2Query q) or
@@ -153,6 +155,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
   isIO2QueryMetadata(query, queryId, ruleId, category) or
   isIO3QueryMetadata(query, queryId, ruleId, category) or
   isIO4QueryMetadata(query, queryId, ruleId, category) or
+  isIntegerOverflowQueryMetadata(query, queryId, ruleId, category) or
   isInvalidMemory1QueryMetadata(query, queryId, ruleId, category) or
   isLanguage1QueryMetadata(query, queryId, ruleId, category) or
   isLanguage2QueryMetadata(query, queryId, ruleId, category) or
diff --git a/cpp/common/src/codingstandards/cpp/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.qll b/cpp/common/src/codingstandards/cpp/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.qll
new file mode 100644
index 0000000000..71b06a4662
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.qll
@@ -0,0 +1,38 @@
+/**
+ * Provides a library which includes a `problems` predicate for reporting unsigned integer
+ * wraparound related to constant expressions.
+ */
+
+import cpp
+import codingstandards.cpp.Customizations
+import codingstandards.cpp.Macro
+import codingstandards.cpp.Exclusions
+import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+
+abstract class ConstantUnsignedIntegerExpressionsWrapAroundSharedQuery extends Query { }
+
+Query getQuery() { result instanceof ConstantUnsignedIntegerExpressionsWrapAroundSharedQuery }
+
+query predicate problems(BinaryArithmeticOperation bao, string message) {
+  not isExcluded(bao, getQuery()) and
+  bao.isConstant() and
+  bao.getUnderlyingType().(IntegralType).isUnsigned() and
+  convertedExprMightOverflow(bao) and
+  // Exclude expressions generated from macro invocations of argument-less macros in third party
+  // code. This is because these are not under the control of the developer. Macros with arguments
+  // are not excluded, so that we can report cases where the argument provided by the developer
+  // wraps around (this may also report cases where the macro itself contains a wrapping expression,
+  // but we cannot distinguish these cases because we don't know which generated expressions are
+  // affected by which arguments).
+  //
+  // This addresses a false positive in the test cases on UULONG_MAX, which is reported in MUSL
+  // because it is defined as (2ULL*LLONG_MAX+1), which is a constant integer expression, and
+  // although it doesn't wrap in practice, our range analysis loses precision at the top end of the
+  // unsigned long long range so incorrectly assumes it can wrap.
+  not exists(LibraryMacro m, MacroInvocation mi |
+    mi = m.getAnInvocation() and
+    mi.getAnExpandedElement() = bao and
+    not exists(mi.getUnexpandedArgument(_))
+  ) and
+  message = "Use of a constant, unsigned, integer expression that over- or under-flows."
+}
diff --git a/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.expected b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected
similarity index 94%
rename from cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.expected
rename to cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected
index 89bf61f701..9b9718a09a 100644
--- a/cpp/autosar/test/rules/M5-19-1/ConstantUnsignedIntegerExpressionsWrapAround.expected
+++ b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.expected
@@ -14,3 +14,4 @@
 | test.cpp:59:7:59:17 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
 | test.cpp:63:7:63:45 | ... - ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
 | test.cpp:64:7:64:45 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
+| test.cpp:69:20:69:31 | ... + ... | Use of a constant, unsigned, integer expression that over- or under-flows. |
diff --git a/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
new file mode 100644
index 0000000000..9fcc41c831
--- /dev/null
+++ b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/ConstantUnsignedIntegerExpressionsWrapAround.ql
@@ -0,0 +1,2 @@
+// GENERATED FILE - DO NOT MODIFY
+import codingstandards.cpp.rules.constantunsignedintegerexpressionswraparound.ConstantUnsignedIntegerExpressionsWrapAround
diff --git a/cpp/autosar/test/rules/M5-19-1/test.cpp b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/test.cpp
similarity index 91%
rename from cpp/autosar/test/rules/M5-19-1/test.cpp
rename to cpp/common/test/rules/constantunsignedintegerexpressionswraparound/test.cpp
index 215c99bb30..52e6e1ffa1 100644
--- a/cpp/autosar/test/rules/M5-19-1/test.cpp
+++ b/cpp/common/test/rules/constantunsignedintegerexpressionswraparound/test.cpp
@@ -9,7 +9,7 @@ template <typename T> constexpr T constexpr_max() {
   return std::numeric_limits<T>::max();
 }
 
-void test_signed_int() {
+void test_unsigned_int() {
   unsigned int a;
   a = 1 + 1;                                        // COMPLIANT
   a = 0 - 1;                                        // COMPLIANT
@@ -62,4 +62,10 @@ void test_long_long() {
   a = constexpr_max<unsigned long long>() - 1; // COMPLIANT
   a = constexpr_min<unsigned long long>() - 1; // NON_COMPLIANT
   a = constexpr_max<unsigned long long>() + 1; // NON_COMPLIANT
+}
+
+void test_conversion() {
+  signed int a =
+      (signed int)(UINT_MAX + 1); // NON_COMPLIANT - still an unsigned integer
+                                  // constant expression
 }
\ No newline at end of file
diff --git a/rule_packages/c/IntegerOverflow.json b/rule_packages/c/IntegerOverflow.json
new file mode 100644
index 0000000000..5edc90eb21
--- /dev/null
+++ b/rule_packages/c/IntegerOverflow.json
@@ -0,0 +1,124 @@
+{
+  "CERT-C": {
+    "INT30-C": {
+      "properties": {
+        "obligation": "rule"
+      },
+      "queries": [
+        {
+          "description": "Unsigned integer expressions do not strictly overflow, but instead wrap around in a modular way. If the size of the type is not sufficient, this can happen unexpectedly.",
+          "kind": "problem",
+          "name": "Ensure that unsigned integer operations do not wrap",
+          "precision": "medium",
+          "severity": "error",
+          "short_name": "UnsignedIntegerOperationsWrapAround",
+          "tags": [
+            "correctness",
+            "security"
+          ]
+        }
+      ],
+      "title": "Ensure that unsigned integer operations do not wrap"
+    },
+    "INT31-C": {
+      "properties": {
+        "obligation": "rule"
+      },
+      "queries": [
+        {
+          "description": "Converting an integer value to another integer type with a different sign or size can lead to data loss or misinterpretation of the value.",
+          "kind": "problem",
+          "name": "Ensure that integer conversions do not result in lost or misinterpreted data",
+          "precision": "medium",
+          "severity": "error",
+          "short_name": "IntegerConversionCausesDataLoss",
+          "tags": [
+            "correctness"
+          ]
+        }
+      ],
+      "title": "Ensure that integer conversions do not result in lost or misinterpreted data"
+    },
+    "INT32-C": {
+      "properties": {
+        "obligation": "rule"
+      },
+      "queries": [
+        {
+          "description": "The multiplication of two signed integers can lead to underflow or overflow and therefore undefined behavior.",
+          "kind": "problem",
+          "name": "Ensure that operations on signed integers do not result in overflow",
+          "precision": "medium",
+          "severity": "error",
+          "short_name": "SignedIntegerOverflow",
+          "tags": [
+            "correctness",
+            "security"
+          ]
+        }
+      ],
+      "title": "Ensure that operations on signed integers do not result in overflow"
+    },
+    "INT33-C": {
+      "properties": {
+        "obligation": "rule"
+      },
+      "queries": [
+        {
+          "description": "Dividing or taking the remainder by zero is undefined behavior.",
+          "kind": "problem",
+          "name": "Ensure that division and remainder operations do not result in divide-by-zero errors",
+          "precision": "medium",
+          "severity": "error",
+          "short_name": "DivOrRemByZero",
+          "tags": [
+            "correctness"
+          ]
+        }
+      ],
+      "title": "Ensure that division and remainder operations do not result in divide-by-zero errors"
+    },
+    "INT35-C": {
+      "properties": {
+        "obligation": "rule"
+      },
+      "queries": [
+        {
+          "description": "The precision of integer types in C cannot be deduced from the size of the type (due to padding and sign bits) otherwise a loss of data may occur.",
+          "kind": "problem",
+          "name": "Use correct integer precisions",
+          "precision": "high",
+          "severity": "error",
+          "short_name": "UseCorrectIntegerPrecisions",
+          "tags": [
+            "correctness"
+          ]
+        }
+      ],
+      "title": "Use correct integer precisions"
+    }
+  },
+  "MISRA-C-2012": {
+    "RULE-12-4": {
+      "properties": {
+        "obligation": "advisory"
+      },
+      "queries": [
+        {
+          "description": "Unsigned integer expressions do not strictly overflow, but instead wrap around in a modular way. Any constant unsigned integer expressions that in effect \"overflow\" will not be detected by the compiler. Although there may be good reasons at run-time to rely on the modular arithmetic provided by unsigned integer types, the reasons for using it at compile-time to evaluate a constant expression are less obvious. Any instance of an unsigned integer constant expression wrapping around is therefore likely to indicate a programming error.",
+          "kind": "problem",
+          "name": "Evaluation of constant expressions should not lead to unsigned integer wrap-around",
+          "precision": "very-high",
+          "severity": "error",
+          "short_name": "ConstantUnsignedIntegerExpressionsWrapAround",
+          "shared_implementation_short_name": "ConstantUnsignedIntegerExpressionsWrapAround",
+          "tags": [
+            "correctness",
+            "security"
+          ]
+        }
+      ],
+      "title": "Evaluation of constant expressions should not lead to unsigned integer wrap-around"
+    }
+  }
+}
\ No newline at end of file
diff --git a/rule_packages/cpp/Expressions.json b/rule_packages/cpp/Expressions.json
index 8bf26eb14c..c0a7b6bb0b 100644
--- a/rule_packages/cpp/Expressions.json
+++ b/rule_packages/cpp/Expressions.json
@@ -249,6 +249,7 @@
           "precision": "very-high",
           "severity": "error",
           "short_name": "ConstantUnsignedIntegerExpressionsWrapAround",
+          "shared_implementation_short_name": "ConstantUnsignedIntegerExpressionsWrapAround",
           "tags": [
             "correctness",
             "security"
diff --git a/rules.csv b/rules.csv
index ab005cbe5b..27622288c2 100644
--- a/rules.csv
+++ b/rules.csv
@@ -548,12 +548,12 @@ c,CERT-C,FLP32-C,Yes,Rule,,,Prevent or detect domain and range errors in math fu
 c,CERT-C,FLP34-C,Yes,Rule,,,Ensure that floating-point conversions are within range of the new type,,FloatingTypes,Medium,
 c,CERT-C,FLP36-C,Yes,Rule,,,Preserve precision when converting integral values to floating-point type,,FloatingTypes,Medium,
 c,CERT-C,FLP37-C,Yes,Rule,,,Do not use object representations to compare floating-point values,,FloatingTypes,Medium,
-c,CERT-C,INT30-C,Yes,Rule,,,Ensure that unsigned integer operations do not wrap,A4-7-1,Types,Hard,
-c,CERT-C,INT31-C,Yes,Rule,,,Ensure that integer conversions do not result in lost or misinterpreted data,A4-7-1,Types,Hard,
-c,CERT-C,INT32-C,Yes,Rule,,,Ensure that operations on signed integers do not result in overflow,A4-7-1,Types,Hard,
-c,CERT-C,INT33-C,Yes,Rule,,,Ensure that division and remainder operations do not result in divide-by-zero errors,,Types,Hard,
+c,CERT-C,INT30-C,Yes,Rule,,,Ensure that unsigned integer operations do not wrap,A4-7-1,IntegerOverflow,Hard,
+c,CERT-C,INT31-C,Yes,Rule,,,Ensure that integer conversions do not result in lost or misinterpreted data,A4-7-1,IntegerOverflow,Hard,
+c,CERT-C,INT32-C,Yes,Rule,,,Ensure that operations on signed integers do not result in overflow,A4-7-1,IntegerOverflow,Hard,
+c,CERT-C,INT33-C,Yes,Rule,,,Ensure that division and remainder operations do not result in divide-by-zero errors,,IntegerOverflow,Hard,
 c,CERT-C,INT34-C,Yes,Rule,,,Do not shift an expression by a negative number of bits or by greater than or equal to the number of bits that exist in the operand,M5-8-1,Types,Import,
-c,CERT-C,INT35-C,Yes,Rule,,,Use correct integer precisions,,Types,Hard,
+c,CERT-C,INT35-C,Yes,Rule,,,Use correct integer precisions,,IntegerOverflow,Hard,
 c,CERT-C,INT36-C,Yes,Rule,,,Converting a pointer to integer or integer to pointer,M5-2-9,Types,Easy,
 c,CERT-C,MEM30-C,Yes,Rule,,,Do not access freed memory,MEM50-CPP,InvalidMemory1,Import,
 c,CERT-C,MEM31-C,Yes,Rule,,,Free dynamically allocated memory when no longer needed,,Memory2,Very Hard,
@@ -685,7 +685,7 @@ c,MISRA-C-2012,RULE-11-9,Yes,Required,,,The macro NULL shall be the only permitt
 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,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-4,Yes,Advisory,,,Evaluation of constant expressions should not lead to unsigned integer wrap-around,INT30-C,IntegerOverflow,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,
 c,MISRA-C-2012,RULE-13-1,Yes,Required,,,Initializer lists shall not contain persistent side effects,,SideEffects1,Medium,
 c,MISRA-C-2012,RULE-13-2,Yes,Required,,,The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders,PRE31-C,SideEffects,Medium,