diff --git a/cpp/common/src/codingstandards/cpp/OutOfBounds.qll b/cpp/common/src/codingstandards/cpp/OutOfBounds.qll
new file mode 100644
index 000000000..b59018613
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/OutOfBounds.qll
@@ -0,0 +1,1350 @@
+/**
+ * This module provides classes and predicates for analyzing the size of buffers
+ * or objects from their base or a byte-offset, and identifying the potential for
+ * expressions accessing those buffers to overflow.
+ */
+
+import cpp
+import codingstandards.cpp.types.Pointers
+import codingstandards.cpp.Allocations
+import codingstandards.cpp.Overflow
+import codingstandards.cpp.PossiblyUnsafeStringOperation
+import codingstandards.cpp.SimpleRangeAnalysisCustomizations
+private import semmle.code.cpp.dataflow.DataFlow
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+module OOB {
+  /**
+   * Holds if `result` is either `name` or a string matching a pattern such as
+   * `__builtin_*name*_chk` or similar. This predicate exists to model internal functions
+   * such as `__builtin___memcpy_chk` under a common `memcpy` name in the table.
+   */
+  bindingset[name, result]
+  string getNameOrInternalName(string name) {
+    result.regexpMatch("^(?:__.*_+)?" + name + "(?:_[^s].*)?$")
+  }
+
+  /**
+   * MISRA-C Rule 21.17 function table of names and parameter indices
+   * which covers functions from <string.h> that rely on null-terminated strings.
+   *
+   * This table is a subset of `libraryFunctionNameParamTable`.
+   *
+   * Note: These functions do not share a common semantic pattern of source and destination
+   * parameters with the other functions explicitly defined in `libraryFunctionNameParamTable`,
+   * although they do share a common issue of parsing non-null-terminated strings.
+   * The `SimpleStringLibraryFunction` base class provides an appropriate
+   * interface for analyzing the functions in the below table.
+   */
+  private Function libraryFunctionNameParamTableSimpleString(
+    string name, int dst, int src, int src_sz, int dst_sz
+  ) {
+    result.getName() = getNameOrInternalName(name) and
+    src_sz = -1 and
+    dst_sz = -1 and
+    (
+      name = "strcat" and
+      dst = 0 and
+      src = 1
+      or
+      name = "strchr" and
+      dst = -1 and
+      src = 0
+      or
+      name = ["strcmp", "strcoll"] and
+      dst = -1 and
+      src = [0, 1]
+      or
+      name = "strcpy" and
+      dst = 0 and
+      src = 1
+      or
+      name = "strcspn" and
+      dst = -1 and
+      src = [0, 1]
+      or
+      name = "strlen" and
+      dst = -1 and
+      src = 0
+      or
+      name = "strpbrk" and
+      dst = -1 and
+      src = [0, 1]
+      or
+      name = "strrchr" and
+      dst = -1 and
+      src = 0
+      or
+      name = "strspn" and
+      dst = -1 and
+      src = [0, 1]
+      or
+      name = "strstr" and
+      dst = -1 and
+      src = [0, 1]
+      or
+      // do not specify a src and dst to avoid buffer size assumptions
+      name = ["strtok", "strtok_r"] and
+      dst = -1 and
+      src = [0, 1]
+    )
+  }
+
+  /**
+   * A relation of the indices of buffer and size parameters of standard library functions
+   * which are defined in rules CERT ARR38-C and MISRA-C rules 21.17 and 21.18.
+   */
+  private Function libraryFunctionNameParamTable(
+    string name, int dst, int src, int src_sz, int dst_sz
+  ) {
+    result = libraryFunctionNameParamTableSimpleString(name, dst, src, src_sz, dst_sz)
+    or
+    result.getName() = getNameOrInternalName(name) and
+    (
+      name = ["fgets", "fgetws"] and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 1
+      or
+      name = ["mbstowcs", "wcstombs"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = ["mbrtoc16", "mbrtoc32"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = 2 and
+      dst_sz = -1
+      or
+      name = ["mbsrtowcs", "wcsrtombs"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = ["mbtowc", "mbrtowc"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = 2 and
+      dst_sz = -1
+      or
+      name = ["mblen", "mbrlen"] and
+      dst = -1 and
+      src = 0 and
+      src_sz = 1 and
+      dst_sz = -1
+      or
+      name = ["memchr", "wmemchr"] and
+      dst = -1 and
+      src = 0 and
+      src_sz = 2 and
+      dst_sz = -1
+      or
+      name = ["memset", "wmemset"] and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = ["strftime", "wcsftime"] and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 1
+      or
+      name = ["strxfrm", "wcsxfrm"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = ["strncat", "wcsncat"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = 2 and
+      dst_sz = -1
+      or
+      name = ["snprintf", "vsnprintf", "swprintf", "vswprintf"] and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 1
+      or
+      name = "setvbuf" and
+      dst = -1 and
+      src = 1 and
+      src_sz = 3 and
+      dst_sz = -1
+      or
+      name = ["memcpy", "wmemcpy", "memmove", "wmemmove", "memcmp", "wmemcmp", "strncmp", "wcsncmp"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = 2 and
+      dst_sz = 2
+      or
+      name = ["strncpy", "wcsncpy"] and
+      dst = 0 and
+      src = 1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = "qsort" and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 1
+      or
+      name = "bsearch" and
+      dst = -1 and
+      src = 1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = "fread" and
+      dst = 0 and
+      src = -1 and
+      src_sz = -1 and
+      dst_sz = 2
+      or
+      name = "fwrite" and
+      dst = -1 and
+      src = 0 and
+      src_sz = 2 and
+      dst_sz = -1
+    )
+  }
+
+  /**
+   * A library function that accesses one or more buffers supplied via arguments.
+   */
+  class BufferAccessLibraryFunction extends Function {
+    BufferAccessLibraryFunction() { this = libraryFunctionNameParamTable(_, _, _, _, _) }
+
+    /**
+     * Returns the indices of parameters that are a destination buffer.
+     */
+    int getWriteParamIndex() {
+      this = libraryFunctionNameParamTable(_, result, _, _, _) and
+      result >= 0
+    }
+
+    /**
+     * Returns the indices of parameters that are a source buffer.
+     */
+    int getReadParamIndex() {
+      this = libraryFunctionNameParamTable(_, _, result, _, _) and
+      result >= 0
+    }
+
+    /**
+     * Returns the index of the parameter that is the source buffer size.
+     */
+    int getReadSizeParamIndex() {
+      this = libraryFunctionNameParamTable(_, _, _, result, _) and
+      result >= 0
+    }
+
+    /**
+     * Returns the index of the parameter that is the destination buffer size.
+     */
+    int getWriteSizeParamIndex() {
+      this = libraryFunctionNameParamTable(_, _, _, _, result) and
+      result >= 0
+    }
+
+    /**
+     * Gets a parameter than is a source (read) buffer.
+     */
+    Parameter getReadParam() { result = this.getParameter(this.getReadParamIndex()) }
+
+    /**
+     * Gets a parameter than is a destination (write) buffer.
+     */
+    Parameter getWriteParam() { result = this.getParameter(this.getWriteParamIndex()) }
+
+    /**
+     * Gets a parameter than is a source (read) buffer size.
+     */
+    Parameter getReadSizeParam() { result = this.getParameter(this.getReadSizeParamIndex()) }
+
+    /**
+     * Gets a parameter than is a destination (write) buffer size.
+     */
+    Parameter getWriteSizeParam() { result = this.getParameter(this.getWriteSizeParamIndex()) }
+
+    /**
+     * Gets the size of an element in the destination buffer class
+     */
+    int getWriteParamElementSize(Parameter p) {
+      p = this.getWriteParam() and
+      p.getType().getUnspecifiedType().(DerivedType).getBaseType().getSize().maximum(1) = result
+    }
+
+    /**
+     * Gets the size of an element in the source buffer class
+     */
+    int getReadParamElementSize(Parameter p) {
+      p = this.getReadParam() and
+      p.getType().getUnspecifiedType().(DerivedType).getBaseType().getSize().maximum(1) = result
+    }
+
+    /**
+     * Holds if `i` is the index of a parameter of this function that requires arguments to be null-terminated.
+     * This predicate should be overriden by extending classes to specify null-terminated parameters, if necessary.
+     */
+    predicate getANullTerminatedParameterIndex(int i) {
+      // by default, require null-terminated parameters for src but
+      // only if the type of src is a plain char pointer or wchar_t.
+      this.getReadParamIndex() = i and
+      exists(Type baseType |
+        baseType = this.getReadParam().getUnspecifiedType().(PointerType).getBaseType() and
+        (
+          baseType.getUnspecifiedType() instanceof PlainCharType or
+          baseType.getUnspecifiedType() instanceof Wchar_t
+        )
+      )
+    }
+
+    /**
+     * Holds if `i` is the index of a parameter of this function that is a size multiplier.
+     * This predicate should be overriden by extending classes to specify size multiplier parameters, if necessary.
+     */
+    predicate getASizeMultParameterIndex(int i) {
+      // by default, there is no size multiplier parameter
+      // exceptions: fread, fwrite, bsearch, qsort
+      none()
+    }
+
+    /**
+     * Holds if `i` is the index of a parameter of this function that expects an element count rather than buffer size argument.
+     * This predicate should be overriden by extending classes to specify length parameters, if necessary.
+     */
+    predicate getALengthParameterIndex(int i) {
+      // by default, size parameters do not exclude the size of a null terminator
+      none()
+    }
+
+    /**
+     * Holds if the read or write parameter at index `i` is allowed to be null.
+     * This predicate should be overriden by extending classes to specify permissibly null parameters, if necessary.
+     */
+    predicate getAPermissiblyNullParameterIndex(int i) {
+      // by default, pointer parameters are not allowed to be null
+      none()
+    }
+  }
+
+  /**
+   * A library function that accesses one or more string buffers and has no
+   * additional parameters for specifying the size of the buffers.
+   */
+  class SimpleStringLibraryFunction extends BufferAccessLibraryFunction {
+    SimpleStringLibraryFunction() {
+      this = libraryFunctionNameParamTableSimpleString(_, _, _, -1, -1)
+    }
+
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // by default, require null-terminated parameters for src but
+      // only if the type of src is a plain char pointer.
+      this.getReadParamIndex() = i and
+      this.getReadParam().getUnspecifiedType().(PointerType).getBaseType().getUnspecifiedType()
+        instanceof PlainCharType
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` that performs string concatenation.
+   */
+  abstract class StringConcatenationFunctionLibraryFunction extends BufferAccessLibraryFunction {
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // `strcat` and variants require null-terminated params for both src and dst
+      i = [0, 1]
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `strcat`
+   */
+  class StrcatLibraryFunction extends StringConcatenationFunctionLibraryFunction {
+    StrcatLibraryFunction() { this.getName() = getNameOrInternalName("strcat") }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `strncat` or `wcsncat`
+   */
+  class StrncatLibraryFunction extends StringConcatenationFunctionLibraryFunction {
+    StrncatLibraryFunction() { this.getName() = getNameOrInternalName(["strncat", "wcsncat"]) }
+
+    override predicate getALengthParameterIndex(int i) {
+      // `strncat` and `wcsncat` exclude the size of a null terminator
+      i = 2
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `strncpy`
+   */
+  class StrncpyLibraryFunction extends StringConcatenationFunctionLibraryFunction {
+    StrncpyLibraryFunction() { this.getName() = getNameOrInternalName("strncpy") }
+
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // `strncpy` does not require null-terminated parameters
+      none()
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `strncmp`
+   */
+  class StrncmpLibraryFunction extends BufferAccessLibraryFunction {
+    StrncmpLibraryFunction() { this.getName() = getNameOrInternalName("strncmp") }
+
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // `strncmp` does not require null-terminated parameters
+      none()
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `mbtowc` and `mbrtowc`
+   */
+  class MbtowcLibraryFunction extends BufferAccessLibraryFunction {
+    MbtowcLibraryFunction() { this.getName() = getNameOrInternalName(["mbtowc", "mbrtowc"]) }
+
+    override predicate getAPermissiblyNullParameterIndex(int i) {
+      // `mbtowc` requires null-terminated parameters for both src and dst
+      i = [0, 1]
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `mblen` and `mbrlen`
+   */
+  class MblenLibraryFunction extends BufferAccessLibraryFunction {
+    MblenLibraryFunction() { this.getName() = getNameOrInternalName(["mblen", "mbrlen"]) }
+
+    override predicate getAPermissiblyNullParameterIndex(int i) { i = 0 }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `setvbuf`
+   */
+  class SetvbufLibraryFunction extends BufferAccessLibraryFunction {
+    SetvbufLibraryFunction() { this.getName() = getNameOrInternalName("setvbuf") }
+
+    override predicate getAPermissiblyNullParameterIndex(int i) { i = 1 }
+
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // `setvbuf` does not require a null-terminated buffer
+      none()
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `snprintf`, `vsnprintf`, `swprintf`, and `vswprintf`.
+   * This class overrides the `getANullTerminatedParameterIndex` predicate to include the `format` parameter.
+   */
+  class PrintfLibraryFunction extends BufferAccessLibraryFunction {
+    PrintfLibraryFunction() {
+      this.getName() = getNameOrInternalName(["snprintf", "vsnprintf", "swprintf", "vswprintf"])
+    }
+
+    override predicate getANullTerminatedParameterIndex(int i) {
+      // `snprintf` and variants require a null-terminated format string
+      i = 2
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `fread` and `fwrite`.
+   */
+  class FreadFwriteLibraryFunction extends BufferAccessLibraryFunction {
+    FreadFwriteLibraryFunction() { this.getName() = getNameOrInternalName(["fread", "fwrite"]) }
+
+    override predicate getASizeMultParameterIndex(int i) {
+      // `fread` and `fwrite` have a size multiplier parameter
+      i = 1
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `bsearch`
+   */
+  class BsearchLibraryFunction extends BufferAccessLibraryFunction {
+    BsearchLibraryFunction() { this.getName() = getNameOrInternalName("bsearch") }
+
+    override predicate getASizeMultParameterIndex(int i) {
+      // `bsearch` has a size multiplier parameter
+      i = 3
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `qsort`
+   */
+  class QsortLibraryFunction extends BufferAccessLibraryFunction {
+    QsortLibraryFunction() { this.getName() = getNameOrInternalName("qsort") }
+
+    override predicate getASizeMultParameterIndex(int i) {
+      // `qsort` has a size multiplier parameter
+      i = 2
+    }
+  }
+
+  /**
+   * A `BufferAccessLibraryFunction` modelling `strtok`
+   */
+  class StrtokLibraryFunction extends BufferAccessLibraryFunction {
+    StrtokLibraryFunction() { this.getName() = getNameOrInternalName(["strtok", "strtok_r"]) }
+
+    override predicate getAPermissiblyNullParameterIndex(int i) {
+      // `strtok` does not require a non-null `str` parameter
+      i = 0
+    }
+  }
+
+  /**
+   * An construction of a pointer to a buffer.
+   */
+  abstract class BufferAccess extends Expr {
+    abstract predicate hasABuffer(Expr buffer, Expr size, int sizeMult);
+
+    Expr getARelevantExpr() {
+      hasABuffer(result, _, _)
+      or
+      hasABuffer(_, result, _)
+    }
+  }
+
+  class PointerArithmeticBufferAccess extends BufferAccess instanceof PointerArithmeticExpr {
+    override predicate hasABuffer(Expr buffer, Expr size, int sizeMult) {
+      buffer = this.(PointerArithmeticExpr).getPointer() and
+      size = this.(PointerArithmeticExpr).getOperand() and
+      sizeMult =
+        buffer.getType().getUnspecifiedType().(DerivedType).getBaseType().getSize().maximum(1)
+    }
+  }
+
+  class ArrayBufferAccess extends BufferAccess, ArrayExpr {
+    override predicate hasABuffer(Expr buffer, Expr size, int sizeMult) {
+      buffer = this.getArrayBase() and
+      size = this.getArrayOffset() and
+      sizeMult =
+        buffer.getType().getUnspecifiedType().(DerivedType).getBaseType().getSize().maximum(1)
+    }
+  }
+
+  /**
+   * A `FunctionCall` to a `BufferAccessLibraryFunction` that provides predicates for
+   * reasoning about buffer overflow and other buffer access violations.
+   */
+  class BufferAccessLibraryFunctionCall extends FunctionCall, BufferAccess {
+    BufferAccessLibraryFunctionCall() { this.getTarget() instanceof BufferAccessLibraryFunction }
+
+    override predicate hasABuffer(Expr buffer, Expr size, int sizeMult) {
+      buffer = this.getWriteArg() and
+      size = this.getWriteSizeArg(sizeMult)
+      or
+      buffer = this.getReadArg() and
+      size = this.getReadSizeArg(sizeMult)
+    }
+
+    Expr getReadArg() {
+      result = this.getArgument(this.getTarget().(BufferAccessLibraryFunction).getReadParamIndex())
+    }
+
+    Expr getWriteArg() {
+      result = this.getArgument(this.getTarget().(BufferAccessLibraryFunction).getWriteParamIndex())
+    }
+
+    Expr getReadSizeArg(int mult) {
+      result =
+        this.getArgument(this.getTarget().(BufferAccessLibraryFunction).getReadSizeParamIndex()) and
+      getReadSizeArgMult() = mult
+    }
+
+    Expr getWriteSizeArg(int mult) {
+      result =
+        this.getArgument(this.getTarget().(BufferAccessLibraryFunction).getWriteSizeParamIndex()) and
+      getWriteSizeArgMult() = mult
+    }
+
+    int getReadSizeArgMult() {
+      result =
+        this.getTarget().(BufferAccessLibraryFunction).getReadParamElementSize(_) *
+          getSizeMultArgValue()
+    }
+
+    int getWriteSizeArgMult() {
+      result =
+        this.getTarget().(BufferAccessLibraryFunction).getWriteParamElementSize(_) *
+          getSizeMultArgValue()
+    }
+
+    int getSizeMultArgValue() {
+      // Note: This predicate currently expects the size multiplier argument to be a constant.
+      // This implementation could be improved with range-analysis or data-flow to determine the argument value.
+      exists(int i |
+        this.getTarget().(BufferAccessLibraryFunction).getASizeMultParameterIndex(i) and
+        result = this.getArgument(i).getValue().toInt()
+      )
+      or
+      not this.getTarget().(BufferAccessLibraryFunction).getASizeMultParameterIndex(_) and
+      result = 1
+    }
+  }
+
+  /**
+   * A `FunctionCall` to a `SimpleStringLibraryFunction`
+   */
+  class SimpleStringLibraryFunctionCall extends BufferAccessLibraryFunctionCall {
+    SimpleStringLibraryFunctionCall() { this.getTarget() instanceof SimpleStringLibraryFunction }
+  }
+
+  bindingset[dest]
+  private Expr getSourceConstantExpr(Expr dest) {
+    exists(result.getValue().toInt()) and
+    DataFlow::localExprFlow(result, dest)
+  }
+
+  /**
+   * Gets the smallest of the upper bound of `e` or the largest source value (i.e. "stated value") that flows to `e`.
+   * Because range-analysis can over-widen bounds, take the minimum of range analysis and data-flow sources.
+   *
+   * If there is no source value that flows to `e`, this predicate does not hold.
+   *
+   * This predicate, if `e` is the size argument to malloc, would return `20` for the following example:
+   * ```
+   * size_t sz = condition ? 10 : 20;
+   * malloc(sz);
+   * ```
+   */
+  private int getMaxStatedValue(Expr e) {
+    result = upperBound(e).minimum(max(getSourceConstantExpr(e).getValue().toInt()))
+  }
+
+  /**
+   * Gets the smallest of the upper bound of `e` or the smallest source value (i.e. "stated value") that flows to `e`.
+   * Because range-analysis can over-widen bounds, take the minimum of range analysis and data-flow sources.
+   *
+   * If there is no source value that flows to `e`, this predicate does not hold.
+   *
+   * This predicate, if `e` is the size argument to malloc, would return `10` for the following example:
+   * ```
+   * size_t sz = condition ? 10 : 20;
+   * malloc(sz);
+   * ```
+   */
+  bindingset[e]
+  private int getMinStatedValue(Expr e) {
+    result = upperBound(e).minimum(min(getSourceConstantExpr(e).getValue().toInt()))
+  }
+
+  /**
+   * A class for reasoning about the offset of a variable from the original value flowing to it
+   * as a result of arithmetic or pointer arithmetic expressions.
+   */
+  bindingset[expr]
+  private int getArithmeticOffsetValue(Expr expr, Expr base) {
+    result = getMinStatedValue(expr.(PointerArithmeticExpr).getOperand()) and
+    base = expr.(PointerArithmeticExpr).getPointer()
+    or
+    // &(array[index]) expressions
+    result =
+      getMinStatedValue(expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getOperand()) and
+    base = expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getPointer()
+    or
+    result = getMinStatedValue(expr.(AddExpr).getRightOperand()) and
+    base = expr.(AddExpr).getLeftOperand()
+    or
+    result = -getMinStatedValue(expr.(SubExpr).getRightOperand()) and
+    base = expr.(SubExpr).getLeftOperand()
+    or
+    expr instanceof IncrementOperation and
+    result = 1 and
+    base = expr.(IncrementOperation).getOperand()
+    or
+    expr instanceof DecrementOperation and
+    result = -1 and
+    base = expr.(DecrementOperation).getOperand()
+    or
+    // fall-back if `expr` is not an arithmetic or pointer arithmetic expression
+    not expr instanceof PointerArithmeticExpr and
+    not expr.(AddressOfExpr).getOperand() instanceof PointerArithmeticExpr and
+    not expr instanceof AddExpr and
+    not expr instanceof SubExpr and
+    not expr instanceof IncrementOperation and
+    not expr instanceof DecrementOperation and
+    base = expr and
+    result = 0
+  }
+
+  private int constOrZero(Expr e) {
+    result = e.getValue().toInt()
+    or
+    not exists(e.getValue().toInt()) and result = 0
+  }
+
+  abstract class PointerToObjectSource extends Expr {
+    /**
+     * Gets the expression that points to the object.
+     */
+    abstract Expr getPointer();
+
+    /**
+     * Gets the expression, if any, that defines the size of the object.
+     */
+    abstract Expr getSizeExpr();
+
+    /**
+     * Gets the size of the object, if it is statically known.
+     */
+    abstract int getFixedSize();
+
+    /**
+     * Holds if the object is not null-terminated.
+     */
+    abstract predicate isNotNullTerminated();
+  }
+
+  private class DynamicAllocationSource extends PointerToObjectSource instanceof AllocationExpr,
+    FunctionCall
+  {
+    DynamicAllocationSource() {
+      // exclude OperatorNewAllocationFunction to only deal with raw malloc-style calls,
+      // which do not apply a multiple to the size of the allocation passed to them.
+      not this.(FunctionCall).getTarget() instanceof OperatorNewAllocationFunction
+    }
+
+    override Expr getPointer() { result = this }
+
+    override Expr getSizeExpr() {
+      // AllocationExpr may sometimes return a subexpression of the size expression
+      // in order to separate the size from a sizeof expression in a MulExpr.
+      exists(AllocationFunction f |
+        f = this.(FunctionCall).getTarget() and
+        result = this.(FunctionCall).getArgument(f.getSizeArg())
+      )
+    }
+
+    /**
+     * Returns either `getSizeExpr()`, or, if a value assigned to a variable flows
+     * to `getSizeExpr()` or an `AddExpr` within it, the value assigned to that variable.
+     *
+     * If an `AddExpr` exists in the value assignment or `getSizeExpr()`, and that `AddExpr`
+     * has a constant right operand, then value of that operand is `offset`. Otherwise, `offset` is 0.
+     *
+     * If no `AddExpr` exists, `base = result`. Otherwise, `base` is the left operand of the `AddExpr`.
+     * If the left operand of the `AddExpr` comes from a variable assignment, `base` is assigned value.
+     *
+     * This predicate serves as a rough heuristic for cases such as the following:
+     * 1. `size_t sz = strlen(src) + 1; malloc(sz);`
+     * 2. `size_t sz = strlen(src); malloc(sz + 1);`
+     */
+    Expr getSizeExprSource(Expr base, int offset) {
+      if this.getSizeExpr() instanceof AddExpr
+      then
+        exists(AddExpr ae |
+          exists(Variable v |
+            // case 1: variable access + const in the size expression
+            this.getSizeExpr() = ae and
+            result = v.getAnAssignedValue() and
+            base = ae.getLeftOperand() and
+            offset = constOrZero(ae.getRightOperand()) and
+            DataFlow::localExprFlow(result, base)
+            or
+            // case 2: expr + const in the variable assignment
+            v.getAnAssignedValue() = ae and
+            result = ae and
+            base = ae.getLeftOperand() and
+            offset = constOrZero(ae.getRightOperand()) and
+            DataFlow::localExprFlow(result, this.getSizeExpr())
+          )
+          or
+          // case 3: function call + const
+          result = ae and
+          this.getSizeExpr() = ae and
+          ae.getLeftOperand() = base and
+          ae.getLeftOperand() instanceof FunctionCall and
+          offset = constOrZero(ae.getRightOperand())
+        )
+      else (
+        offset = 0 and
+        // case 3: a variable is read in the size expression
+        // if the VariableAccess does not have a computable constant value,
+        // the source node could still be useful for data-flow and GVN comparisons
+        if this.getSizeExpr() instanceof VariableAccess
+        then
+          exists(Variable v |
+            v = this.getSizeExpr().(VariableAccess).getTarget() and
+            not v instanceof Field and
+            DataFlow::localExprFlow(v.getAnAssignedValue(), base) and
+            result = base
+          )
+        else (
+          // Case 4: no variable access in the size expression
+          // This case is equivalent to getSizeExpr.
+          base = this.getSizeExpr() and
+          result = base
+        )
+      )
+    }
+
+    override int getFixedSize() { result = getMaxStatedValue(getSizeExpr()) }
+
+    override predicate isNotNullTerminated() { none() }
+  }
+
+  /**
+   * A `PointerToObjectSource` which is an `AddressOfExpr` to a variable
+   * that is not a field or pointer type.
+   */
+  private class AddressOfExprSource extends PointerToObjectSource instanceof AddressOfExpr {
+    AddressOfExprSource() {
+      exists(Variable v |
+        v = this.getOperand().(VariableAccess).getTarget() and
+        not v.getUnderlyingType() instanceof PointerType and
+        not v instanceof Field
+      )
+    }
+
+    override Expr getPointer() { result = this }
+
+    override Expr getSizeExpr() { none() }
+
+    override int getFixedSize() {
+      result = min(this.(AddressOfExpr).getOperand().getType().getSize())
+    }
+
+    override predicate isNotNullTerminated() { none() }
+  }
+
+  /**
+   * A `PointerToObjectSource` which is a `VariableAccess` to a static buffer
+   */
+  private class StaticBufferAccessSource extends PointerToObjectSource instanceof VariableAccess {
+    StaticBufferAccessSource() {
+      not this.getTarget() instanceof Field and
+      not this.getTarget().getUnspecifiedType() instanceof PointerType and
+      this.getTarget().getUnderlyingType().(ArrayType).getSize() > 0
+    }
+
+    override Expr getPointer() { result = this }
+
+    override Expr getSizeExpr() { none() }
+
+    override int getFixedSize() {
+      result = this.(VariableAccess).getTarget().getUnderlyingType().(ArrayType).getSize()
+    }
+
+    override predicate isNotNullTerminated() {
+      // StringLiteral::getOriginalLength uses Expr::getValue, which implicitly truncates string literal
+      // values to the length fitting the buffer they are assigned to, thus breaking the 'obvious' check.
+      // Note: `CharArrayInitializedWithStringLiteral` falsely reports the string literal length in certain cases
+      // (e.g. when the string literal contains escape characters or on certain compilers), resulting in false-negatives
+      exists(CharArrayInitializedWithStringLiteral init |
+        init = this.(VariableAccess).getTarget().getInitializer().getExpr() and
+        init.getStringLiteralLength() + 1 > init.getContainerLength()
+      )
+      or
+      // if the buffer is not initialized and does not have any memset call zeroing it, it is not null-terminated.
+      // note that this heuristic does not evaluate the order of the memset calls made and whether they dominate
+      // any use of the buffer by functions requiring it to be null-terminated.
+      (
+        this.(VariableAccess).getTarget().getUnspecifiedType().(ArrayType).getBaseType() instanceof
+          PlainCharType
+        or
+        this.(VariableAccess).getTarget().getUnspecifiedType().(ArrayType).getBaseType() instanceof
+          Wchar_t
+      ) and
+      not this.(VariableAccess).getTarget() instanceof GlobalVariable and
+      not exists(this.(VariableAccess).getTarget().getInitializer()) and
+      // exclude any BufferAccessLibraryFunction that writes to the buffer and does not require
+      // a null-terminated buffer argument for its write argument
+      not exists(
+        BufferAccessLibraryFunctionCall fc, BufferAccessLibraryFunction f, int writeParamIndex
+      |
+        f = fc.getTarget() and
+        writeParamIndex = f.getWriteParamIndex() and
+        not f.getANullTerminatedParameterIndex(writeParamIndex) and
+        fc.getArgument(writeParamIndex) = this.(VariableAccess).getTarget().getAnAccess()
+      ) and
+      // exclude any buffers that have an assignment, deref, or array expr with a zero constant
+      // note: heuristically implemented using getAChild*()
+      not exists(AssignExpr assign |
+        assign.getRValue().getValue().toInt() = 0 and
+        assign.getLValue().getAChild*() = this.(VariableAccess).getTarget().getAnAccess()
+      )
+      // note: the case of initializers that are not string literals and non-zero constants is not handled here.
+      // e.g. char buf[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; (not null-terminated)
+      //      char buf[10] = { 1 }; (not null-terminated)
+    }
+  }
+
+  /**
+   * A `PointerToObjectSource` which is a string literal that is not
+   * part of an variable initializer (to deduplicate `StaticBufferAccessSource`)
+   */
+  private class StringLiteralSource extends PointerToObjectSource instanceof StringLiteral {
+    StringLiteralSource() { not this instanceof CharArrayInitializedWithStringLiteral }
+
+    override Expr getPointer() { result = this }
+
+    override Expr getSizeExpr() { none() }
+
+    override int getFixedSize() {
+      // (length of the string literal + null terminator) * (size of the base type)
+      result =
+        this.(StringLiteral).getOriginalLength() *
+          this.(StringLiteral).getUnderlyingType().(DerivedType).getBaseType().getSize()
+    }
+
+    override predicate isNotNullTerminated() { none() }
+  }
+
+  private module PointerToObjectSourceOrSizeToBufferAccessFunctionConfig implements
+    DataFlow::ConfigSig
+  {
+    predicate isSource(DataFlow::Node source) {
+      source.asExpr() instanceof PointerToObjectSource
+      or
+      exists(PointerToObjectSource ptr |
+        source.asExpr() = ptr.getSizeExpr() or
+        source.asExpr() = ptr.(DynamicAllocationSource).getSizeExprSource(_, _)
+      )
+    }
+
+    predicate isSink(DataFlow::Node sink) {
+      exists(BufferAccess ba, Expr arg |
+        (
+          arg = ba.(BufferAccessLibraryFunctionCall).getAnArgument() or
+          arg = ba.getARelevantExpr()
+        ) and
+        (
+          sink.asExpr() = arg or
+          exists(getArithmeticOffsetValue(arg, sink.asExpr()))
+        )
+      )
+    }
+
+    predicate isBarrierOut(DataFlow::Node node) {
+      // the default interprocedural data-flow model flows through any array assignment expressions
+      // to the qualifier (array base or pointer dereferenced) instead of the individual element
+      // that the assignment modifies. this default behaviour causes false positives for any future
+      // access of the array base, so remove the assignment edge at the expense of false-negatives.
+      exists(AssignExpr a |
+        node.asExpr() = a.getRValue().getAChild*() and
+        (
+          a.getLValue() instanceof ArrayExpr or
+          a.getLValue() instanceof PointerDereferenceExpr
+        )
+      )
+      or
+      // remove flow from `src` to `dst` in a buffer access function call
+      // the standard library models such flow through functions such as memcpy, strcpy, etc.
+      exists(BufferAccessLibraryFunctionCall fc | node.asExpr() = fc.getReadArg().getAChild*())
+      or
+      node.asDefiningArgument() instanceof AddressOfExpr
+    }
+  }
+
+  private module PointerToObjectSourceOrSizeToBufferAccessFunctionFlow =
+    DataFlow::Global<PointerToObjectSourceOrSizeToBufferAccessFunctionConfig>;
+
+  private predicate hasFlowFromBufferOrSizeExprToUse(Expr source, Expr use) {
+    exists(Expr useOrChild |
+      exists(getArithmeticOffsetValue(use, useOrChild)) and
+      PointerToObjectSourceOrSizeToBufferAccessFunctionFlow::flow(DataFlow::exprNode(source),
+        DataFlow::exprNode(useOrChild))
+    )
+  }
+
+  private predicate bufferUseComputableBufferSize(
+    Expr bufferUse, PointerToObjectSource source, int size
+  ) {
+    // flow from a PointerToObjectSource for which we can compute the exact size
+    size = source.getFixedSize() and
+    hasFlowFromBufferOrSizeExprToUse(source, bufferUse)
+  }
+
+  private predicate bufferUseNonComputableSize(Expr bufferUse, Expr source) {
+    not bufferUseComputableBufferSize(bufferUse, source, _) and
+    hasFlowFromBufferOrSizeExprToUse(source.(DynamicAllocationSource), bufferUse)
+  }
+
+  /**
+   * Relates `sizeExpr`, a buffer access size expresion, to `source`, which is either `sizeExpr`
+   * if `sizeExpr` has a stated value, or a `DynamicAllocationSource::getSizeExprSource` for which
+   * we can compute the exact size and that has flow to `sizeExpr`.
+   */
+  private predicate sizeExprComputableSize(Expr sizeExpr, Expr source, int size) {
+    // computable direct value, e.g. array_base[10], where "10" is sizeExpr and source.
+    size = getMinStatedValue(sizeExpr) and
+    source = sizeExpr
+    or
+    // computable source value that flows to the size expression, e.g. in cases such as the following:
+    // size_t sz = 10;
+    // malloc(sz);
+    // ... sz passed interprocedurally to another function ...
+    // use(p, sz + 1);
+    size = source.(DynamicAllocationSource).getFixedSize() + getArithmeticOffsetValue(sizeExpr, _) and
+    hasFlowFromBufferOrSizeExprToUse(source.(DynamicAllocationSource).getSizeExprSource(_, _),
+      sizeExpr)
+  }
+
+  /**
+   * If the size is not computable locally, then it is either:
+   *
+   * 1. A dynamic allocation, from which we can get `getSizeExprSource()', from which
+   *    we can either check specific logic (e.g. string length with offset) or compare GVNs.
+   * 2. An unrelateable size expression, which we might, however, be able to compute the bounds
+   *    of and check against the buffer size, if that is known.
+   *
+   * In case 2, this predicate does not hold.
+   *
+   * NOTE: This predicate does not actually perform the above mentioned heuristics.
+   */
+  predicate sizeExprNonComputableSize(
+    Expr bufferSizeArg, Expr alloc, Expr allocSize, Expr allocSizeBase, int offset
+  ) {
+    bufferSizeArg = any(BufferAccess access).getARelevantExpr() and
+    not sizeExprComputableSize(bufferSizeArg, alloc, _) and
+    allocSize = alloc.(DynamicAllocationSource).getSizeExprSource(allocSizeBase, offset) and
+    hasFlowFromBufferOrSizeExprToUse(allocSize, bufferSizeArg)
+  }
+
+  /**
+   * Holds if `arg` refers to the number of characters excluding a null terminator
+   */
+  bindingset[fc, arg]
+  private predicate isArgNumCharacters(BufferAccessLibraryFunctionCall fc, Expr arg) {
+    exists(int i |
+      arg = fc.getArgument(i) and
+      fc.getTarget().(BufferAccessLibraryFunction).getALengthParameterIndex(i)
+    )
+  }
+
+  /**
+   * Returns '1' if `arg` refers to the number of characters excluding a null terminator,
+   * otherwise '0' if `arg` refers to the number of characters including a null terminator.
+   */
+  bindingset[fc, arg]
+  private int argNumCharactersOffset(BufferAccess fc, Expr arg) {
+    if isArgNumCharacters(fc, arg) then result = 1 else result = 0
+  }
+
+  /**
+   * Holds if the call `fc` may result in an invalid buffer access due a read buffer being bigger
+   * than the write buffer. This heuristic is useful for cases such as strcpy(dst, src).
+   */
+  predicate isReadBufferSizeGreaterThanWriteBufferSize(
+    Expr readBuffer, Expr writeBuffer, int readBufferSize, int writeBufferSize,
+    BufferAccessLibraryFunctionCall fc
+  ) {
+    readBuffer = fc.getReadArg() and
+    writeBuffer = fc.getWriteArg() and
+    exists(int readSizeMult, int writeSizeMult, int readBufferSizeBase, int writeBufferSizeBase |
+      // the read and write buffer sizes must be derived from computable constants
+      bufferUseComputableBufferSize(readBuffer, _, readBufferSizeBase) and
+      bufferUseComputableBufferSize(writeBuffer, _, writeBufferSizeBase) and
+      // calculate the buffer byte sizes (size base is the number of elements)
+      readSizeMult = fc.getReadSizeArgMult() and
+      writeSizeMult = fc.getWriteSizeArgMult() and
+      readBufferSize = readBufferSizeBase - readSizeMult * getArithmeticOffsetValue(readBuffer, _) and
+      writeBufferSize =
+        writeBufferSizeBase - writeSizeMult * getArithmeticOffsetValue(writeBuffer, _) and
+      // the read buffer size is larger than the write buffer size
+      readBufferSize > writeBufferSize and
+      (
+        // if a size arg exists and it is computable, then it must be <= to the write buffer size
+        exists(fc.getWriteSizeArg(writeSizeMult))
+        implies
+        (
+          sizeExprComputableSize(fc.getWriteSizeArg(writeSizeMult), _, _) and
+          not exists(Expr writeSizeArg, int writeSizeArgValue |
+            writeSizeArg = fc.getWriteSizeArg(writeSizeMult) and
+            sizeExprComputableSize(writeSizeArg, _, writeSizeArgValue) and
+            writeSizeMult.(float) *
+              (writeSizeArgValue + argNumCharactersOffset(fc, writeSizeArg)).(float) <=
+              writeBufferSize
+          )
+        )
+      )
+    )
+  }
+
+  /**
+   * Holds if `sizeArg` is the right operand of a `PointerSubExpr`
+   */
+  predicate isSizeArgPointerSubExprRightOperand(Expr sizeArg) {
+    exists(PointerSubExpr subExpr | sizeArg = subExpr.getRightOperand())
+  }
+
+  /**
+   * Holds if the BufferAccess `bufferAccess` results in a buffer overflow due to a size argument
+   * or buffer access offset being greater in size than the buffer size being accessed or written to.
+   */
+  predicate isSizeArgGreaterThanBufferSize(
+    Expr bufferArg, Expr sizeArg, PointerToObjectSource bufferSource, int computedBufferSize,
+    int computedSizeAccessed, BufferAccess bufferAccess
+  ) {
+    exists(float sizeMult, int bufferArgSize, int sizeArgValue |
+      bufferAccess.hasABuffer(bufferArg, sizeArg, sizeMult) and
+      bufferUseComputableBufferSize(bufferArg, bufferSource, bufferArgSize) and
+      // If the bufferArg is an access of a static buffer, do not look for "long distance" sources
+      (bufferArg instanceof StaticBufferAccessSource implies bufferSource = bufferArg) and
+      sizeExprComputableSize(sizeArg, _, sizeArgValue) and
+      computedBufferSize = bufferArgSize - sizeMult.(float) * getArithmeticOffsetValue(bufferArg, _) and
+      // Handle cases such as *(ptr - 1)
+      (
+        if isSizeArgPointerSubExprRightOperand(sizeArg)
+        then
+          computedSizeAccessed =
+            sizeMult.(float) *
+              (-sizeArgValue + argNumCharactersOffset(bufferAccess, sizeArg)).(float)
+        else
+          computedSizeAccessed =
+            sizeMult.(float) *
+              (sizeArgValue + argNumCharactersOffset(bufferAccess, sizeArg)).(float)
+      ) and
+      computedBufferSize < computedSizeAccessed
+    )
+  }
+
+  /**
+   * Holds if the call `fc` may result in an invalid buffer access due to a buffer argument
+   * being accessed at an offset that is greater than the size of the buffer.
+   */
+  predicate isBufferOffsetGreaterThanBufferSize(
+    Expr bufferArg, int bufferArgOffset, int bufferSize, BufferAccessLibraryFunctionCall fc
+  ) {
+    exists(int bufferElementSize |
+      (
+        bufferArg = fc.getReadArg() and
+        bufferElementSize = fc.getReadSizeArgMult()
+        or
+        bufferArg = fc.getWriteArg() and
+        bufferElementSize = fc.getWriteSizeArgMult()
+      ) and
+      bufferUseComputableBufferSize(bufferArg, _, bufferSize) and
+      bufferArgOffset = getArithmeticOffsetValue(bufferArg, _) * bufferElementSize and
+      bufferArgOffset >= bufferSize
+    )
+  }
+
+  /**
+   * Holds if `a` and `b` are function calls to the same target function and
+   * have identical arguments (determined by their global value number or `VariableAccess` targets).
+   */
+  bindingset[a, b]
+  private predicate areFunctionCallsSyntacticallySame(FunctionCall a, FunctionCall b) {
+    a.getTarget() = b.getTarget() and
+    (
+      exists(a.getAnArgument())
+      implies
+      not exists(int i, Expr argA, Expr argB |
+        i = [0 .. a.getTarget().getNumberOfParameters() - 1]
+      |
+        argA = a.getArgument(i) and
+        argB = b.getArgument(i) and
+        not globalValueNumber(argA) = globalValueNumber(argB) and
+        not argA.(VariableAccess).getTarget() = argB.(VariableAccess).getTarget()
+      )
+    )
+  }
+
+  /**
+   * Holds if `a` and `b` have the same global value number or are syntactically identical function calls
+   */
+  bindingset[a, b]
+  private predicate isGVNOrFunctionCallSame(Expr a, Expr b) {
+    globalValueNumber(a) = globalValueNumber(b)
+    or
+    areFunctionCallsSyntacticallySame(a, b)
+  }
+
+  /**
+   * Holds if the BufferAccess is accessed with a `base + accessOffset` on a buffer that was
+   * allocated a size of the form `base + allocationOffset`.
+   */
+  predicate isGVNOffsetGreaterThanBufferSize(
+    Expr bufferArg, Expr bufferSizeArg, Expr sourceSizeExpr, int sourceSizeExprOffset,
+    int sizeArgOffset, BufferAccessLibraryFunctionCall fc
+  ) {
+    exists(
+      DynamicAllocationSource source, Expr sourceSizeExprBase, int bufferArgOffset, int sizeMult
+    |
+      (
+        bufferArg = fc.getWriteArg() and
+        bufferSizeArg = fc.getWriteSizeArg(sizeMult)
+        or
+        bufferArg = fc.getReadArg() and
+        bufferSizeArg = fc.getReadSizeArg(sizeMult)
+      ) and
+      sourceSizeExpr = source.getSizeExprSource(sourceSizeExprBase, sourceSizeExprOffset) and
+      bufferUseNonComputableSize(bufferArg, source) and
+      not globalValueNumber(sourceSizeExpr) = globalValueNumber(bufferSizeArg) and
+      exists(Expr sizeArgBase |
+        sizeArgOffset = getArithmeticOffsetValue(bufferSizeArg.getAChild*(), sizeArgBase) and
+        isGVNOrFunctionCallSame(sizeArgBase, sourceSizeExprBase) and
+        bufferArgOffset = getArithmeticOffsetValue(bufferArg, _) and
+        sourceSizeExprOffset + bufferArgOffset < sizeArgOffset
+      )
+    )
+  }
+
+  /**
+   * Holds if the call `fc` may result in an invalid buffer access due to a standard library
+   * function being called with a null pointer as a buffer argument while expecting only non-null input.
+   */
+  predicate isMandatoryBufferArgNull(Expr bufferArg, BufferAccessLibraryFunctionCall fc) {
+    exists(int i |
+      i =
+        [
+          fc.getTarget().(BufferAccessLibraryFunction).getReadParamIndex(),
+          fc.getTarget().(BufferAccessLibraryFunction).getWriteParamIndex()
+        ] and
+      not fc.getTarget().(BufferAccessLibraryFunction).getAPermissiblyNullParameterIndex(i) and
+      bufferArg = fc.getArgument(i) and
+      getMinStatedValue(bufferArg) = 0
+    )
+  }
+
+  /**
+   * Holds if the call `fc` may result in an invalid buffer access due to a standard library function
+   * receiving a non-null terminated buffer as a buffer argument and accessing it.
+   */
+  predicate isNullTerminatorMissingFromArg(
+    Expr arg, PointerToObjectSource source, BufferAccessLibraryFunctionCall fc
+  ) {
+    exists(int i, Expr argChild |
+      fc.getTarget().(BufferAccessLibraryFunction).getANullTerminatedParameterIndex(i) and
+      fc.getArgument(i) = arg and
+      source.isNotNullTerminated() and
+      argChild = arg.getAChild*() and
+      // ignore cases like strcpy(irrelevant_func(non_null_terminated_str, ...), src)
+      not exists(FunctionCall other |
+        not other = fc and
+        other.getAnArgument().getAChild*() = argChild
+      ) and
+      hasFlowFromBufferOrSizeExprToUse(source, argChild)
+    )
+  }
+
+  predicate isSizeArgNotCheckedLessThanFixedBufferSize(
+    Expr bufferArg, Expr sizeArg, PointerToObjectSource bufferSource, int bufferArgSize,
+    BufferAccess bufferAccess, int sizeArgUpperBound, int sizeMult
+  ) {
+    bufferAccess.hasABuffer(bufferArg, sizeArg, sizeMult) and
+    bufferUseComputableBufferSize(bufferArg, bufferSource, bufferArgSize) and
+    // If the bufferArg is an access of a static buffer, do not look for "long distant" sources
+    (bufferArg instanceof StaticBufferAccessSource implies bufferSource = bufferArg) and
+    // Not a size expression for which we can compute a specific size
+    not sizeExprComputableSize(sizeArg, _, _) and
+    // Range analysis considers the upper bound to be larger than the buffer size
+    sizeArgUpperBound = upperBound(sizeArg) and
+    // Ignore bitwise & operations
+    not sizeArg instanceof BitwiseAndExpr and
+    sizeArgUpperBound * sizeMult > bufferArgSize and
+    // There isn't a relational operation guarding this access that seems to check the
+    // upper bound against a plausible terminal value
+    not exists(RelationalOperation relOp, Expr checkedUpperBound |
+      globalValueNumber(relOp.getLesserOperand()) = globalValueNumber(sizeArg) and
+      checkedUpperBound = relOp.getGreaterOperand() and
+      // There's no closer inferred bounds - otherwise we let range analysis check it
+      upperBound(checkedUpperBound) = exprMaxVal(checkedUpperBound)
+    )
+  }
+
+  predicate isSizeArgNotCheckedGreaterThanZero(
+    Expr bufferArg, Expr sizeArg, PointerToObjectSource bufferSource, BufferAccess bufferAccess
+  ) {
+    exists(float sizeMult |
+      bufferAccess.hasABuffer(bufferArg, sizeArg, sizeMult) and
+      (
+        bufferUseComputableBufferSize(bufferArg, bufferSource, _) or
+        bufferUseNonComputableSize(bufferArg, bufferSource)
+      ) and
+      (
+        // Not a size expression for which we can compute a specific size
+        not sizeExprComputableSize(sizeArg, _, _) and
+        // and with a lower bound that is less than zero, taking into account offsets
+        lowerBound(sizeArg) + getArithmeticOffsetValue(bufferArg, _) < 0
+        or
+        // A size expression for which we can compute a specific size and that size is less than zero
+        sizeExprComputableSize(sizeArg, _, _) and
+        (
+          if isSizeArgPointerSubExprRightOperand(sizeArg)
+          then -sizeArg.getValue().toInt() + getArithmeticOffsetValue(bufferArg, _) < 0
+          else sizeArg.getValue().toInt() + getArithmeticOffsetValue(bufferArg, _) < 0
+        )
+      )
+    )
+  }
+
+  private string bufferArgType(BufferAccessLibraryFunctionCall fc, Expr bufferArg) {
+    fc.getReadArg() = bufferArg and
+    result = "read buffer"
+    or
+    fc.getWriteArg() = bufferArg and
+    result = "write buffer"
+  }
+
+  predicate problems(
+    BufferAccessLibraryFunctionCall fc, string message, Expr bufferArg, string bufferArgStr,
+    Expr sizeOrOtherBufferArg, string otherStr
+  ) {
+    exists(int bufferArgSize, int sizeArgValue |
+      isSizeArgGreaterThanBufferSize(bufferArg, sizeOrOtherBufferArg, _, bufferArgSize,
+        sizeArgValue, fc) and
+      bufferArgStr = bufferArgType(fc, bufferArg) and
+      message =
+        "The size of the $@ passed to " + fc.getTarget().getName() + " is " + bufferArgSize +
+          " bytes, but the " + "$@ is " + sizeArgValue + " bytes." and
+      otherStr = "size argument"
+      or
+      isBufferOffsetGreaterThanBufferSize(bufferArg, sizeArgValue, bufferArgSize, fc) and
+      bufferArgStr = bufferArgType(fc, bufferArg) and
+      message =
+        "The $@ passed to " + fc.getTarget().getName() + " is " + bufferArgSize +
+          " bytes, but an offset of " + sizeArgValue + " bytes is used to access it." and
+      otherStr = "" and
+      sizeOrOtherBufferArg = bufferArg
+    )
+    or
+    isMandatoryBufferArgNull(bufferArg, fc) and
+    message = "The $@ passed to " + fc.getTarget().getName() + " is null." and
+    bufferArgStr = "argument" and
+    otherStr = "" and
+    sizeOrOtherBufferArg = bufferArg
+    or
+    isNullTerminatorMissingFromArg(bufferArg, _, fc) and
+    message = "The $@ passed to " + fc.getTarget().getName() + " might not be null-terminated." and
+    bufferArgStr = "argument" and
+    otherStr = "" and
+    sizeOrOtherBufferArg = bufferArg
+    or
+    exists(int readBufferSize, int writeBufferSize |
+      isReadBufferSizeGreaterThanWriteBufferSize(bufferArg, sizeOrOtherBufferArg, readBufferSize,
+        writeBufferSize, fc) and
+      message =
+        "The size of the $@ passed to " + fc.getTarget().getName() + " is " + readBufferSize +
+          " bytes, but the size of the $@ is only " + writeBufferSize + " bytes." and
+      bufferArgStr = "read buffer" and
+      otherStr = "write buffer"
+    )
+    or
+    exists(int accessOffset, Expr source |
+      isGVNOffsetGreaterThanBufferSize(bufferArg, _, source, _, accessOffset, fc) and
+      message =
+        "The $@ passed to " + fc.getTarget().getName() + " is accessed at an excessive offset of " +
+          accessOffset + " element(s) from the $@." and
+      bufferArgStr = bufferArgType(fc, bufferArg) and
+      sizeOrOtherBufferArg = source and
+      otherStr = "allocation size base"
+    )
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/cpp/Memory1.qll b/cpp/common/src/codingstandards/cpp/exclusions/cpp/Memory1.qll
new file mode 100644
index 000000000..d59212417
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/exclusions/cpp/Memory1.qll
@@ -0,0 +1,44 @@
+//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY.  **/
+import cpp
+import RuleMetadata
+import codingstandards.cpp.exclusions.RuleMetadata
+
+newtype Memory1Query =
+  TPointerArithmeticFormsAnInvalidPointerQuery() or
+  TPointerArgumentToCstringFunctionIsInvalidQuery()
+
+predicate isMemory1QueryMetadata(Query query, string queryId, string ruleId, string category) {
+  query =
+    // `Query` instance for the `pointerArithmeticFormsAnInvalidPointer` query
+    Memory1Package::pointerArithmeticFormsAnInvalidPointerQuery() and
+  queryId =
+    // `@id` for the `pointerArithmeticFormsAnInvalidPointer` query
+    "cpp/misra/pointer-arithmetic-forms-an-invalid-pointer" and
+  ruleId = "RULE-8-7-1" and
+  category = "required"
+  or
+  query =
+    // `Query` instance for the `pointerArgumentToCstringFunctionIsInvalid` query
+    Memory1Package::pointerArgumentToCstringFunctionIsInvalidQuery() and
+  queryId =
+    // `@id` for the `pointerArgumentToCstringFunctionIsInvalid` query
+    "cpp/misra/pointer-argument-to-cstring-function-is-invalid" and
+  ruleId = "RULE-8-7-1" and
+  category = "required"
+}
+
+module Memory1Package {
+  Query pointerArithmeticFormsAnInvalidPointerQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `pointerArithmeticFormsAnInvalidPointer` query
+      TQueryCPP(TMemory1PackageQuery(TPointerArithmeticFormsAnInvalidPointerQuery()))
+  }
+
+  Query pointerArgumentToCstringFunctionIsInvalidQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `pointerArgumentToCstringFunctionIsInvalid` query
+      TQueryCPP(TMemory1PackageQuery(TPointerArgumentToCstringFunctionIsInvalidQuery()))
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/cpp/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/cpp/RuleMetadata.qll
index 0c3cbcc28..115edcf84 100644
--- a/cpp/common/src/codingstandards/cpp/exclusions/cpp/RuleMetadata.qll
+++ b/cpp/common/src/codingstandards/cpp/exclusions/cpp/RuleMetadata.qll
@@ -37,6 +37,7 @@ import Lambdas
 import Literals
 import Loops
 import Macros
+import Memory1
 import MoveForward
 import Naming
 import Null
@@ -99,6 +100,7 @@ newtype TCPPQuery =
   TLiteralsPackageQuery(LiteralsQuery q) or
   TLoopsPackageQuery(LoopsQuery q) or
   TMacrosPackageQuery(MacrosQuery q) or
+  TMemory1PackageQuery(Memory1Query q) or
   TMoveForwardPackageQuery(MoveForwardQuery q) or
   TNamingPackageQuery(NamingQuery q) or
   TNullPackageQuery(NullQuery q) or
@@ -161,6 +163,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
   isLiteralsQueryMetadata(query, queryId, ruleId, category) or
   isLoopsQueryMetadata(query, queryId, ruleId, category) or
   isMacrosQueryMetadata(query, queryId, ruleId, category) or
+  isMemory1QueryMetadata(query, queryId, ruleId, category) or
   isMoveForwardQueryMetadata(query, queryId, ruleId, category) or
   isNamingQueryMetadata(query, queryId, ruleId, category) or
   isNullQueryMetadata(query, queryId, ruleId, category) or
diff --git a/cpp/common/test/includes/standard-library/cstdlib b/cpp/common/test/includes/standard-library/cstdlib
index 3b1eefc4a..0eb1a3e7e 100644
--- a/cpp/common/test/includes/standard-library/cstdlib
+++ b/cpp/common/test/includes/standard-library/cstdlib
@@ -23,5 +23,8 @@ using ::strtoll;
 using ::strtoul;
 using ::strtoull;
 using ::system;
+using ::malloc;
+using ::calloc;
+using ::realloc;
 } // namespace std
 #endif // _GHLIBCPP_CSTDLIB
\ No newline at end of file
diff --git a/cpp/common/test/includes/standard-library/stdlib.h b/cpp/common/test/includes/standard-library/stdlib.h
index eb73db062..090932715 100644
--- a/cpp/common/test/includes/standard-library/stdlib.h
+++ b/cpp/common/test/includes/standard-library/stdlib.h
@@ -36,4 +36,10 @@ long double strtold(const char *str, char **endptr);
 
 int rand(void);
 
-#endif // _GHLIBCPP_STDLIB
\ No newline at end of file
+int mblen (const char *, size_t);
+int mbtowc (wchar_t *__restrict, const char *__restrict, size_t);
+int wctomb (char *, wchar_t);
+size_t mbstowcs (wchar_t *__restrict, const char *__restrict, size_t);
+size_t wcstombs (char *__restrict, const wchar_t *__restrict, size_t);
+
+#endif // _GHLIBCPP_STDLIB
diff --git a/cpp/common/test/includes/standard-library/string.h b/cpp/common/test/includes/standard-library/string.h
index b4b4d9b12..5f041682f 100644
--- a/cpp/common/test/includes/standard-library/string.h
+++ b/cpp/common/test/includes/standard-library/string.h
@@ -43,5 +43,6 @@ void *memcpy(void *dest, const void *src, size_t count);
 void *memset(void *dest, int ch, size_t count);
 void *memmove(void *dest, const void *src, size_t count);
 int memcmp(const void *lhs, const void *rhs, size_t count);
+void *memchr (const void *, int, size_t);
 
-#endif // _GHLIBCPP_STRINGH
\ No newline at end of file
+#endif // _GHLIBCPP_STRINGH
diff --git a/cpp/common/test/includes/standard-library/wchar.h b/cpp/common/test/includes/standard-library/wchar.h
index 055520eb2..2352d1233 100644
--- a/cpp/common/test/includes/standard-library/wchar.h
+++ b/cpp/common/test/includes/standard-library/wchar.h
@@ -17,6 +17,9 @@ double wcstod(const wchar_t *str, wchar_t **endptr);
 float wcstof(const wchar_t *str, wchar_t **endptr);
 long double wcstold(const wchar_t *str, wchar_t **endptr);
 
+size_t wcsftime (wchar_t *__restrict, size_t, const wchar_t *__restrict, const struct tm *__restrict);
+size_t wcsxfrm (wchar_t *__restrict, const wchar_t *__restrict, size_t);
+
 // Character classification and conversion types
 typedef struct {
   int __count;
@@ -26,4 +29,4 @@ typedef struct {
   } __value;
 } mbstate_t;
 
-#endif // _GHLIBCPP_WCHAR
\ No newline at end of file
+#endif // _GHLIBCPP_WCHAR
diff --git a/cpp/misra/src/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.ql b/cpp/misra/src/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.ql
new file mode 100644
index 000000000..349a0a5c2
--- /dev/null
+++ b/cpp/misra/src/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.ql
@@ -0,0 +1,26 @@
+/**
+ * @id cpp/misra/pointer-argument-to-cstring-function-is-invalid
+ * @name RULE-8-7-1: Pointer and index arguments passed to functions in <cstring> shall not be invalid.
+ * @description Pointer and index arguments passed to functions in <cstring> should result in valid
+ *              reads and/or writes.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/misra/id/rule-8-7-1
+ *       scope/system
+ *       external/misra/enforcement/undecidable
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codingstandards.cpp.OutOfBounds // for OOB::problems
+import codingstandards.cpp.Exclusions // for isExcluded(Element, Query)
+import codingstandards.cpp.exclusions.c.RuleMetadata
+
+from
+  OOB::BufferAccessLibraryFunctionCall fc, string message, Expr bufferArg, string bufferArgStr,
+  Expr sizeOrOtherBufferArg, string otherStr
+where
+  not isExcluded(fc, OutOfBoundsPackage::libraryFunctionArgumentOutOfBoundsQuery()) and
+  OOB::problems(fc, message, bufferArg, bufferArgStr, sizeOrOtherBufferArg, otherStr)
+select fc, message, bufferArg, bufferArgStr, sizeOrOtherBufferArg, otherStr
diff --git a/cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql b/cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql
new file mode 100644
index 000000000..0b51300b6
--- /dev/null
+++ b/cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql
@@ -0,0 +1,268 @@
+/**
+ * @id cpp/misra/pointer-arithmetic-forms-an-invalid-pointer
+ * @name RULE-8-7-1: Pointer arithmetic shall not form an invalid pointer.
+ * @description Pointers obtained as result of performing arithmetic should point to an initialized
+ *              object, or an element right next to the last element of an array.
+ * @kind path-problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/misra/id/rule-8-7-1
+ *       scope/system
+ *       external/misra/enforcement/undecidable
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codingstandards.cpp.misra
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.security.BufferAccess
+
+class ArrayDeclaration extends VariableDeclarationEntry {
+  int length;
+
+  ArrayDeclaration() { this.getType().getUnderlyingType().(ArrayType).getArraySize() = length }
+
+  /**
+   * Gets the declared length of this array.
+   */
+  int getLength() { result = length }
+}
+
+class HeapAllocationFunctionCall extends FunctionCall {
+  AllocationFunction heapAllocFunction;
+
+  HeapAllocationFunctionCall() { this.getTarget() = heapAllocFunction }
+
+  predicate isMallocCall() { heapAllocFunction.getName() = "malloc" }
+
+  predicate isCallocCall() { heapAllocFunction.getName() = "calloc" }
+
+  predicate isReallocCall() { heapAllocFunction.getName() = "realloc" }
+
+  abstract int getMinNumBytes();
+}
+
+class MallocFunctionCall extends HeapAllocationFunctionCall {
+  MallocFunctionCall() { this.isMallocCall() }
+
+  override int getMinNumBytes() { result = lowerBound(this.getArgument(0)) }
+}
+
+class CallocFunctionCall extends HeapAllocationFunctionCall {
+  CallocFunctionCall() { this.isCallocCall() }
+
+  override int getMinNumBytes() {
+    result = lowerBound(this.getArgument(0)) * lowerBound(this.getArgument(1))
+  }
+}
+
+class ReallocFunctionCall extends HeapAllocationFunctionCall {
+  ReallocFunctionCall() { this.isReallocCall() }
+
+  override int getMinNumBytes() { result = lowerBound(this.getArgument(1)) }
+}
+
+class NarrowedHeapAllocationFunctionCall extends Cast {
+  HeapAllocationFunctionCall alloc;
+
+  NarrowedHeapAllocationFunctionCall() { alloc = this.getExpr() }
+
+  int getMinNumElements() {
+    result = alloc.getMinNumBytes() / this.getUnderlyingType().(PointerType).getBaseType().getSize()
+  }
+
+  HeapAllocationFunctionCall getAllocFunctionCall() { result = alloc }
+}
+
+newtype TArrayAllocation =
+  TStackAllocation(ArrayDeclaration arrayDecl) or
+  TDynamicAllocation(NarrowedHeapAllocationFunctionCall narrowedAlloc)
+
+newtype TPointerFormation =
+  TArrayExpr(ArrayExprBA arrayExpr) or
+  TPointerArithmetic(PointerArithmeticOperation pointerArithmetic)
+
+class ArrayAllocation extends TArrayAllocation {
+  ArrayDeclaration asStackAllocation() { this = TStackAllocation(result) }
+
+  NarrowedHeapAllocationFunctionCall asDynamicAllocation() { this = TDynamicAllocation(result) }
+
+  string toString() {
+    result = this.asStackAllocation().toString() or
+    result = this.asDynamicAllocation().toString()
+  }
+
+  /**
+   * Gets the number of the object that the array holds. This number is exact for a stack-allocated
+   * array, and the minimum estimated value for a heap-allocated one.
+   */
+  int getLength() {
+    result = this.asStackAllocation().getLength() or
+    result = this.asDynamicAllocation().getMinNumElements()
+  }
+
+  Location getLocation() {
+    result = this.asStackAllocation().getLocation() or
+    result = this.asDynamicAllocation().getLocation()
+  }
+
+  DataFlow::Node getNode() {
+    result.asUninitialized() = this.asStackAllocation().getVariable() or
+    result.asConvertedExpr() = this.asDynamicAllocation()
+  }
+}
+
+class PointerFormation extends TPointerFormation {
+  ArrayExprBA asArrayExpr() { this = TArrayExpr(result) }
+
+  PointerArithmeticOperation asPointerArithmetic() { this = TPointerArithmetic(result) }
+
+  string toString() {
+    result = this.asArrayExpr().toString() or
+    result = this.asPointerArithmetic().toString()
+  }
+
+  int getOffset() {
+    result = this.asArrayExpr().getArrayOffset().getValue().toInt()
+    or
+    exists(PointerAddExpr pointerAddition | pointerAddition = this.asPointerArithmetic() |
+      result = pointerAddition.getAnOperand().getValue().toInt() // TODO: only get the number being added
+    )
+    or
+    exists(PointerSubExpr pointerSubtraction | pointerSubtraction = this.asPointerArithmetic() |
+      result = -pointerSubtraction.getAnOperand().getValue().toInt()
+    )
+  }
+
+  Expr asExpr() {
+    result = this.asArrayExpr() or
+    /*.getArrayBase()*/ result = this.asPointerArithmetic()
+  }
+
+  DataFlow::Node getNode() { result.asExpr() = this.asExpr() }
+
+  Location getLocation() {
+    result = this.asArrayExpr().getLocation() or
+    result = this.asPointerArithmetic().getLocation()
+  }
+}
+
+/**
+ * NOTE The code in the below module is copied from
+ * `cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TaintTrackingUtil.qll` in `github/codeql`, commit hash
+ * `960e990`. This commit hash is the latest of the ones with tag  `codeql-cli-2.21.4` which is the CLI version
+ * compatible with `codeql/cpp-all: 5.0.0` that this query depends on.
+ */
+module Copied {
+  import semmle.code.cpp.ir.IR
+  import semmle.code.cpp.ir.dataflow.internal.SsaInternals as Ssa
+
+  predicate operandToInstructionTaintStep(Operand opFrom, Instruction instrTo) {
+    // Taint can flow through expressions that alter the value but preserve
+    // more than one bit of it _or_ expressions that follow data through
+    // pointer indirections.
+    instrTo.getAnOperand() = opFrom and
+    (
+      instrTo instanceof ArithmeticInstruction
+      or
+      instrTo instanceof BitwiseInstruction
+      or
+      instrTo instanceof PointerArithmeticInstruction
+    )
+    or
+    // Taint flow from an address to its dereference.
+    Ssa::isDereference(instrTo, opFrom, _)
+    or
+    // Unary instructions tend to preserve enough information in practice that we
+    // want taint to flow through.
+    // The exception is `FieldAddressInstruction`. Together with the rules below for
+    // `LoadInstruction`s and `ChiInstruction`s, flow through `FieldAddressInstruction`
+    // could cause flow into one field to come out an unrelated field.
+    // This would happen across function boundaries, where the IR would not be able to
+    // match loads to stores.
+    instrTo.(UnaryInstruction).getUnaryOperand() = opFrom and
+    (
+      not instrTo instanceof FieldAddressInstruction
+      or
+      instrTo.(FieldAddressInstruction).getField().getDeclaringType() instanceof Union
+    )
+    or
+    // Taint from int to boolean casts. This ensures that we have flow to `!x` in:
+    // ```cpp
+    // x = integer_source();
+    // if(!x) { ... }
+    // ```
+    exists(Operand zero |
+      zero.getDef().(ConstantValueInstruction).getValue() = "0" and
+      instrTo.(CompareNEInstruction).hasOperands(opFrom, zero)
+    )
+  }
+}
+
+import Copied
+
+module TrackArrayConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node node) {
+    exists(ArrayAllocation arrayAllocation | node = arrayAllocation.getNode())
+  }
+
+  predicate isSink(DataFlow::Node node) {
+    exists(PointerFormation pointerFormation | node = pointerFormation.getNode())
+  }
+
+  predicate isAdditionalFlowStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
+    operandToInstructionTaintStep(nodeFrom.asOperand(), nodeTo.asInstruction())
+  }
+}
+
+module TrackArray = DataFlow::Global<TrackArrayConfig>;
+
+predicate arrayIndexIsNegative(
+  DataFlow::Node arrayDeclarationNode, DataFlow::Node pointerFormationNode
+) {
+  /* 1. Ensure the array access is reachable from the array declaration. */
+  TrackArray::flow(arrayDeclarationNode, pointerFormationNode) and
+  /* 2. An offset cannot be negative. */
+  exists(ArrayAllocation arrayAllocation, PointerFormation pointerFormation |
+    arrayDeclarationNode = arrayAllocation.getNode() and
+    pointerFormationNode = pointerFormation.getNode()
+  |
+    pointerFormation.getOffset() < 0
+  )
+}
+
+predicate arrayIndexExceedsBounds(
+  DataFlow::Node arrayDeclarationNode, DataFlow::Node pointerFormationNode, int pointerOffset,
+  int arrayLength
+) {
+  /* 1. Ensure the array access is reachable from the array declaration. */
+  TrackArray::flow(arrayDeclarationNode, pointerFormationNode) and
+  /* 2. The offset must be at most (number of elements) + 1 = (the declared length). */
+  exists(ArrayAllocation arrayAllocation, PointerFormation pointerFormation |
+    arrayDeclarationNode = arrayAllocation.getNode() and
+    pointerFormationNode = pointerFormation.getNode() and
+    pointerOffset = pointerFormation.getOffset() and
+    arrayLength = arrayAllocation.getLength()
+  |
+    arrayLength < pointerOffset
+  )
+}
+
+import TrackArray::PathGraph
+
+from TrackArray::PathNode source, TrackArray::PathNode sink, string message
+where
+  not isExcluded(sink.getNode().asExpr(),
+    Memory1Package::pointerArithmeticFormsAnInvalidPointerQuery()) and
+  (
+    exists(int pointerOffset, int arrayLength |
+      arrayIndexExceedsBounds(source.getNode(), sink.getNode(), pointerOffset, arrayLength) and
+      message =
+        "This pointer has offset " + pointerOffset +
+          " when the minimum possible length of the object is " + arrayLength + "."
+    )
+    or
+    arrayIndexIsNegative(source.getNode(), sink.getNode()) and
+    message = "This pointer has a negative offset."
+  )
+select sink, source, sink, message
diff --git a/cpp/misra/test/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.testref b/cpp/misra/test/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.testref
new file mode 100644
index 000000000..7b2a86463
--- /dev/null
+++ b/cpp/misra/test/rules/RULE-8-7-1/PointerArgumentToCstringFunctionIsInvalid.testref
@@ -0,0 +1 @@
+c/cert/src/rules/ARR38-C/LibraryFunctionArgumentOutOfBounds.ql
\ No newline at end of file
diff --git a/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.expected b/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.expected
new file mode 100644
index 000000000..7cf6ed525
--- /dev/null
+++ b/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.expected
@@ -0,0 +1,282 @@
+WARNING: unused method 'getAllocFunctionCall' (PointerArithmeticFormsAnInvalidPointer.ql:74,30-50)
+edges
+| test.cpp:3:65:3:69 | array | test.cpp:5:17:5:21 | array | provenance |  |
+| test.cpp:5:17:5:21 | array | test.cpp:6:17:6:25 | ... + ... | provenance | Config |
+| test.cpp:5:17:5:21 | array | test.cpp:7:17:7:25 | ... + ... | provenance | Config |
+| test.cpp:5:17:5:21 | array | test.cpp:9:7:9:15 | ... + ... | provenance | Config |
+| test.cpp:5:17:5:21 | array | test.cpp:11:7:12:7 | ... + ... | provenance | Config |
+| test.cpp:5:17:5:21 | array | test.cpp:13:19:13:27 | ... - ... | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:18:16:18:23 | access to array | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:19:16:19:23 | access to array | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:20:16:20:23 | access to array | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:21:16:21:23 | access to array | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:23:18:23:25 | access to array | provenance | Config |
+| test.cpp:16:59:16:63 | array | test.cpp:25:18:25:26 | access to array | provenance | Config |
+| test.cpp:28:56:28:60 | array | test.cpp:30:17:30:21 | array | provenance |  |
+| test.cpp:30:17:30:21 | array | test.cpp:31:17:31:25 | ... + ... | provenance | Config |
+| test.cpp:30:17:30:21 | array | test.cpp:33:17:33:25 | ... + ... | provenance | Config |
+| test.cpp:30:17:30:21 | array | test.cpp:35:17:35:25 | ... + ... | provenance | Config |
+| test.cpp:30:17:30:21 | array | test.cpp:37:19:37:27 | ... + ... | provenance | Config |
+| test.cpp:30:17:30:21 | array | test.cpp:39:19:39:27 | ... + ... | provenance | Config |
+| test.cpp:30:17:30:21 | array | test.cpp:41:19:41:27 | ... - ... | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:47:7:47:14 | access to array | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:48:16:48:23 | access to array | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:51:16:51:23 | access to array | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:53:16:53:23 | access to array | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:55:18:55:25 | access to array | provenance | Config |
+| test.cpp:44:50:44:54 | array | test.cpp:57:18:57:26 | access to array | provenance | Config |
+| test.cpp:60:56:60:60 | array | test.cpp:62:17:62:21 | array | provenance |  |
+| test.cpp:62:17:62:21 | array | test.cpp:64:7:64:15 | ... + ... | provenance | Config |
+| test.cpp:62:17:62:21 | array | test.cpp:65:17:65:25 | ... + ... | provenance | Config |
+| test.cpp:62:17:62:21 | array | test.cpp:68:17:68:25 | ... + ... | provenance | Config |
+| test.cpp:62:17:62:21 | array | test.cpp:70:19:70:27 | ... + ... | provenance | Config |
+| test.cpp:62:17:62:21 | array | test.cpp:72:19:72:27 | ... - ... | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:77:16:77:23 | access to array | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:78:16:78:23 | access to array | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:79:16:79:23 | access to array | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:82:16:82:23 | access to array | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:84:18:84:25 | access to array | provenance | Config |
+| test.cpp:75:50:75:54 | array | test.cpp:86:18:86:26 | access to array | provenance | Config |
+| test.cpp:89:57:89:61 | array | test.cpp:91:17:91:21 | array | provenance |  |
+| test.cpp:91:17:91:21 | array | test.cpp:93:7:93:15 | ... + ... | provenance | Config |
+| test.cpp:91:17:91:21 | array | test.cpp:95:7:95:15 | ... + ... | provenance | Config |
+| test.cpp:91:17:91:21 | array | test.cpp:96:17:96:25 | ... + ... | provenance | Config |
+| test.cpp:91:17:91:21 | array | test.cpp:98:19:98:27 | ... + ... | provenance | Config |
+| test.cpp:91:17:91:21 | array | test.cpp:100:19:100:27 | ... - ... | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:106:7:106:14 | access to array | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:108:7:108:14 | access to array | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:110:7:110:14 | access to array | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:112:7:112:14 | access to array | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:114:18:114:25 | access to array | provenance | Config |
+| test.cpp:103:51:103:55 | array | test.cpp:116:18:116:26 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:120:17:120:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:120:17:120:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:121:17:121:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:121:17:121:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:122:17:122:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:122:17:122:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:124:18:124:25 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:124:18:124:28 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:127:17:127:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:127:17:127:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:128:17:128:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:128:17:128:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:129:17:129:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:129:17:129:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:132:18:132:25 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:132:18:132:28 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:135:17:135:24 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:135:17:135:27 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:137:18:137:25 | access to array | provenance | Config |
+| test.cpp:119:57:119:61 | array | test.cpp:137:18:137:28 | access to array | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:142:20:142:31 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:142:20:142:35 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:144:7:145:10 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:148:20:148:31 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:148:20:148:35 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:150:9:151:9 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:153:9:153:20 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:153:9:153:24 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:156:7:157:7 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:159:21:159:32 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:159:21:159:36 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:162:9:162:18 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:165:20:165:31 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:165:20:165:35 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:167:7:168:10 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:169:19:169:30 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:169:19:169:34 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:171:9:171:20 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:171:9:171:24 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:173:20:173:31 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:173:20:173:35 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:177:9:177:20 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:177:9:177:24 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:179:20:181:8 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:183:21:183:32 | * ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:183:21:183:36 | ... + ... | provenance | Config |
+| test.cpp:141:63:141:67 | array | test.cpp:186:9:186:20 | * ... | provenance | Config |
+| test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | test.cpp:195:7:195:36 | stack_single_dimensional_array | provenance |  |
+| test.cpp:195:7:195:36 | stack_single_dimensional_array | test.cpp:3:65:3:69 | array | provenance |  |
+| test.cpp:195:7:195:36 | stack_single_dimensional_array | test.cpp:197:7:197:36 | stack_single_dimensional_array | provenance |  |
+| test.cpp:197:7:197:36 | stack_single_dimensional_array | test.cpp:16:59:16:63 | array | provenance |  |
+| test.cpp:215:7:215:57 | call to malloc | test.cpp:215:7:215:57 | call to malloc | provenance |  |
+| test.cpp:215:7:215:57 | call to malloc | test.cpp:220:7:220:37 | single_dimensional_array_malloc | provenance |  |
+| test.cpp:215:7:215:57 | call to malloc | test.cpp:220:7:220:37 | single_dimensional_array_malloc | provenance | Config |
+| test.cpp:217:7:217:56 | call to calloc | test.cpp:217:7:217:56 | call to calloc | provenance |  |
+| test.cpp:217:7:217:56 | call to calloc | test.cpp:225:48:225:78 | single_dimensional_array_calloc | provenance |  |
+| test.cpp:219:43:220:77 | call to realloc | test.cpp:219:43:220:77 | call to realloc | provenance |  |
+| test.cpp:219:43:220:77 | call to realloc | test.cpp:229:7:229:38 | single_dimensional_array_realloc | provenance |  |
+| test.cpp:220:7:220:37 | single_dimensional_array_malloc | test.cpp:222:48:222:78 | single_dimensional_array_malloc | provenance |  |
+| test.cpp:222:48:222:78 | single_dimensional_array_malloc | test.cpp:28:56:28:60 | array | provenance |  |
+| test.cpp:222:48:222:78 | single_dimensional_array_malloc | test.cpp:223:42:223:72 | single_dimensional_array_malloc | provenance |  |
+| test.cpp:223:42:223:72 | single_dimensional_array_malloc | test.cpp:44:50:44:54 | array | provenance |  |
+| test.cpp:225:48:225:78 | single_dimensional_array_calloc | test.cpp:60:56:60:60 | array | provenance |  |
+| test.cpp:225:48:225:78 | single_dimensional_array_calloc | test.cpp:226:42:226:72 | single_dimensional_array_calloc | provenance |  |
+| test.cpp:226:42:226:72 | single_dimensional_array_calloc | test.cpp:75:50:75:54 | array | provenance |  |
+| test.cpp:229:7:229:38 | single_dimensional_array_realloc | test.cpp:89:57:89:61 | array | provenance |  |
+| test.cpp:229:7:229:38 | single_dimensional_array_realloc | test.cpp:230:43:230:74 | single_dimensional_array_realloc | provenance |  |
+| test.cpp:230:43:230:74 | single_dimensional_array_realloc | test.cpp:103:51:103:55 | array | provenance |  |
+| test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:239:50:239:78 | stack_multi_dimensional_array | provenance |  |
+| test.cpp:239:50:239:78 | stack_multi_dimensional_array | test.cpp:119:57:119:61 | array | provenance |  |
+| test.cpp:239:50:239:78 | stack_multi_dimensional_array | test.cpp:241:7:241:35 | stack_multi_dimensional_array | provenance |  |
+| test.cpp:241:7:241:35 | stack_multi_dimensional_array | test.cpp:141:63:141:67 | array | provenance |  |
+nodes
+| test.cpp:3:65:3:69 | array | semmle.label | array |
+| test.cpp:5:17:5:21 | array | semmle.label | array |
+| test.cpp:6:17:6:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:7:17:7:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:9:7:9:15 | ... + ... | semmle.label | ... + ... |
+| test.cpp:11:7:12:7 | ... + ... | semmle.label | ... + ... |
+| test.cpp:13:19:13:27 | ... - ... | semmle.label | ... - ... |
+| test.cpp:16:59:16:63 | array | semmle.label | array |
+| test.cpp:18:16:18:23 | access to array | semmle.label | access to array |
+| test.cpp:19:16:19:23 | access to array | semmle.label | access to array |
+| test.cpp:20:16:20:23 | access to array | semmle.label | access to array |
+| test.cpp:21:16:21:23 | access to array | semmle.label | access to array |
+| test.cpp:23:18:23:25 | access to array | semmle.label | access to array |
+| test.cpp:25:18:25:26 | access to array | semmle.label | access to array |
+| test.cpp:28:56:28:60 | array | semmle.label | array |
+| test.cpp:30:17:30:21 | array | semmle.label | array |
+| test.cpp:31:17:31:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:33:17:33:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:35:17:35:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:37:19:37:27 | ... + ... | semmle.label | ... + ... |
+| test.cpp:39:19:39:27 | ... + ... | semmle.label | ... + ... |
+| test.cpp:41:19:41:27 | ... - ... | semmle.label | ... - ... |
+| test.cpp:44:50:44:54 | array | semmle.label | array |
+| test.cpp:47:7:47:14 | access to array | semmle.label | access to array |
+| test.cpp:48:16:48:23 | access to array | semmle.label | access to array |
+| test.cpp:51:16:51:23 | access to array | semmle.label | access to array |
+| test.cpp:53:16:53:23 | access to array | semmle.label | access to array |
+| test.cpp:55:18:55:25 | access to array | semmle.label | access to array |
+| test.cpp:57:18:57:26 | access to array | semmle.label | access to array |
+| test.cpp:60:56:60:60 | array | semmle.label | array |
+| test.cpp:62:17:62:21 | array | semmle.label | array |
+| test.cpp:64:7:64:15 | ... + ... | semmle.label | ... + ... |
+| test.cpp:65:17:65:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:68:17:68:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:70:19:70:27 | ... + ... | semmle.label | ... + ... |
+| test.cpp:72:19:72:27 | ... - ... | semmle.label | ... - ... |
+| test.cpp:75:50:75:54 | array | semmle.label | array |
+| test.cpp:77:16:77:23 | access to array | semmle.label | access to array |
+| test.cpp:78:16:78:23 | access to array | semmle.label | access to array |
+| test.cpp:79:16:79:23 | access to array | semmle.label | access to array |
+| test.cpp:82:16:82:23 | access to array | semmle.label | access to array |
+| test.cpp:84:18:84:25 | access to array | semmle.label | access to array |
+| test.cpp:86:18:86:26 | access to array | semmle.label | access to array |
+| test.cpp:89:57:89:61 | array | semmle.label | array |
+| test.cpp:91:17:91:21 | array | semmle.label | array |
+| test.cpp:93:7:93:15 | ... + ... | semmle.label | ... + ... |
+| test.cpp:95:7:95:15 | ... + ... | semmle.label | ... + ... |
+| test.cpp:96:17:96:25 | ... + ... | semmle.label | ... + ... |
+| test.cpp:98:19:98:27 | ... + ... | semmle.label | ... + ... |
+| test.cpp:100:19:100:27 | ... - ... | semmle.label | ... - ... |
+| test.cpp:103:51:103:55 | array | semmle.label | array |
+| test.cpp:106:7:106:14 | access to array | semmle.label | access to array |
+| test.cpp:108:7:108:14 | access to array | semmle.label | access to array |
+| test.cpp:110:7:110:14 | access to array | semmle.label | access to array |
+| test.cpp:112:7:112:14 | access to array | semmle.label | access to array |
+| test.cpp:114:18:114:25 | access to array | semmle.label | access to array |
+| test.cpp:116:18:116:26 | access to array | semmle.label | access to array |
+| test.cpp:119:57:119:61 | array | semmle.label | array |
+| test.cpp:120:17:120:24 | access to array | semmle.label | access to array |
+| test.cpp:120:17:120:27 | access to array | semmle.label | access to array |
+| test.cpp:121:17:121:24 | access to array | semmle.label | access to array |
+| test.cpp:121:17:121:27 | access to array | semmle.label | access to array |
+| test.cpp:122:17:122:24 | access to array | semmle.label | access to array |
+| test.cpp:122:17:122:27 | access to array | semmle.label | access to array |
+| test.cpp:124:18:124:25 | access to array | semmle.label | access to array |
+| test.cpp:124:18:124:28 | access to array | semmle.label | access to array |
+| test.cpp:127:17:127:24 | access to array | semmle.label | access to array |
+| test.cpp:127:17:127:27 | access to array | semmle.label | access to array |
+| test.cpp:128:17:128:24 | access to array | semmle.label | access to array |
+| test.cpp:128:17:128:27 | access to array | semmle.label | access to array |
+| test.cpp:129:17:129:24 | access to array | semmle.label | access to array |
+| test.cpp:129:17:129:27 | access to array | semmle.label | access to array |
+| test.cpp:132:18:132:25 | access to array | semmle.label | access to array |
+| test.cpp:132:18:132:28 | access to array | semmle.label | access to array |
+| test.cpp:135:17:135:24 | access to array | semmle.label | access to array |
+| test.cpp:135:17:135:27 | access to array | semmle.label | access to array |
+| test.cpp:137:18:137:25 | access to array | semmle.label | access to array |
+| test.cpp:137:18:137:28 | access to array | semmle.label | access to array |
+| test.cpp:141:63:141:67 | array | semmle.label | array |
+| test.cpp:142:20:142:31 | * ... | semmle.label | * ... |
+| test.cpp:142:20:142:35 | ... + ... | semmle.label | ... + ... |
+| test.cpp:144:7:145:10 | * ... | semmle.label | * ... |
+| test.cpp:148:20:148:31 | * ... | semmle.label | * ... |
+| test.cpp:148:20:148:35 | ... + ... | semmle.label | ... + ... |
+| test.cpp:150:9:151:9 | ... + ... | semmle.label | ... + ... |
+| test.cpp:153:9:153:20 | * ... | semmle.label | * ... |
+| test.cpp:153:9:153:24 | ... + ... | semmle.label | ... + ... |
+| test.cpp:156:7:157:7 | ... + ... | semmle.label | ... + ... |
+| test.cpp:159:21:159:32 | * ... | semmle.label | * ... |
+| test.cpp:159:21:159:36 | ... + ... | semmle.label | ... + ... |
+| test.cpp:162:9:162:18 | ... + ... | semmle.label | ... + ... |
+| test.cpp:165:20:165:31 | * ... | semmle.label | * ... |
+| test.cpp:165:20:165:35 | ... + ... | semmle.label | ... + ... |
+| test.cpp:167:7:168:10 | * ... | semmle.label | * ... |
+| test.cpp:169:19:169:30 | * ... | semmle.label | * ... |
+| test.cpp:169:19:169:34 | ... + ... | semmle.label | ... + ... |
+| test.cpp:171:9:171:20 | * ... | semmle.label | * ... |
+| test.cpp:171:9:171:24 | ... + ... | semmle.label | ... + ... |
+| test.cpp:173:20:173:31 | * ... | semmle.label | * ... |
+| test.cpp:173:20:173:35 | ... + ... | semmle.label | ... + ... |
+| test.cpp:177:9:177:20 | * ... | semmle.label | * ... |
+| test.cpp:177:9:177:24 | ... + ... | semmle.label | ... + ... |
+| test.cpp:179:20:181:8 | * ... | semmle.label | * ... |
+| test.cpp:183:21:183:32 | * ... | semmle.label | * ... |
+| test.cpp:183:21:183:36 | ... + ... | semmle.label | ... + ... |
+| test.cpp:186:9:186:20 | * ... | semmle.label | * ... |
+| test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | semmle.label | definition of stack_single_dimensional_array |
+| test.cpp:195:7:195:36 | stack_single_dimensional_array | semmle.label | stack_single_dimensional_array |
+| test.cpp:197:7:197:36 | stack_single_dimensional_array | semmle.label | stack_single_dimensional_array |
+| test.cpp:215:7:215:57 | call to malloc | semmle.label | call to malloc |
+| test.cpp:215:7:215:57 | call to malloc | semmle.label | call to malloc |
+| test.cpp:217:7:217:56 | call to calloc | semmle.label | call to calloc |
+| test.cpp:217:7:217:56 | call to calloc | semmle.label | call to calloc |
+| test.cpp:219:43:220:77 | call to realloc | semmle.label | call to realloc |
+| test.cpp:219:43:220:77 | call to realloc | semmle.label | call to realloc |
+| test.cpp:220:7:220:37 | single_dimensional_array_malloc | semmle.label | single_dimensional_array_malloc |
+| test.cpp:222:48:222:78 | single_dimensional_array_malloc | semmle.label | single_dimensional_array_malloc |
+| test.cpp:223:42:223:72 | single_dimensional_array_malloc | semmle.label | single_dimensional_array_malloc |
+| test.cpp:225:48:225:78 | single_dimensional_array_calloc | semmle.label | single_dimensional_array_calloc |
+| test.cpp:226:42:226:72 | single_dimensional_array_calloc | semmle.label | single_dimensional_array_calloc |
+| test.cpp:229:7:229:38 | single_dimensional_array_realloc | semmle.label | single_dimensional_array_realloc |
+| test.cpp:230:43:230:74 | single_dimensional_array_realloc | semmle.label | single_dimensional_array_realloc |
+| test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | semmle.label | definition of stack_multi_dimensional_array |
+| test.cpp:239:50:239:78 | stack_multi_dimensional_array | semmle.label | stack_multi_dimensional_array |
+| test.cpp:241:7:241:35 | stack_multi_dimensional_array | semmle.label | stack_multi_dimensional_array |
+subpaths
+#select
+| test.cpp:11:7:12:7 | ... + ... | test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | test.cpp:11:7:12:7 | ... + ... | This pointer has offset 4 when the minimum possible length of the object is 3. |
+| test.cpp:13:19:13:27 | ... - ... | test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | test.cpp:13:19:13:27 | ... - ... | This pointer has a negative offset. |
+| test.cpp:23:18:23:25 | access to array | test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | test.cpp:23:18:23:25 | access to array | This pointer has offset 4 when the minimum possible length of the object is 3. |
+| test.cpp:25:18:25:26 | access to array | test.cpp:192:7:192:36 | definition of stack_single_dimensional_array | test.cpp:25:18:25:26 | access to array | This pointer has a negative offset. |
+| test.cpp:33:17:33:25 | ... + ... | test.cpp:215:7:215:57 | call to malloc | test.cpp:33:17:33:25 | ... + ... | This pointer has offset 2 when the minimum possible length of the object is 1. |
+| test.cpp:35:17:35:25 | ... + ... | test.cpp:215:7:215:57 | call to malloc | test.cpp:35:17:35:25 | ... + ... | This pointer has offset 3 when the minimum possible length of the object is 1. |
+| test.cpp:37:19:37:27 | ... + ... | test.cpp:215:7:215:57 | call to malloc | test.cpp:37:19:37:27 | ... + ... | This pointer has offset 4 when the minimum possible length of the object is 1. |
+| test.cpp:39:19:39:27 | ... + ... | test.cpp:215:7:215:57 | call to malloc | test.cpp:39:19:39:27 | ... + ... | This pointer has offset 5 when the minimum possible length of the object is 1. |
+| test.cpp:41:19:41:27 | ... - ... | test.cpp:215:7:215:57 | call to malloc | test.cpp:41:19:41:27 | ... - ... | This pointer has a negative offset. |
+| test.cpp:51:16:51:23 | access to array | test.cpp:215:7:215:57 | call to malloc | test.cpp:51:16:51:23 | access to array | This pointer has offset 2 when the minimum possible length of the object is 1. |
+| test.cpp:53:16:53:23 | access to array | test.cpp:215:7:215:57 | call to malloc | test.cpp:53:16:53:23 | access to array | This pointer has offset 3 when the minimum possible length of the object is 1. |
+| test.cpp:55:18:55:25 | access to array | test.cpp:215:7:215:57 | call to malloc | test.cpp:55:18:55:25 | access to array | This pointer has offset 4 when the minimum possible length of the object is 1. |
+| test.cpp:57:18:57:26 | access to array | test.cpp:215:7:215:57 | call to malloc | test.cpp:57:18:57:26 | access to array | This pointer has a negative offset. |
+| test.cpp:68:17:68:25 | ... + ... | test.cpp:217:7:217:56 | call to calloc | test.cpp:68:17:68:25 | ... + ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:70:19:70:27 | ... + ... | test.cpp:217:7:217:56 | call to calloc | test.cpp:70:19:70:27 | ... + ... | This pointer has offset 4 when the minimum possible length of the object is 2. |
+| test.cpp:72:19:72:27 | ... - ... | test.cpp:217:7:217:56 | call to calloc | test.cpp:72:19:72:27 | ... - ... | This pointer has a negative offset. |
+| test.cpp:82:16:82:23 | access to array | test.cpp:217:7:217:56 | call to calloc | test.cpp:82:16:82:23 | access to array | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:84:18:84:25 | access to array | test.cpp:217:7:217:56 | call to calloc | test.cpp:84:18:84:25 | access to array | This pointer has offset 4 when the minimum possible length of the object is 2. |
+| test.cpp:86:18:86:26 | access to array | test.cpp:217:7:217:56 | call to calloc | test.cpp:86:18:86:26 | access to array | This pointer has a negative offset. |
+| test.cpp:98:19:98:27 | ... + ... | test.cpp:219:43:220:77 | call to realloc | test.cpp:98:19:98:27 | ... + ... | This pointer has offset 4 when the minimum possible length of the object is 3. |
+| test.cpp:100:19:100:27 | ... - ... | test.cpp:219:43:220:77 | call to realloc | test.cpp:100:19:100:27 | ... - ... | This pointer has a negative offset. |
+| test.cpp:114:18:114:25 | access to array | test.cpp:219:43:220:77 | call to realloc | test.cpp:114:18:114:25 | access to array | This pointer has offset 4 when the minimum possible length of the object is 3. |
+| test.cpp:116:18:116:26 | access to array | test.cpp:219:43:220:77 | call to realloc | test.cpp:116:18:116:26 | access to array | This pointer has a negative offset. |
+| test.cpp:124:18:124:28 | access to array | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:124:18:124:28 | access to array | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:132:18:132:28 | access to array | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:132:18:132:28 | access to array | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:137:18:137:25 | access to array | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:137:18:137:25 | access to array | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:159:21:159:36 | ... + ... | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:159:21:159:36 | ... + ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:162:9:162:18 | ... + ... | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:162:9:162:18 | ... + ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:173:20:173:35 | ... + ... | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:173:20:173:35 | ... + ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:183:21:183:32 | * ... | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:183:21:183:32 | * ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
+| test.cpp:186:9:186:20 | * ... | test.cpp:233:7:233:35 | definition of stack_multi_dimensional_array | test.cpp:186:9:186:20 | * ... | This pointer has offset 3 when the minimum possible length of the object is 2. |
diff --git a/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.qlref b/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.qlref
new file mode 100644
index 000000000..a512fe0a6
--- /dev/null
+++ b/cpp/misra/test/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.qlref
@@ -0,0 +1 @@
+rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql
\ No newline at end of file
diff --git a/cpp/misra/test/rules/RULE-8-7-1/test.cpp b/cpp/misra/test/rules/RULE-8-7-1/test.cpp
new file mode 100644
index 000000000..2150935e2
--- /dev/null
+++ b/cpp/misra/test/rules/RULE-8-7-1/test.cpp
@@ -0,0 +1,512 @@
+#include <cstdlib>
+#include <cstring>
+#include <ctime>
+#include <cwchar>
+
+void stack_allocated_single_dimensional_pointer_arithmetic(int *array) {
+  /* 1. Pointer formed from performing arithmetic */
+  int *valid1 = array;     // COMPLIANT: pointer is within boundary
+  int *valid2 = array + 1; // COMPLIANT: pointer is within boundary
+  int *valid3 = array + 2; // COMPLIANT: pointer is within boundary
+  int *valid4 =
+      array + 3; // COMPLIANT: pointer points one beyond the last element
+  int *invalid1 =
+      array +
+      4; // NON_COMPLIANT: pointer points more than one beyond the last element
+  int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void stack_allocated_single_dimensional_array_access(int *array) {
+  /* 2. Array Access (entails pointer arithmetic) */
+  int valid1 = array[0];   // COMPLIANT: pointer is within boundary
+  int valid2 = array[1];   // COMPLIANT: pointer is within boundary
+  int valid3 = array[2];   // COMPLIANT: pointer is within boundary
+  int valid4 = array[3];   // COMPLIANT: pointer points one beyond the last
+                           // element, but non-compliant to Rule 4.1.3
+  int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element
+  int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void malloc_single_dimensional_pointer_arithmetic(int *array) { // [1, 4]
+  /* 1. Pointer formed from performing arithmetic */
+  int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 1)
+  int *valid2 = array + 1; // COMPLIANT: pointer points more than one beyond the
+                           // last element (lower bound: 1)
+  int *valid3 = array + 2; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 1)
+  int *valid4 = array + 3; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 1)
+  int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
+                             // beyond the last element (lower bound: 1)
+  int *invalid2 = array + 5; // NON_COMPLIANT: pointer points more than one
+                             // beyond the last element (lower bound: 1)
+  int *invalid3 = array - 1; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void malloc_single_dimensional_array_access(int *array) { // [1, 4]
+  /* 2. Array Access (entails pointer arithmetic) */
+  int valid1 =
+      array[0]; // COMPLIANT: pointer is within boundary (lower bound: 1)
+  int valid2 = array[1]; // COMPLIANT: pointer points more than one beyond the
+                         // last element, but non-compliant to Rule 4.1.3 (lower
+                         // bound: 1)
+  int valid3 = array[2]; // NON_COMPLIANT: pointer points more than one beyond
+                         // the last element (lower bound: 1)
+  int valid4 = array[3]; // NON_COMPLIANT: pointer points more than one beyond
+                         // the last element (lower bound: 1)
+  int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 1)
+  int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void calloc_single_dimensional_pointer_arithmetic(int *array) { // [2, 5]
+  /* 1. Pointer formed from performing arithmetic */
+  int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 2)
+  int *valid2 =
+      array + 1; // COMPLIANT: pointer is within boundary (lower bound: 2)
+  int *valid3 = array + 2; // COMPLIANT: pointer points more than one beyond the
+                           // last element, but non-compliant to Rule 4.1.3
+                           // (lower bound: 2)
+  int *valid4 = array + 3; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 2)
+  int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
+                             // beyond the last element (lower bound: 2)
+  int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void calloc_single_dimensional_array_access(int *array) { // [2, 5]
+  /* 2. Array Access (entails pointer arithmetic) */
+  int valid1 = array[0];   // COMPLIANT: pointer is within boundary
+  int valid2 = array[1];   // COMPLIANT: pointer is within boundary
+  int valid3 = array[2];   // COMPLIANT: pointer points more than one beyond the
+                           // last element, but non-compliant to Rule 4.1.3
+                           // (lower bound: 2)
+  int valid4 = array[3];   // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 2)
+  int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one
+                           // beyond the last element (lower bound: 2)
+  int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void realloc_single_dimensional_pointer_arithmetic(int *array) { // [3, 6]
+  /* 1. Pointer formed from performing arithmetic */
+  int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int *valid2 =
+      array + 1; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int *valid3 =
+      array + 2; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int *valid4 = array + 3;   // COMPLIANT: pointer points one beyond the last
+                             // element (lower bound: 3)
+  int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
+                             // beyond the last element (lower bound: 3)
+  int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void realloc_single_dimensional_array_access(int *array) { // [3, 6]
+  /* 2. Array Access (entails pointer arithmetic) */
+  int valid1 =
+      array[0]; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int valid2 =
+      array[1]; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int valid3 =
+      array[2]; // COMPLIANT: pointer is within boundary (lower bound: 3)
+  int valid4 =
+      array[3]; // COMPLIANT: pointer points one beyond the last
+                // element, but non-compliant to Rule 4.1.3 (lower bound: 3)
+  int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
+                           // the last element (lower bound: 3)
+  int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
+}
+
+void stack_allocated_multi_dimensional_array_access(int array[2][3]) {
+  int valid11 = array[0][0];  // COMPLIANT: pointer is within boundary
+  int valid12 = array[0][1];  // COMPLIANT: pointer is within boundary
+  int valid13 = array[0][2];  // COMPLIANT: pointer points one beyond the last
+                              // element, but non-compliant to Rule 4.1.3
+  int invalid1 = array[0][3]; // NON_COMPLIANT: pointer points more than one
+                              // beyond the last element
+
+  int valid21 = array[1][0]; // COMPLIANT: pointer is within boundary
+  int valid22 = array[1][1]; // COMPLIANT: pointer is within boundary
+  int valid23 = array[1][2]; // COMPLIANT: pointer points one beyond the last
+                             // element, but non-compliant to Rule 4.1.3
+
+  int invalid2 = array[1][3]; // NON_COMPLIANT: pointer points more than one
+                              // beyond the last element
+
+  int valid31 = array[2][0];  // COMPLIANT: pointer points one beyond the last
+                              // element, but non-compliant to Rule 4.1.3
+  int invalid3 = array[3][0]; // NON_COMPLIANT: pointer points more than one
+                              // beyond the last element
+}
+
+void stack_allocated_multi_dimensional_pointer_arithmetic(int array[2][3]) {
+  int valid111 = *(*(array + 0) + 0); // COMPLIANT: pointer is within boundary
+  int valid112 = *(
+      *(array +
+        0)); // COMPLIANT: pointer is within boundary (equivalent to the above)
+  int valid113 = **array; // COMPLIANT: pointer is within boundary (equivalent
+                          // to the above)
+  int valid121 = *(*(array + 0) + 1); // COMPLIANT: pointer is within boundary
+  int valid122 =
+      *(*array +
+        1); // COMPLIANT: pointer is within boundary (equivalent to the above)
+  int valid131 =
+      *(*(array + 0) + 2); // COMPLIANT: pointer points one beyond the last
+                           // element, but non-compliant to Rule 4.1.3
+  int valid132 = *(
+      *array +
+      2); // COMPLIANT: pointer points one beyond the last
+          // element, but non-compliant to Rule 4.1.3 (equivalent to the above)
+  int invalid11 = *(*(array + 0) + 3); // NON_COMPLIANT: pointer points more
+                                       // than one beyond the last element
+  int invalid12 =
+      *(*array + 3); // NON_COMPLIANT: pointer points more than
+                     // one beyond the last element (equivalent to the above)
+
+  int valid211 = *(*(array + 1) + 0); // COMPLIANT: pointer is within boundary
+  int valid212 = *(
+      *(array +
+        1)); // COMPLIANT: pointer is within boundary (equivalent to the above)
+  int valid22 = *(*(array + 1) + 1); // COMPLIANT: pointer is within boundary
+  int valid23 =
+      *(*(array + 1) + 2); // COMPLIANT: pointer points one beyond the last
+                           // element, but non-compliant to Rule 4.1.3
+  int invalid2 = *(*(array + 1) + 3); // NON_COMPLIANT: pointer points more than
+                                      // one beyond the last element
+
+  int valid311 =
+      *(*(array + 2) + 0); // COMPLIANT: pointer points one beyond the last
+                           // element, but non-compliant to Rule 4.1.3
+  int valid312 = *(*(
+      array +
+      2)); // COMPLIANT: pointer points one beyond the last
+           // element, but non-compliant to Rule 4.1.3 (equivalent to the above)
+  int invalid31 = *(*(array + 3) + 0); // NON_COMPLIANT: pointer points more
+                                       // than one beyond the last element
+  int invalid32 =
+      *(*(array + 3)); // NON_COMPLIANT: pointer points more than
+                       // one beyond the last element (equivalent to the above)
+}
+
+/**
+ * Test code that was copied from that of ARR38-C, at revision `d82ed6ee`.
+ */
+namespace ARR38_C_copied {
+char *get_ca_5(void) {
+  void *ptr = malloc(5 * sizeof(char));
+  memset(ptr, 0, 5 * sizeof(char));
+  return (char *)ptr;
+}
+
+int compare(void *a, void *b) {}
+
+void test_strings_loop(void) {
+  char ca5[5] = "test"; // ok
+  char buf5[5] = {0};
+
+  for (int i = 0; i < 5; i++) {
+    strcpy(buf5, ca5);         // COMPLIANT
+    strcpy(buf5 + i, ca5);     // NON_COMPLIANT[FALSE_NEGATIVE]
+    strncpy(buf5, ca5, i);     // COMPLIANT
+    strncpy(buf5, ca5, i + 1); // NON_COMPLIANT[FALSE_NEGATIVE]
+  }
+}
+
+void test_strings(int flow, int unk_size) {
+  char ca5_good[5] = "test";  // ok
+  char ca6_good[6] = "test1"; // ok
+
+  wchar_t wa5_good[5] = L"test"; // ok
+  wchar_t wa6_good[6] = L"test"; // ok
+
+  // strchr
+  strchr(ca5_good, 't');     // COMPLIANT
+  strchr(ca5_good + 4, 't'); // COMPLIANT
+  strchr(ca5_good + 5, 't'); // NON_COMPLIANT
+
+  if (flow) {
+    // strcpy from literal
+    strcpy(ca5_good, "test1"); // NON_COMPLIANT
+  }
+
+  if (flow) {
+    // strcpy to char buffer indirect
+    strcpy(get_ca_5(), ca5_good); // COMPLIANT
+    strcpy(get_ca_5(), ca6_good); // NON_COMPLIANT
+  }
+
+  // strcpy between string buffers (must be null-terminated)
+  if (flow) {
+    strcpy(ca5_good, ca6_good);
+  } // NON_COMPLIANT
+  if (flow) {
+    strcpy(get_ca_5(), ca5_good);
+  } // COMPLIANT
+  if (flow) {
+    strcpy(get_ca_5(), ca6_good);
+  } // NON_COMPLIANT
+  if (flow) {
+    strcpy(ca5_good, get_ca_5());
+  } // NON_COMPLIANT[FALSE_NEGATIVE]
+
+  // strncpy between char buffers (does not have to be null-terminated)
+  if (flow) {
+    strncpy(ca5_good, ca6_good, 4);
+  } // COMPLIANT
+  if (flow) {
+    strncpy(ca5_good, ca6_good, 5);
+  } // COMPLIANT
+  if (flow) {
+    strncpy(ca5_good, ca5_good, 5);
+  } // COMPLIANT
+  if (flow) {
+    strncpy(ca5_good + 1, ca5_good + 2, 3);
+  } // COMPLIANT
+  if (flow) {
+    strncpy(ca5_good + 1, ca5_good + 2, 2);
+  } // COMPLIANT
+
+  // wrong allocation size
+  char *p1 = (char *)malloc(strlen(ca5_good) + 1);
+  char *p2 = (char *)malloc(strlen(ca5_good));
+
+  // memcpy with strings and strlen
+  if (flow) {
+    memcpy(p1, ca5_good, strlen(ca5_good) + 1);
+  } // COMPLIANT
+  if (flow) {
+    memcpy(p2, ca5_good, strlen(ca5_good) + 1);
+  } // NON_COMPLIANT
+  if (flow) {
+    memcpy(p2 + 1, ca5_good, strlen(ca5_good) - 1);
+  } // COMPLIANT
+  if (flow) {
+    memcpy(p1, ca5_good, strlen(ca5_good));
+  } // COMPLIANT - but not terminated
+  if (flow) {
+    memcpy(p2, ca5_good, strlen(ca5_good));
+  } // COMPLIANT - but not terminated
+
+  // strcat
+  if (flow) {
+    char buf0[10]; // memset after first use
+    char buf1[10]; // no memset
+    char buf2[10]; // memset before first use
+    char buf3[10] = {'\0'};
+    char buf4[10] = "12345";
+
+    strcat(buf0, " "); // NON_COMPLIANT[FALSE_NEGATIVE] - not null terminated at
+                       // initialization
+
+    memset(buf0, 0, sizeof(buf0)); // COMPLIANT
+    memset(buf2, 0, sizeof(buf2)); // COMPLIANT
+
+    strcat(buf1, " ");     // NON_COMPLIANT - not null terminated
+    strcat(buf2, " ");     // COMPLIANT
+    strcat(buf3, " ");     // COMPLIANT
+    strcat(buf4, "12345"); // NON_COMPLIANT
+
+    strcat(get_ca_5(), "12345");    // NON_COMPLIANT
+    strcat(get_ca_5(), "1234");     // COMPLIANT
+    strcat(get_ca_5() + 1, "1234"); // NON_COMPLIANT
+  }
+
+  // strcmp
+  if (flow) {
+    strcmp(ca5_good, ca5_good); // COMPLIANT
+    strcmp(ca5_good, ca6_good); // COMPLIANT
+    strcmp(ca6_good, ca5_good); // COMPLIANT
+  }
+}
+
+void test_wrong_buf_size(void) {
+  // mbstowcs
+  {
+    char buf1[128] = {0};
+    char buf2[128];
+    wchar_t wbuf[128];
+
+    mbstowcs(wbuf, buf1, sizeof(wbuf)); // NON_COMPLIANT - count too large
+    mbstowcs(wbuf, buf1, sizeof(buf1)); // COMPLIANT - but wrong arithmetic
+    mbstowcs(wbuf, buf2,
+             sizeof(wbuf) /
+                 sizeof(wchar_t)); // NON_COMPLIANT - not null-terminated
+    mbstowcs(wbuf, buf1, sizeof(wbuf) / sizeof(wchar_t)); // COMPLIANT
+  }
+
+  // wcstombs
+  {
+    char buf[128];
+    wchar_t wbuf[128] = {0};
+    wcstombs(buf, wbuf, sizeof(wbuf)); // NON_COMPLIANT - count too large
+    wcstombs(buf, wbuf, sizeof(buf));  // COMPLIANT
+    wcstombs(buf + 1, wbuf + 1, sizeof(buf) - 1); // COMPLIANT
+    wcstombs(buf + 1, wbuf + 1, sizeof(buf));     // NON_COMPLIANT
+  }
+
+  // mbtowc
+  {
+    wchar_t c;
+    char buf[2] = {0};
+    mbtowc(&c, buf, sizeof(buf));     // COMPLIANT
+    mbtowc(&c, buf, sizeof(buf) - 1); // COMPLIANT
+    mbtowc(&c, buf, sizeof(buf) + 1); // NON_COMPLIANT
+    mbtowc(NULL, NULL, 0);            // COMPLIANT - exception
+  }
+
+  // mblen
+  {
+    char buf[3] = {0};
+    mblen(buf, sizeof(buf));                   // COMPLIANT
+    mblen(buf, sizeof(buf) + 1);               // NON_COMPLIANT
+    mblen((char *)malloc(5), sizeof(buf) * 2); // NON_COMPLIANT
+    mblen(NULL, 0);                            // COMPLIANT - exception
+  }
+
+  // memchr, memset
+  {
+    char buf[128];
+    memchr(buf, 0, sizeof(buf));     // COMPLIANT
+    memchr(buf, 0, sizeof(buf) + 1); // NON_COMPLIANT
+    memset(buf, 0, sizeof(buf) + 1); // NON_COMPLIANT
+    memchr(buf, 0, sizeof(buf) - 1); // COMPLIANT
+    memchr(NULL, 0, sizeof(buf));    // NON_COMPLIANT
+  }
+
+  // strftime
+  {
+    char buf[128];
+    strftime(buf, sizeof(buf), "%Y-%m-%d", NULL);     // COMPLIANT
+    strftime(buf, sizeof(buf) + 1, "%Y-%m-%d", NULL); // NON_COMPLIANT
+    strftime(buf, sizeof(buf) - 1, "%Y-%m-%d", NULL); // COMPLIANT
+    strftime(buf + 1, sizeof(buf), "%Y-%m-%d", NULL); // NON_COMPLIANT
+  }
+
+  // wcsftime
+  {
+    wchar_t wbuf[128] = {0};
+    wcsftime(wbuf, sizeof(wbuf) / sizeof(wchar_t), L"%Y-%m-%d",
+             NULL); // COMPLIANT
+    wcsftime(wbuf, sizeof(wbuf) / sizeof(wchar_t) + 2, L"%Y-%m-%d",
+             NULL); // NON_COMPLIANT
+    wcsftime(wbuf, sizeof(wbuf) / sizeof(wchar_t) - 2, L"%Y-%m-%d",
+             NULL); // COMPLIANT
+    wcsftime(wbuf + 1, sizeof(wbuf) / sizeof(wchar_t), L"%Y-%m-%d",
+             NULL);                                  // NON_COMPLIANT
+    wcsftime(wbuf, sizeof(wbuf), L"%Y-%m-%d", NULL); // NON_COMPLIANT
+  }
+
+  // strxfrm
+  {
+    char buf[64];
+    char buf2[128];
+    strxfrm(buf, "abc", sizeof(buf));     // COMPLIANT
+    strxfrm(buf, "abc", sizeof(buf) + 1); // NON_COMPLIANT
+    strxfrm(buf, "abc", sizeof(buf) - 1); // COMPLIANT
+    strxfrm(buf + 1, buf2,
+            sizeof(buf) - 1); // NON_COMPLIANT - not null terminated
+  }
+
+  // strncat
+  {
+    char buf[64];
+    char buf2[64];
+    strncat(buf, buf2, sizeof(buf));         // COMPLIANT
+    strncat(buf, buf2, sizeof(buf) + 1);     // NON_COMPLIANT
+    strncat(buf, buf2, sizeof(buf) - 1);     // COMPLIANT
+    strncat(buf + 1, buf2, sizeof(buf));     // NON_COMPLIANT
+    strncat(buf, buf2 + 1, sizeof(buf) * 2); // NON_COMPLIANT
+  }
+  // wcsxfrm
+  {
+    wchar_t wbuf[64];
+    wchar_t wbuf2[128];
+    wcsxfrm(wbuf, L"abc", sizeof(wbuf) / sizeof(wchar_t));     // COMPLIANT
+    wcsxfrm(wbuf, L"abc", sizeof(wbuf) / sizeof(wchar_t) + 1); // NON_COMPLIANT
+    wcsxfrm(wbuf, L"abc", sizeof(wbuf) / sizeof(wchar_t) - 1); // COMPLIANT
+    wcsxfrm(wbuf + 1, wbuf2, sizeof(wbuf) / sizeof(wchar_t) - 1); // COMPLIANT
+  }
+
+  // "memcpy", "wmemcpy", "memmove", "wmemmove", "memcmp", "wmemcmp"
+
+  // memcpy
+  {
+    char buf[64];
+    char buf2[64];
+    wchar_t wbuf[64];
+    wchar_t wbuf2[64];
+
+    memcpy(buf, buf2, sizeof(buf));         // COMPLIANT
+    memcpy(buf, buf2, sizeof(buf) + 1);     // NON_COMPLIANT
+    memcpy(buf, buf2, sizeof(buf) - 1);     // COMPLIANT
+    memcpy(buf + 1, buf2, sizeof(buf));     // NON_COMPLIANT
+    memcpy(buf, buf2 + 1, sizeof(buf) * 2); // NON_COMPLIANT
+  }
+}
+
+void test_equivalent_expressions(void *in, int x, int y, int a, int b) {
+  short *p = (short *)malloc(x * y * sizeof(short));
+  memcpy(p, in, x * y * sizeof(short));     // COMPLIANT
+  memcpy(p, in, x * y * sizeof(short) + 1); // NON_COMPLIANT
+  memcpy(p, in, x * y * sizeof(short) - 1); // COMPLIANT
+  memcpy(p, in, a * b * sizeof(short) + 1); // COMPLIANT - unknown
+}
+} // namespace ARR38_C_copied
+
+int main(int argc, char *argv[]) {
+  /* 1. Single-dimensional array initialized on the stack */
+  int stack_single_dimensional_array[3] = {0, 1, 2};
+
+  stack_allocated_single_dimensional_pointer_arithmetic(
+      stack_single_dimensional_array);
+  stack_allocated_single_dimensional_array_access(
+      stack_single_dimensional_array);
+
+  /* 2. Single-dimensional array initialized on the heap */
+  int num_of_elements_malloc;
+  int num_of_elements_calloc;
+  int num_of_elements_realloc;
+
+  if (argc) {
+    num_of_elements_malloc = 1;
+    num_of_elements_calloc = 2;
+    num_of_elements_realloc = 3;
+  } else {
+    num_of_elements_malloc = 4;
+    num_of_elements_calloc = 5;
+    num_of_elements_realloc = 6;
+  }
+
+  int *single_dimensional_array_malloc =
+      (int *)malloc(num_of_elements_malloc * sizeof(int));
+  int *single_dimensional_array_calloc =
+      (int *)calloc(num_of_elements_calloc, sizeof(int));
+
+  int *single_dimensional_array_realloc = (int *)realloc(
+      single_dimensional_array_malloc, num_of_elements_realloc * sizeof(int));
+
+  malloc_single_dimensional_pointer_arithmetic(single_dimensional_array_malloc);
+  malloc_single_dimensional_array_access(single_dimensional_array_malloc);
+
+  calloc_single_dimensional_pointer_arithmetic(single_dimensional_array_calloc);
+  calloc_single_dimensional_array_access(single_dimensional_array_calloc);
+
+  realloc_single_dimensional_pointer_arithmetic(
+      single_dimensional_array_realloc);
+  realloc_single_dimensional_array_access(single_dimensional_array_realloc);
+
+  /* 3. Multi-dimensional array initialized on the stack */
+  int stack_multi_dimensional_array[2][3] = {{1, 2, 3}, {4, 5, 6}};
+
+  /* 4. Multi-dimensional array initialized on the heap */
+  int (*heap_multi_dimensional_array)[3] =
+      (int (*)[3])malloc(sizeof(int[2][3]));
+
+  stack_allocated_multi_dimensional_array_access(stack_multi_dimensional_array);
+  stack_allocated_multi_dimensional_pointer_arithmetic(
+      stack_multi_dimensional_array);
+
+  return 0;
+}
diff --git a/rule_packages/cpp/Memory1.json b/rule_packages/cpp/Memory1.json
new file mode 100644
index 000000000..6dd049fd0
--- /dev/null
+++ b/rule_packages/cpp/Memory1.json
@@ -0,0 +1,35 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-8-7-1": {
+      "properties": {
+        "enforcement": "undecidable",
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Pointers obtained as result of performing arithmetic should point to an initialized object, or an element right next to the last element of an array.",
+          "kind": "path-problem",
+          "name": "Pointer arithmetic shall not form an invalid pointer.",
+          "precision": "high",
+          "severity": "error",
+          "short_name": "PointerArithmeticFormsAnInvalidPointer",
+          "tags": [
+            "scope/system"
+          ]
+        },
+        {
+          "description": "Pointer and index arguments passed to functions in <cstring> should result in valid reads and/or writes.",
+          "kind": "problem",
+          "name": "Pointer and index arguments passed to functions in <cstring> shall not be invalid.",
+          "precision": "high",
+          "severity": "error",
+          "short_name": "PointerArgumentToCstringFunctionIsInvalid",
+          "tags": [
+            "scope/system"
+          ]
+        }
+      ],
+      "title": "Pointers obtained as result of performing arithmetic should point to an initialized object, or an element right next to the last element of an array."
+    }
+  }
+}
diff --git a/rule_packages/cpp/Memory2.json b/rule_packages/cpp/Memory2.json
new file mode 100644
index 000000000..067af41b1
--- /dev/null
+++ b/rule_packages/cpp/Memory2.json
@@ -0,0 +1,24 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-8-7-2": {
+      "properties": {
+        "enforcement": "undecidable",
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Pointer difference should be taken from pointers that belong to a same array.",
+          "kind": "problem",
+          "name": "Subtraction between pointers shall only be applied to ones that address elements of the same array.",
+          "precision": "very-high",
+          "severity": "error",
+          "short_name": "PointerDifferenceTakenBetweenDifferentArrays",
+          "tags": [
+            "scope/system"
+          ]
+        }
+      ],
+      "title": "Pointer difference should be taken from pointers that belong to a same array."
+    }
+  }
+}
diff --git a/rule_packages/cpp/Memory3.json b/rule_packages/cpp/Memory3.json
new file mode 100644
index 000000000..1117c552b
--- /dev/null
+++ b/rule_packages/cpp/Memory3.json
@@ -0,0 +1,24 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-8-9-1": {
+      "properties": {
+        "enforcement": "undecidable",
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Pointer comparison should be done between ones that belong to a same array.",
+          "kind": "problem",
+          "name": "The built-in relational operators >, >=, < and <= shall not be applied to objects of pointer type.",
+          "precision": "very-high",
+          "severity": "error",
+          "short_name": "PointerComparedBetweenDifferentArrays",
+          "tags": [
+            "scope/system"
+          ]
+        }
+      ],
+      "title": "Pointer comparison should be done between ones that belong to a same array."
+    }
+  }
+}
diff --git a/rule_packages/cpp/Memory4.json b/rule_packages/cpp/Memory4.json
new file mode 100644
index 000000000..f2fa1803c
--- /dev/null
+++ b/rule_packages/cpp/Memory4.json
@@ -0,0 +1,24 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-8-18-1": {
+      "properties": {
+        "enforcement": "undecidable",
+        "obligation": "mandatory"
+      },
+      "queries": [
+        {
+          "description": "Copying a member of a union to another, and copying a slice of an array to an overlapping one causes undefined behavior.",
+          "kind": "problem",
+          "name": "An object or subobject must not be copied to an overlapping object.",
+          "precision": "high",
+          "severity": "error",
+          "short_name": "ObjectMustNotBeCopiedToAnOverlappingObject",
+          "tags": [
+            "scope/system"
+          ]
+        }
+      ],
+      "title": "Copying a member of a union to another, and copying a slice of an array to an overlapping one causes undefined behavior."
+    }
+  }
+}
diff --git a/rule_packages/cpp/Memory5.json b/rule_packages/cpp/Memory5.json
new file mode 100644
index 000000000..40a5ea765
--- /dev/null
+++ b/rule_packages/cpp/Memory5.json
@@ -0,0 +1,24 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-21-6-2": {
+      "properties": {
+        "enforcement": "decidable",
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Dynamically allocated memory must not be managed manually.",
+          "kind": "problem",
+          "name": "Dynamic memory shall be managed automatically.",
+          "precision": "very-high",
+          "severity": "error",
+          "short_name": "DynamicMemoryManagedManually",
+          "tags": [
+            "scope/single-translation-unit"
+          ]
+        }
+      ],
+      "title": "Dynamically allocated memory must not be managed manually."
+    }
+  }
+}
diff --git a/rule_packages/cpp/Memory6.json b/rule_packages/cpp/Memory6.json
new file mode 100644
index 000000000..14a935afb
--- /dev/null
+++ b/rule_packages/cpp/Memory6.json
@@ -0,0 +1,24 @@
+{
+  "MISRA-C++-2023": {
+    "RULE-21-6-3": {
+      "properties": {
+        "enforcement": "decidable",
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Using advanced memory management that either alters allocation and deallocation or constructs object construction on uninitalized memory may result in undefined behavior.",
+          "kind": "problem",
+          "name": "Advanced memory management shall not be used.",
+          "precision": "very-high",
+          "severity": "error",
+          "short_name": "AdvancedMemoryManagementUsed",
+          "tags": [
+            "scope/single-translation-unit"
+          ]
+        }
+      ],
+      "title": "Using advanced memory management that either alters allocation and deallocation or constructs object construction on uninitalized memory may result in undefined behavior."
+    }
+  }
+}
diff --git a/rules.csv b/rules.csv
index a2eb7eddd..1a2112b45 100644
--- a/rules.csv
+++ b/rules.csv
@@ -895,11 +895,11 @@ cpp,MISRA-C++-2023,RULE-8-2-10,Yes,Required,Undecidable,System,"Functions shall
 cpp,MISRA-C++-2023,RULE-8-2-11,Yes,Required,Decidable,Single Translation Unit,An argument passed via ellipsis shall have an appropriate type,,Preconditions,Easy,
 cpp,MISRA-C++-2023,RULE-8-3-1,Yes,Advisory,Decidable,Single Translation Unit,The built-in unary - operator should not be applied to an expression of unsigned type,M5-3-2,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-8-3-2,Yes,Advisory,Decidable,Single Translation Unit,The built-in unary + operator should not be used,,Banned,Easy,
-cpp,MISRA-C++-2023,RULE-8-7-1,Yes,Required,Undecidable,System,Pointer arithmetic shall not form an invalid pointer,ARR30-C,Memory,Easy,
-cpp,MISRA-C++-2023,RULE-8-7-2,Yes,Required,Undecidable,System,Subtraction between pointers shall only be applied to pointers that address elements of the same array,ARR36-C,Memory,Easy,
-cpp,MISRA-C++-2023,RULE-8-9-1,Yes,Required,Undecidable,System,"The built-in relational operators >, >=, < and <= shall not be applied to objects of pointer type, except where they point to elements of the same array",ARR36-C,Memory,Easy,
+cpp,MISRA-C++-2023,RULE-8-7-1,Yes,Required,Undecidable,System,Pointer arithmetic shall not form an invalid pointer,ARR30-C,Memory1,Easy,
+cpp,MISRA-C++-2023,RULE-8-7-2,Yes,Required,Undecidable,System,Subtraction between pointers shall only be applied to pointers that address elements of the same array,ARR36-C,Memory2,Easy,
+cpp,MISRA-C++-2023,RULE-8-9-1,Yes,Required,Undecidable,System,"The built-in relational operators >, >=, < and <= shall not be applied to objects of pointer type, except where they point to elements of the same array",ARR36-C,Memory3,Easy,
 cpp,MISRA-C++-2023,RULE-8-14-1,Yes,Advisory,Undecidable,System,The right-hand operand of a logical && or operator should not contain persistent side effects,"M5-14-1, RULE-13-5",SideEffects3,Medium,
-cpp,MISRA-C++-2023,RULE-8-18-1,Yes,Mandatory,Undecidable,System,An object or subobject must not be copied to an overlapping object,"M0-2-1, RULE-19-1",Memory,Hard,
+cpp,MISRA-C++-2023,RULE-8-18-1,Yes,Mandatory,Undecidable,System,An object or subobject must not be copied to an overlapping object,"M0-2-1, RULE-19-1",Memory4,Hard,
 cpp,MISRA-C++-2023,RULE-8-18-2,Yes,Advisory,Decidable,Single Translation Unit,The result of an assignment operator should not be used,RULE-13-4,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-8-19-1,Yes,Advisory,Decidable,Single Translation Unit,The comma operator should not be used,M5-18-1,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-8-20-1,Yes,Advisory,Decidable,Single Translation Unit,An unsigned arithmetic operation with constant operands should not wrap,INT30-C,ImportMisra23,Import,
@@ -979,8 +979,8 @@ cpp,MISRA-C++-2023,RULE-21-2-2,Yes,Required,Decidable,Single Translation Unit,"T
 cpp,MISRA-C++-2023,RULE-21-2-3,Yes,Required,Decidable,Single Translation Unit,The library function system from <cstdlib> shall not be used,M18-0-3,BannedAPIs,Easy,
 cpp,MISRA-C++-2023,RULE-21-2-4,Yes,Required,Decidable,Single Translation Unit,The macro offsetof shall not be used,M18-2-1,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-21-6-1,Yes,Advisory,Undecidable,Single Translation Unit,Dynamic memory should not be used,DIR-4-12,Banned,Easy,
-cpp,MISRA-C++-2023,RULE-21-6-2,Yes,Required,Decidable,Single Translation Unit,Dynamic memory shall be managed automatically,,Memory,Easy,
-cpp,MISRA-C++-2023,RULE-21-6-3,Yes,Required,Decidable,Single Translation Unit,Advanced memory management shall not be used,,Memory,Medium,
+cpp,MISRA-C++-2023,RULE-21-6-2,Yes,Required,Decidable,Single Translation Unit,Dynamic memory shall be managed automatically,,Memory5,Easy,
+cpp,MISRA-C++-2023,RULE-21-6-3,Yes,Required,Decidable,Single Translation Unit,Advanced memory management shall not be used,,Memory6,Medium,
 cpp,MISRA-C++-2023,RULE-21-6-4,Yes,Required,Decidable,System,"If a project defines either a sized or unsized version of a global operator delete, then both shall be defined",A18-5-4,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-21-6-5,Yes,Required,Decidable,Single Translation Unit,A pointer to an incomplete class type shall not be deleted,A5-3-3,ImportMisra23,Import,
 cpp,MISRA-C++-2023,RULE-21-10-1,Yes,Required,Decidable,Single Translation Unit,The features of <cstdarg> shall not be used,DCL50-CPP,BannedAPIs,Easy,