diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
index 30fdf102b6b..6d17e85863f 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
@@ -897,23 +897,6 @@ private class MyConsistencyConfiguration extends Consistency::ConsistencyConfigu
   }
 }
 
-/**
- * Gets the basic block of `node`.
- */
-IRBlock getBasicBlock(Node node) {
-  node.asInstruction().getBlock() = result
-  or
-  node.asOperand().getUse().getBlock() = result
-  or
-  node.(SsaPhiNode).getPhiNode().getBasicBlock() = result
-  or
-  node.(RawIndirectOperand).getOperand().getUse().getBlock() = result
-  or
-  node.(RawIndirectInstruction).getInstruction().getBlock() = result
-  or
-  result = getBasicBlock(node.(PostUpdateNode).getPreUpdateNode())
-}
-
 /**
  * A local flow relation that includes both local steps, read steps and
  * argument-to-return flow through summarized functions.
@@ -999,7 +982,8 @@ private int countNumberOfBranchesUsingParameter(SwitchInstruction switch, Parame
     // we pick the one with the highest edge count.
     result =
       max(SsaPhiNode phi |
-        switch.getSuccessor(caseOrDefaultEdge()).getBlock().dominanceFrontier() = getBasicBlock(phi) and
+        switch.getSuccessor(caseOrDefaultEdge()).getBlock().dominanceFrontier() =
+          phi.getBasicBlock() and
         phi.getSourceVariable() = sv
       |
         strictcount(phi.getAnInput())
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
index 714e5bd3b49..8a3568497cc 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll
@@ -160,6 +160,28 @@ class Node extends TIRDataFlowNode {
   /** Gets the operands corresponding to this node, if any. */
   Operand asOperand() { result = this.(OperandNode).getOperand() }
 
+  /**
+   * Holds if this node is at index `i` in basic block `block`.
+   *
+   * Note: Phi nodes are considered to be at index `-1`.
+   */
+  final predicate hasIndexInBlock(IRBlock block, int i) {
+    this.asInstruction() = block.getInstruction(i)
+    or
+    this.asOperand().getUse() = block.getInstruction(i)
+    or
+    this.(SsaPhiNode).getPhiNode().getBasicBlock() = block and i = -1
+    or
+    this.(RawIndirectOperand).getOperand().getUse() = block.getInstruction(i)
+    or
+    this.(RawIndirectInstruction).getInstruction() = block.getInstruction(i)
+    or
+    this.(PostUpdateNode).getPreUpdateNode().hasIndexInBlock(block, i)
+  }
+
+  /** Gets the basic block of this node, if any. */
+  final IRBlock getBasicBlock() { this.hasIndexInBlock(result, _) }
+
   /**
    * Gets the non-conversion expression corresponding to this node, if any.
    * This predicate only has a result on nodes that represent the value of
@@ -530,7 +552,7 @@ class SsaPhiNode extends Node, TSsaPhiNode {
    */
   final Node getAnInput(boolean fromBackEdge) {
     localFlowStep(result, this) and
-    if phi.getBasicBlock().dominates(getBasicBlock(result))
+    if phi.getBasicBlock().dominates(result.getBasicBlock())
     then fromBackEdge = true
     else fromBackEdge = false
   }
@@ -1887,7 +1909,7 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
       e = value.getAnInstruction().getConvertedResultExpression() and
       result.getConvertedExpr() = e and
       guardChecks(g, value.getAnInstruction().getConvertedResultExpression(), edge) and
-      g.controls(getBasicBlock(result), edge)
+      g.controls(result.getBasicBlock(), edge)
     )
   }
 }
diff --git a/cpp/ql/src/Critical/DoubleFree.cpp b/cpp/ql/src/Critical/DoubleFree.cpp
new file mode 100644
index 00000000000..92b12ea5bcb
--- /dev/null
+++ b/cpp/ql/src/Critical/DoubleFree.cpp
@@ -0,0 +1,10 @@
+int* f() {
+	int *buff = malloc(SIZE*sizeof(int));
+	do_stuff(buff);
+	free(buff);
+	int *new_buffer = malloc(SIZE*sizeof(int));
+	free(buff); // BAD: If new_buffer is assigned the same address as buff,
+              // the memory allocator will free the new buffer memory region,
+              // leading to use-after-free problems and memory corruption.
+	return new_buffer;
+}
diff --git a/cpp/ql/src/Critical/DoubleFree.qhelp b/cpp/ql/src/Critical/DoubleFree.qhelp
new file mode 100644
index 00000000000..0b38858eae4
--- /dev/null
+++ b/cpp/ql/src/Critical/DoubleFree.qhelp
@@ -0,0 +1,33 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+
+
+<overview>
+<p>
+Deallocating memory more than once can lead to a double-free vulnerability. This can be exploited to
+corrupt the allocator's internal data structures, which can lead to denial-of-service attacks by crashing
+the program, or security vulnerabilities, by allowing an attacker to overwrite arbitrary memory locations.
+</p>
+
+</overview>
+<recommendation>
+<p>
+Ensure that all execution paths deallocate the allocated memory at most once. If possible, reassign
+the pointer to a null value after deallocating it. This will prevent double-free vulnerabilities since
+most deallocation functions will perform a null-pointer check before attempting to deallocate the memory.
+</p>
+
+</recommendation>
+<example><sample src="DoubleFree.cpp" />
+</example>
+<references>
+
+<li>
+OWASP:
+<a href="https://owasp.org/www-community/vulnerabilities/Doubly_freeing_memory">Doubly freeing memory</a>.
+</li>
+
+</references>
+</qhelp>
diff --git a/cpp/ql/src/Critical/DoubleFree.ql b/cpp/ql/src/Critical/DoubleFree.ql
new file mode 100644
index 00000000000..734e32ea75f
--- /dev/null
+++ b/cpp/ql/src/Critical/DoubleFree.ql
@@ -0,0 +1,49 @@
+/**
+ * @name Potential double free
+ * @description Freeing a resource more than once can lead to undefined behavior and cause memory corruption.
+ * @kind path-problem
+ * @precision medium
+ * @id cpp/double-free
+ * @problem.severity warning
+ * @security-severity 9.3
+ * @tags reliability
+ *       security
+ *       external/cwe/cwe-415
+ */
+
+import cpp
+import semmle.code.cpp.dataflow.new.DataFlow
+import FlowAfterFree
+import DoubleFree::PathGraph
+
+predicate isFree(DataFlow::Node n, Expr e) { isFree(n, e, _) }
+
+/**
+ * `dealloc1` is a deallocation expression and `e` is an expression such
+ * that is deallocated by a deallocation expression, and the `(dealloc1, e)` pair
+ * should be excluded by the `FlowFromFree` library.
+ *
+ * Note that `e` is not necessarily the expression deallocated by `dealloc1`. It will
+ * be bound to the second deallocation as identified by the `FlowFromFree` library.
+ */
+bindingset[dealloc1, e]
+predicate isExcludeFreePair(DeallocationExpr dealloc1, Expr e) {
+  exists(DeallocationExpr dealloc2 | isFree(_, e, dealloc2) |
+    dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and
+    // From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl:
+    // "After calling MmFreePagesFromMdl, the caller must also call ExFreePool
+    // to release the memory that was allocated for the MDL structure."
+    isExFreePoolCall(dealloc2, _)
+  )
+}
+
+module DoubleFree = FlowFromFree<isFree/2, isExcludeFreePair/2>;
+
+from DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2
+where
+  DoubleFree::flowPath(source, sink) and
+  isFree(source.getNode(), _, dealloc) and
+  isFree(sink.getNode(), e2)
+select sink.getNode(), source, sink,
+  "Memory pointed to by '" + e2.toString() + "' may already have been freed by $@.", dealloc,
+  dealloc.toString()
diff --git a/cpp/ql/src/Critical/FlowAfterFree.qll b/cpp/ql/src/Critical/FlowAfterFree.qll
new file mode 100644
index 00000000000..0e04b294d70
--- /dev/null
+++ b/cpp/ql/src/Critical/FlowAfterFree.qll
@@ -0,0 +1,129 @@
+import cpp
+import semmle.code.cpp.dataflow.new.DataFlow
+private import semmle.code.cpp.ir.IR
+
+/**
+ * Signature for a predicate that holds if `n.asExpr() = e` and `n` is a sink in
+ * the `FlowFromFreeConfig` module.
+ */
+private signature predicate isSinkSig(DataFlow::Node n, Expr e);
+
+/**
+ * Holds if `dealloc` is a deallocation expression and `e` is an expression such
+ * that `isFree(_, e)` holds for some `isFree` predicate satisfying `isSinkSig`,
+ * and this source-sink pair should be excluded from the analysis.
+ */
+bindingset[dealloc, e]
+private signature predicate isExcludedSig(DeallocationExpr dealloc, Expr e);
+
+/**
+ * Holds if `(b1, i1)` strictly post-dominates `(b2, i2)`
+ */
+bindingset[i1, i2]
+predicate strictlyPostDominates(IRBlock b1, int i1, IRBlock b2, int i2) {
+  b1 = b2 and
+  i1 > i2
+  or
+  b1.strictlyPostDominates(b2)
+}
+
+/**
+ * Holds if `(b1, i1)` strictly dominates `(b2, i2)`
+ */
+bindingset[i1, i2]
+predicate strictlyDominates(IRBlock b1, int i1, IRBlock b2, int i2) {
+  b1 = b2 and
+  i1 < i2
+  or
+  b1.strictlyDominates(b2)
+}
+
+/**
+ * Constructs a `FlowFromFreeConfig` module that can be used to find flow between
+ * a pointer being freed by some deallocation function, and a user-specified sink.
+ *
+ * In order to reduce false positives, the set of sinks is restricted to only those
+ * that satisfy at least one of the following two criteria:
+ * 1. The source dominates the sink, or
+ * 2. The sink post-dominates the source.
+ */
+module FlowFromFree<isSinkSig/2 isASink, isExcludedSig/2 isExcluded> {
+  module FlowFromFreeConfig implements DataFlow::StateConfigSig {
+    class FlowState instanceof Expr {
+      FlowState() { isFree(_, this, _) }
+
+      string toString() { result = super.toString() }
+    }
+
+    predicate isSource(DataFlow::Node node, FlowState state) { isFree(node, state, _) }
+
+    pragma[inline]
+    predicate isSink(DataFlow::Node sink, FlowState state) {
+      exists(
+        Expr e, DataFlow::Node source, IRBlock b1, int i1, IRBlock b2, int i2,
+        DeallocationExpr dealloc
+      |
+        isASink(sink, e) and
+        isFree(source, state, dealloc) and
+        e != state and
+        source.hasIndexInBlock(b1, i1) and
+        sink.hasIndexInBlock(b2, i2) and
+        not isExcluded(dealloc, e)
+      |
+        strictlyDominates(b1, i1, b2, i2)
+        or
+        strictlyPostDominates(b2, i2, b1, i1)
+      )
+    }
+
+    predicate isBarrierIn(DataFlow::Node n) {
+      n.asIndirectExpr() = any(AddressOfExpr aoe)
+      or
+      n.asIndirectExpr() = any(Call call).getAnArgument()
+      or
+      exists(Expr e |
+        n.asIndirectExpr() = e.(PointerDereferenceExpr).getOperand() or
+        n.asIndirectExpr() = e.(ArrayExpr).getArrayBase()
+      |
+        e = any(StoreInstruction store).getDestinationAddress().getUnconvertedResultExpression()
+      )
+    }
+
+    predicate isBarrier(DataFlow::Node n, FlowState state) { none() }
+
+    predicate isAdditionalFlowStep(
+      DataFlow::Node n1, FlowState state1, DataFlow::Node n2, FlowState state2
+    ) {
+      none()
+    }
+  }
+
+  import DataFlow::GlobalWithState<FlowFromFreeConfig>
+}
+
+/**
+ * Holds if `n` is a dataflow node such that `n.asExpr() = e` and `e`
+ * is being freed by a deallocation expression `dealloc`.
+ */
+predicate isFree(DataFlow::Node n, Expr e, DeallocationExpr dealloc) {
+  e = dealloc.getFreedExpr() and
+  e = n.asExpr() and
+  // Ignore realloc functions
+  not exists(dealloc.(FunctionCall).getTarget().(AllocationFunction).getReallocPtrArg())
+}
+
+/**
+ * Holds if `fc` is a function call that is the result of expanding
+ * the `ExFreePool` macro.
+ */
+predicate isExFreePoolCall(FunctionCall fc, Expr e) {
+  e = fc.getArgument(0) and
+  (
+    exists(MacroInvocation mi |
+      mi.getMacroName() = "ExFreePool" and
+      mi.getExpr() = fc
+    )
+    or
+    fc.getTarget().hasGlobalName("ExFreePool")
+  )
+}
diff --git a/cpp/ql/src/Critical/UseAfterFree.ql b/cpp/ql/src/Critical/UseAfterFree.ql
index 3c67c99ef3c..3356bb7623b 100644
--- a/cpp/ql/src/Critical/UseAfterFree.ql
+++ b/cpp/ql/src/Critical/UseAfterFree.ql
@@ -1,7 +1,8 @@
 /**
  * @name Potential use after free
  * @description An allocated memory block is used after it has been freed. Behavior in such cases is undefined and can cause memory corruption.
- * @kind problem
+ * @kind path-problem
+ * @precision medium
  * @id cpp/use-after-free
  * @problem.severity warning
  * @security-severity 9.3
@@ -11,56 +12,158 @@
  */
 
 import cpp
-import semmle.code.cpp.controlflow.StackVariableReachability
+import semmle.code.cpp.dataflow.new.DataFlow
+import semmle.code.cpp.ir.IR
+import FlowAfterFree
+import UseAfterFree::PathGraph
 
-/** `e` is an expression that frees the memory pointed to by `v`. */
-predicate isFreeExpr(Expr e, StackVariable v) {
-  exists(VariableAccess va | va.getTarget() = v |
-    exists(FunctionCall fc | fc = e |
-      fc.getTarget().hasGlobalOrStdName("free") and
-      va = fc.getArgument(0)
-    )
-    or
-    e.(DeleteExpr).getExpr() = va
-    or
-    e.(DeleteArrayExpr).getExpr() = va
+/**
+ * Holds if `call` is a call to a function that obviously
+ * doesn't dereference its `i`'th argument.
+ */
+private predicate externalCallNeverDereferences(FormattingFunctionCall call, int arg) {
+  exists(int formatArg |
+    pragma[only_bind_out](call.getFormatArgument(formatArg)) =
+      pragma[only_bind_out](call.getArgument(arg)) and
+    call.getFormat().(FormatLiteral).getConvSpec(formatArg) != "%s"
   )
 }
 
-/** `e` is an expression that (may) dereference `v`. */
-predicate isDerefExpr(Expr e, StackVariable v) {
-  v.getAnAccess() = e and dereferenced(e)
-  or
-  isDerefByCallExpr(_, _, e, v)
+predicate isUse0(DataFlow::Node n, Expr e) {
+  e = n.asExpr() and
+  not isFree(_, e, _) and
+  (
+    e = any(PointerDereferenceExpr pde).getOperand()
+    or
+    e = any(PointerFieldAccess pfa).getQualifier()
+    or
+    e = any(ArrayExpr ae).getArrayBase()
+    or
+    e = any(Call call).getQualifier()
+    or
+    // Assume any function without a body will dereference the pointer
+    exists(int i, Call call, Function f |
+      n.asExpr() = call.getArgument(i) and
+      f = call.getTarget() and
+      not f.hasEntryPoint() and
+      // Exclude known functions we know won't dereference the pointer.
+      // For example, a call such as `printf("%p", myPointer)`.
+      not externalCallNeverDereferences(call, i)
+    )
+  )
 }
 
-/**
- * `va` is passed by value as (part of) the `i`th argument in
- * call `c`. The target function is either a library function
- * or a source code function that dereferences the relevant
- * parameter.
- */
-predicate isDerefByCallExpr(Call c, int i, VariableAccess va, StackVariable v) {
-  v.getAnAccess() = va and
-  va = c.getAnArgumentSubExpr(i) and
-  not c.passesByReference(i, va) and
-  (c.getTarget().hasEntryPoint() implies isDerefExpr(_, c.getTarget().getParameter(i)))
-}
+module ParameterSinks {
+  import semmle.code.cpp.ir.ValueNumbering
 
-class UseAfterFreeReachability extends StackVariableReachability {
-  UseAfterFreeReachability() { this = "UseAfterFree" }
+  predicate flowsToUse(DataFlow::Node n) {
+    isUse0(n, _)
+    or
+    exists(DataFlow::Node succ |
+      flowsToUse(succ) and
+      DataFlow::localFlowStep(n, succ)
+    )
+  }
 
-  override predicate isSource(ControlFlowNode node, StackVariable v) { isFreeExpr(node, v) }
+  private predicate flowsFromParam(DataFlow::Node n) {
+    flowsToUse(n) and
+    (
+      n.asParameter().getUnspecifiedType() instanceof PointerType
+      or
+      exists(DataFlow::Node prev |
+        flowsFromParam(prev) and
+        DataFlow::localFlowStep(prev, n)
+      )
+    )
+  }
 
-  override predicate isSink(ControlFlowNode node, StackVariable v) { isDerefExpr(node, v) }
+  private predicate step(DataFlow::Node n1, DataFlow::Node n2) {
+    flowsFromParam(n1) and
+    flowsFromParam(n2) and
+    DataFlow::localFlowStep(n1, n2)
+  }
 
-  override predicate isBarrier(ControlFlowNode node, StackVariable v) {
-    definitionBarrier(v, node) or
-    isFreeExpr(node, v)
+  private predicate paramToUse(DataFlow::Node n1, DataFlow::Node n2) = fastTC(step/2)(n1, n2)
+
+  private predicate hasFlow(
+    DataFlow::Node source, InitializeParameterInstruction init, DataFlow::Node sink
+  ) {
+    pragma[only_bind_out](source.asParameter()) = pragma[only_bind_out](init.getParameter()) and
+    paramToUse(source, sink) and
+    isUse0(sink, _)
+  }
+
+  private InitializeParameterInstruction getAnAlwaysDereferencedParameter0() {
+    exists(DataFlow::Node source, DataFlow::Node sink, IRBlock b1, int i1, IRBlock b2, int i2 |
+      hasFlow(pragma[only_bind_into](source), result, pragma[only_bind_into](sink)) and
+      source.hasIndexInBlock(b1, pragma[only_bind_into](i1)) and
+      sink.hasIndexInBlock(b2, pragma[only_bind_into](i2)) and
+      strictlyPostDominates(b2, i2, b1, i1)
+    )
+  }
+
+  private CallInstruction getAnAlwaysReachedCallInstruction(IRFunction f) {
+    result.getBlock().postDominates(f.getEntryBlock())
+  }
+
+  pragma[nomagic]
+  predicate callHasTargetAndArgument(Function f, int i, CallInstruction call, Instruction argument) {
+    call.getStaticCallTarget() = f and
+    call.getArgument(i) = argument
+  }
+
+  pragma[nomagic]
+  predicate initializeParameterInFunction(Function f, int i, InitializeParameterInstruction init) {
+    pragma[only_bind_out](init.getEnclosingFunction()) = f and
+    init.hasIndex(i)
+  }
+
+  InitializeParameterInstruction getAnAlwaysDereferencedParameter() {
+    result = getAnAlwaysDereferencedParameter0()
+    or
+    exists(
+      CallInstruction call, int i, InitializeParameterInstruction p, Instruction argument,
+      Function f
+    |
+      callHasTargetAndArgument(f, i, call, argument) and
+      initializeParameterInFunction(f, i, p) and
+      p = getAnAlwaysDereferencedParameter() and
+      result = pragma[only_bind_out](valueNumber(argument).getAnInstruction()) and
+      call = getAnAlwaysReachedCallInstruction(_)
+    )
   }
 }
 
-from UseAfterFreeReachability r, StackVariable v, Expr free, Expr e
-where r.reaches(free, v, e)
-select e, "Memory pointed to by '" + v.getName().toString() + "' may have $@.", free,
-  "been previously freed"
+predicate isUse(DataFlow::Node n, Expr e) {
+  isUse0(n, e)
+  or
+  exists(CallInstruction call, int i, InitializeParameterInstruction init |
+    n.asOperand().getDef().getUnconvertedResultExpression() = e and
+    init = ParameterSinks::getAnAlwaysDereferencedParameter() and
+    call.getArgumentOperand(i) = n.asOperand() and
+    init.hasIndex(i) and
+    init.getEnclosingFunction() = call.getStaticCallTarget()
+  )
+}
+
+/**
+ * `dealloc1` is a deallocation expression, `e` is an expression that dereferences a
+ * pointer, and the `(dealloc1, e)` pair should be excluded by the `FlowFromFree` library.
+ */
+bindingset[dealloc1, e]
+predicate isExcludeFreeUsePair(DeallocationExpr dealloc1, Expr e) {
+  // From https://learn.microsoft.com/en-us/windows-hardware/drivers/ddi/wdm/nf-wdm-mmfreepagesfrommdl:
+  // "After calling MmFreePagesFromMdl, the caller must also call ExFreePool
+  // to release the memory that was allocated for the MDL structure."
+  dealloc1.(FunctionCall).getTarget().hasGlobalName("MmFreePagesFromMdl") and
+  isExFreePoolCall(_, e)
+}
+
+module UseAfterFree = FlowFromFree<isUse/2, isExcludeFreeUsePair/2>;
+
+from UseAfterFree::PathNode source, UseAfterFree::PathNode sink, DeallocationExpr dealloc
+where
+  UseAfterFree::flowPath(source, sink) and
+  isFree(source.getNode(), _, dealloc)
+select sink.getNode(), source, sink, "Memory may have been previously freed by $@.", dealloc,
+  dealloc.toString()
diff --git a/cpp/ql/src/change-notes/2023-04-11-double-free.md b/cpp/ql/src/change-notes/2023-04-11-double-free.md
new file mode 100644
index 00000000000..cc04177fe2d
--- /dev/null
+++ b/cpp/ql/src/change-notes/2023-04-11-double-free.md
@@ -0,0 +1,4 @@
+---
+category: newQuery
+---
+* A new query `cpp/double-free` has been added. The query finds possible cases of deallocating the same pointer twice. The precision of the query has been set to "medium".
\ No newline at end of file
diff --git a/cpp/ql/src/change-notes/2023-04-11-use-after-free.md b/cpp/ql/src/change-notes/2023-04-11-use-after-free.md
new file mode 100644
index 00000000000..8331705123e
--- /dev/null
+++ b/cpp/ql/src/change-notes/2023-04-11-use-after-free.md
@@ -0,0 +1,4 @@
+---
+category: newQuery
+---
+* The query `cpp/use-after-free` has been modernized and assigned the precision "medium". The query finds cases of where a pointer is dereferenced after its memory has been deallocated.
\ No newline at end of file
diff --git a/cpp/ql/src/experimental/Security/CWE/CWE-415/DoubleFree.ql b/cpp/ql/src/experimental/Security/CWE/CWE-415/DoubleFree.ql
index 9b9684f12e2..09e44c13fc7 100644
--- a/cpp/ql/src/experimental/Security/CWE/CWE-415/DoubleFree.ql
+++ b/cpp/ql/src/experimental/Security/CWE/CWE-415/DoubleFree.ql
@@ -2,7 +2,7 @@
  * @name Errors When Double Free
  * @description Freeing a previously allocated resource twice can lead to various vulnerabilities in the program.
  * @kind problem
- * @id cpp/double-free
+ * @id cpp/experimental-double-free
  * @problem.severity warning
  * @precision medium
  * @tags security
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.expected b/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.expected
new file mode 100644
index 00000000000..bfc99021d27
--- /dev/null
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.expected
@@ -0,0 +1,96 @@
+edges
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a |
+| test_free.cpp:30:10:30:10 | a | test_free.cpp:31:27:31:27 | a |
+| test_free.cpp:35:10:35:10 | a | test_free.cpp:37:27:37:27 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:50:27:50:27 | a | test_free.cpp:51:10:51:10 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a |
+| test_free.cpp:101:10:101:10 | a | test_free.cpp:103:10:103:10 | a |
+| test_free.cpp:128:10:128:11 | * ... | test_free.cpp:129:10:129:11 | * ... |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a |
+| test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a |
+| test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a |
+| test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a |
+| test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a |
+nodes
+| test_free.cpp:11:10:11:10 | a | semmle.label | a |
+| test_free.cpp:11:10:11:10 | a | semmle.label | a |
+| test_free.cpp:14:10:14:10 | a | semmle.label | a |
+| test_free.cpp:14:10:14:10 | a | semmle.label | a |
+| test_free.cpp:30:10:30:10 | a | semmle.label | a |
+| test_free.cpp:31:27:31:27 | a | semmle.label | a |
+| test_free.cpp:35:10:35:10 | a | semmle.label | a |
+| test_free.cpp:37:27:37:27 | a | semmle.label | a |
+| test_free.cpp:42:27:42:27 | a | semmle.label | a |
+| test_free.cpp:42:27:42:27 | a | semmle.label | a |
+| test_free.cpp:44:27:44:27 | a | semmle.label | a |
+| test_free.cpp:44:27:44:27 | a | semmle.label | a |
+| test_free.cpp:46:10:46:10 | a | semmle.label | a |
+| test_free.cpp:46:10:46:10 | a | semmle.label | a |
+| test_free.cpp:46:10:46:10 | a | semmle.label | a |
+| test_free.cpp:46:10:46:10 | a | semmle.label | a |
+| test_free.cpp:50:27:50:27 | a | semmle.label | a |
+| test_free.cpp:51:10:51:10 | a | semmle.label | a |
+| test_free.cpp:69:10:69:10 | a | semmle.label | a |
+| test_free.cpp:69:10:69:10 | a | semmle.label | a |
+| test_free.cpp:72:14:72:14 | a | semmle.label | a |
+| test_free.cpp:72:14:72:14 | a | semmle.label | a |
+| test_free.cpp:101:10:101:10 | a | semmle.label | a |
+| test_free.cpp:103:10:103:10 | a | semmle.label | a |
+| test_free.cpp:128:10:128:11 | * ... | semmle.label | * ... |
+| test_free.cpp:129:10:129:11 | * ... | semmle.label | * ... |
+| test_free.cpp:152:27:152:27 | a | semmle.label | a |
+| test_free.cpp:152:27:152:27 | a | semmle.label | a |
+| test_free.cpp:154:10:154:10 | a | semmle.label | a |
+| test_free.cpp:154:10:154:10 | a | semmle.label | a |
+| test_free.cpp:207:10:207:10 | a | semmle.label | a |
+| test_free.cpp:207:10:207:10 | a | semmle.label | a |
+| test_free.cpp:209:10:209:10 | a | semmle.label | a |
+| test_free.cpp:209:10:209:10 | a | semmle.label | a |
+subpaths
+#select
+| test_free.cpp:14:10:14:10 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:14:10:14:10 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:14:10:14:10 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:14:10:14:10 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:14:10:14:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:31:27:31:27 | a | test_free.cpp:30:10:30:10 | a | test_free.cpp:31:27:31:27 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:30:5:30:8 | call to free | call to free |
+| test_free.cpp:37:27:37:27 | a | test_free.cpp:35:10:35:10 | a | test_free.cpp:37:27:37:27 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:35:5:35:8 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:46:10:46:10 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:46:10:46:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:51:10:51:10 | a | test_free.cpp:50:27:50:27 | a | test_free.cpp:51:10:51:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:50:22:50:25 | call to free | call to free |
+| test_free.cpp:72:14:72:14 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:72:14:72:14 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:72:14:72:14 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:72:14:72:14 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:72:14:72:14 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:103:10:103:10 | a | test_free.cpp:101:10:101:10 | a | test_free.cpp:103:10:103:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:101:5:101:8 | call to free | call to free |
+| test_free.cpp:129:10:129:11 | * ... | test_free.cpp:128:10:128:11 | * ... | test_free.cpp:129:10:129:11 | * ... | Memory pointed to by '* ...' may already have been freed by $@. | test_free.cpp:128:5:128:8 | call to free | call to free |
+| test_free.cpp:154:10:154:10 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
+| test_free.cpp:154:10:154:10 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
+| test_free.cpp:154:10:154:10 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
+| test_free.cpp:154:10:154:10 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:154:10:154:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
+| test_free.cpp:209:10:209:10 | a | test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:207:5:207:8 | call to free | call to free |
+| test_free.cpp:209:10:209:10 | a | test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:207:5:207:8 | call to free | call to free |
+| test_free.cpp:209:10:209:10 | a | test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:207:5:207:8 | call to free | call to free |
+| test_free.cpp:209:10:209:10 | a | test_free.cpp:207:10:207:10 | a | test_free.cpp:209:10:209:10 | a | Memory pointed to by 'a' may already have been freed by $@. | test_free.cpp:207:5:207:8 | call to free | call to free |
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.qlref b/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.qlref
new file mode 100644
index 00000000000..8e68f14ce22
--- /dev/null
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/DoubleFree.qlref
@@ -0,0 +1 @@
+Critical/DoubleFree.ql
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryFreed.expected b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryFreed.expected
index 0fcfcc8a438..0f3eba134b2 100644
--- a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryFreed.expected
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryFreed.expected
@@ -26,6 +26,69 @@
 | test.cpp:128:15:128:16 | v4 |
 | test.cpp:185:10:185:12 | cpy |
 | test.cpp:199:10:199:12 | cpy |
+| test_free.cpp:11:10:11:10 | a |
+| test_free.cpp:14:10:14:10 | a |
+| test_free.cpp:16:10:16:10 | a |
+| test_free.cpp:18:18:18:18 | a |
+| test_free.cpp:23:10:23:10 | a |
+| test_free.cpp:25:10:25:10 | a |
+| test_free.cpp:26:10:26:10 | b |
+| test_free.cpp:30:10:30:10 | a |
+| test_free.cpp:31:27:31:27 | a |
+| test_free.cpp:35:10:35:10 | a |
+| test_free.cpp:37:27:37:27 | a |
+| test_free.cpp:42:27:42:27 | a |
+| test_free.cpp:44:27:44:27 | a |
+| test_free.cpp:46:10:46:10 | a |
+| test_free.cpp:50:27:50:27 | a |
+| test_free.cpp:51:10:51:10 | a |
+| test_free.cpp:55:27:55:27 | a |
+| test_free.cpp:57:10:57:10 | a |
+| test_free.cpp:61:10:61:10 | a |
+| test_free.cpp:63:10:63:10 | b |
+| test_free.cpp:69:10:69:10 | a |
+| test_free.cpp:72:14:72:14 | a |
+| test_free.cpp:83:12:83:12 | a |
+| test_free.cpp:85:12:85:12 | a |
+| test_free.cpp:90:10:90:10 | a |
+| test_free.cpp:95:10:95:10 | a |
+| test_free.cpp:101:10:101:10 | a |
+| test_free.cpp:102:23:102:23 | a |
+| test_free.cpp:103:10:103:10 | a |
+| test_free.cpp:104:10:104:10 | b |
+| test_free.cpp:107:23:107:23 | a |
+| test_free.cpp:112:14:112:14 | a |
+| test_free.cpp:114:10:114:10 | b |
+| test_free.cpp:118:23:118:23 | a |
+| test_free.cpp:119:17:119:17 | b |
+| test_free.cpp:121:14:121:14 | a |
+| test_free.cpp:126:10:126:11 | * ... |
+| test_free.cpp:128:10:128:11 | * ... |
+| test_free.cpp:129:10:129:11 | * ... |
+| test_free.cpp:131:10:131:13 | access to array |
+| test_free.cpp:132:10:132:13 | access to array |
+| test_free.cpp:143:27:143:30 | data |
+| test_free.cpp:145:14:145:22 | * ... |
+| test_free.cpp:148:10:148:17 | list_ptr |
+| test_free.cpp:152:27:152:27 | a |
+| test_free.cpp:154:10:154:10 | a |
+| test_free.cpp:159:14:159:15 | * ... |
+| test_free.cpp:162:10:162:10 | a |
+| test_free.cpp:167:23:167:23 | a |
+| test_free.cpp:173:10:173:10 | a |
+| test_free.cpp:181:10:181:10 | a |
+| test_free.cpp:183:10:183:10 | a |
+| test_free.cpp:185:10:185:10 | a |
+| test_free.cpp:188:10:188:10 | a |
+| test_free.cpp:193:20:193:20 | a |
+| test_free.cpp:199:20:199:20 | a |
+| test_free.cpp:205:10:205:10 | a |
+| test_free.cpp:207:10:207:10 | a |
+| test_free.cpp:209:10:209:10 | a |
+| test_free.cpp:213:10:213:10 | a |
+| test_free.cpp:216:10:216:10 | a |
+| test_free.cpp:220:10:220:10 | a |
+| test_free.cpp:227:24:227:45 | memory_descriptor_list |
 | virtual.cpp:18:10:18:10 | a |
 | virtual.cpp:19:10:19:10 | c |
 | virtual.cpp:38:10:38:10 | b |
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryMayNotBeFreed.expected b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryMayNotBeFreed.expected
index e69de29bb2d..fa069b8b46a 100644
--- a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryMayNotBeFreed.expected
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryMayNotBeFreed.expected
@@ -0,0 +1 @@
+| test_free.cpp:36:22:36:35 | ... = ... | This memory allocation may not be released at $@. | test_free.cpp:38:1:38:1 | return ... | this exit point |
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryNeverFreed.expected b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryNeverFreed.expected
index 71ba526c674..827c207b659 100644
--- a/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryNeverFreed.expected
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/MemoryNeverFreed.expected
@@ -11,3 +11,4 @@
 | test.cpp:156:3:156:26 | new | This memory is never freed. |
 | test.cpp:157:3:157:26 | new[] | This memory is never freed. |
 | test.cpp:169:14:169:19 | call to strdup | This memory is never freed. |
+| test_free.cpp:167:15:167:21 | call to realloc | This memory is never freed. |
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.expected b/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.expected
new file mode 100644
index 00000000000..56f2d0370a5
--- /dev/null
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.expected
@@ -0,0 +1,59 @@
+edges
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:12:5:12:5 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:12:5:12:5 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:13:6:13:6 | a |
+| test_free.cpp:11:10:11:10 | a | test_free.cpp:13:6:13:6 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:45:5:45:5 | a |
+| test_free.cpp:42:27:42:27 | a | test_free.cpp:45:5:45:5 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:45:5:45:5 | a |
+| test_free.cpp:44:27:44:27 | a | test_free.cpp:45:5:45:5 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:71:9:71:9 | a |
+| test_free.cpp:69:10:69:10 | a | test_free.cpp:71:9:71:9 | a |
+| test_free.cpp:90:10:90:10 | a | test_free.cpp:91:5:91:5 | a |
+| test_free.cpp:90:10:90:10 | a | test_free.cpp:91:5:91:5 | a |
+| test_free.cpp:95:10:95:10 | a | test_free.cpp:96:9:96:9 | a |
+| test_free.cpp:101:10:101:10 | a | test_free.cpp:102:23:102:23 | a |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:153:5:153:5 | a |
+| test_free.cpp:152:27:152:27 | a | test_free.cpp:153:5:153:5 | a |
+nodes
+| test_free.cpp:11:10:11:10 | a | semmle.label | a |
+| test_free.cpp:11:10:11:10 | a | semmle.label | a |
+| test_free.cpp:12:5:12:5 | a | semmle.label | a |
+| test_free.cpp:13:6:13:6 | a | semmle.label | a |
+| test_free.cpp:42:27:42:27 | a | semmle.label | a |
+| test_free.cpp:42:27:42:27 | a | semmle.label | a |
+| test_free.cpp:44:27:44:27 | a | semmle.label | a |
+| test_free.cpp:44:27:44:27 | a | semmle.label | a |
+| test_free.cpp:45:5:45:5 | a | semmle.label | a |
+| test_free.cpp:45:5:45:5 | a | semmle.label | a |
+| test_free.cpp:69:10:69:10 | a | semmle.label | a |
+| test_free.cpp:69:10:69:10 | a | semmle.label | a |
+| test_free.cpp:71:9:71:9 | a | semmle.label | a |
+| test_free.cpp:90:10:90:10 | a | semmle.label | a |
+| test_free.cpp:90:10:90:10 | a | semmle.label | a |
+| test_free.cpp:91:5:91:5 | a | semmle.label | a |
+| test_free.cpp:95:10:95:10 | a | semmle.label | a |
+| test_free.cpp:96:9:96:9 | a | semmle.label | a |
+| test_free.cpp:101:10:101:10 | a | semmle.label | a |
+| test_free.cpp:102:23:102:23 | a | semmle.label | a |
+| test_free.cpp:152:27:152:27 | a | semmle.label | a |
+| test_free.cpp:152:27:152:27 | a | semmle.label | a |
+| test_free.cpp:153:5:153:5 | a | semmle.label | a |
+subpaths
+#select
+| test_free.cpp:12:5:12:5 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:12:5:12:5 | a | Memory may have been previously freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:12:5:12:5 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:12:5:12:5 | a | Memory may have been previously freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:13:6:13:6 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:13:6:13:6 | a | Memory may have been previously freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:13:6:13:6 | a | test_free.cpp:11:10:11:10 | a | test_free.cpp:13:6:13:6 | a | Memory may have been previously freed by $@. | test_free.cpp:11:5:11:8 | call to free | call to free |
+| test_free.cpp:45:5:45:5 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:45:5:45:5 | a | Memory may have been previously freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:45:5:45:5 | a | test_free.cpp:42:27:42:27 | a | test_free.cpp:45:5:45:5 | a | Memory may have been previously freed by $@. | test_free.cpp:42:22:42:25 | call to free | call to free |
+| test_free.cpp:45:5:45:5 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:45:5:45:5 | a | Memory may have been previously freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:45:5:45:5 | a | test_free.cpp:44:27:44:27 | a | test_free.cpp:45:5:45:5 | a | Memory may have been previously freed by $@. | test_free.cpp:44:22:44:25 | call to free | call to free |
+| test_free.cpp:71:9:71:9 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:71:9:71:9 | a | Memory may have been previously freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:71:9:71:9 | a | test_free.cpp:69:10:69:10 | a | test_free.cpp:71:9:71:9 | a | Memory may have been previously freed by $@. | test_free.cpp:69:5:69:8 | call to free | call to free |
+| test_free.cpp:91:5:91:5 | a | test_free.cpp:90:10:90:10 | a | test_free.cpp:91:5:91:5 | a | Memory may have been previously freed by $@. | test_free.cpp:90:5:90:8 | call to free | call to free |
+| test_free.cpp:91:5:91:5 | a | test_free.cpp:90:10:90:10 | a | test_free.cpp:91:5:91:5 | a | Memory may have been previously freed by $@. | test_free.cpp:90:5:90:8 | call to free | call to free |
+| test_free.cpp:96:9:96:9 | a | test_free.cpp:95:10:95:10 | a | test_free.cpp:96:9:96:9 | a | Memory may have been previously freed by $@. | test_free.cpp:95:5:95:8 | call to free | call to free |
+| test_free.cpp:102:23:102:23 | a | test_free.cpp:101:10:101:10 | a | test_free.cpp:102:23:102:23 | a | Memory may have been previously freed by $@. | test_free.cpp:101:5:101:8 | call to free | call to free |
+| test_free.cpp:153:5:153:5 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:153:5:153:5 | a | Memory may have been previously freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
+| test_free.cpp:153:5:153:5 | a | test_free.cpp:152:27:152:27 | a | test_free.cpp:153:5:153:5 | a | Memory may have been previously freed by $@. | test_free.cpp:152:22:152:25 | call to free | call to free |
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.qlref b/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.qlref
new file mode 100644
index 00000000000..e299a3055e0
--- /dev/null
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/UseAfterFree.qlref
@@ -0,0 +1 @@
+Critical/UseAfterFree.ql
\ No newline at end of file
diff --git a/cpp/ql/test/query-tests/Critical/MemoryFreed/test_free.cpp b/cpp/ql/test/query-tests/Critical/MemoryFreed/test_free.cpp
new file mode 100644
index 00000000000..82b5d8eac6e
--- /dev/null
+++ b/cpp/ql/test/query-tests/Critical/MemoryFreed/test_free.cpp
@@ -0,0 +1,229 @@
+void *malloc(int);
+void free(void *);
+bool condition();
+void use(void*);
+void *realloc(void*, unsigned long);
+int strlen(char*);
+int asprintf(char ** strp, const char * fmt, ...);
+
+
+void* test_double_free1(int *a) {
+    free(a); // GOOD
+    a[5] = 5; // BAD
+    *a = 5; // BAD
+    free(a); // BAD
+    a = (int*) malloc(8);
+    free(a); // GOOD
+    a = (int*) malloc(8);
+    if (!a) free(a);
+    return a;
+}
+
+void test_double_free_aliasing(void *a, void* b) {
+    free(a); // GOOD
+    a = b;
+    free(a); // GOOD
+    free(b); // BAD [NOT DETECTED]
+}
+
+void test_dominance1(void *a) {
+    free(a);
+    if (condition()) free(a); // BAD
+}
+
+void test_dominance2(void *a) {
+    free(a);
+    if (condition()) a = malloc(10);
+    if (condition()) free(a); // BAD
+}
+
+void test_post_dominance1(int *a)
+{
+    if (condition()) free(a);
+    if (condition()) a[2] = 5; // BAD [NOT DETECTED]
+    if (condition()) free(a); // BAD [NOT DETECTED]
+    a[2] = 5; // BAD
+    free(a); // BAD
+}
+
+void test_post_dominance2(void *a) {
+    if (condition()) free(a);
+    free(a); // BAD
+}
+
+void test_post_dominance3(void *a) {
+    if (condition()) free(a);
+    a = malloc(10);
+    free(a); // GOOD
+}
+
+void test_use_after_free6(int *a, int *b) {
+    free(a);
+    a=b;
+    free(b);
+    if (condition()) a[0] = 5; // BAD [NOT DETECTED]
+}
+
+void test_use_after_free7(int *a) {
+    a[0] = 42;
+    free(a);
+
+    if (a[3]) { // BAD
+        free(a); // BAD
+    }
+}
+
+class A {
+public:
+    void f();
+};
+
+void test_new1() {
+    A *a = new A();
+    delete(a);
+    a->f(); // BAD [NOT DETECTED]
+    delete(a); // BAD [NOT DETECTED]
+}
+
+void test_dereference1(A *a) {
+    a->f(); // GOOD
+    free(a);
+    a->f(); // BAD
+}
+
+void* use_after_free(void *a) {
+    free(a);
+    use(a); // BAD
+    return a; // BAD
+}
+
+void test_realloc1(void *a) {
+    free(a);
+    void *b = realloc(a, sizeof(a)*3); // BAD [NOT DETECTED by cpp/double-free]
+    free(a); // BAD
+    free(b); // GOOD
+}
+void* test_realloc2(char *a) {
+    void *b = realloc(a, strlen(a)+3); // GOOD
+
+    // From the man page on return values from realloc and reallocarray:
+    // "If these functions  fail, the original block is left untouched; it is not freed or moved."
+    if (!b) {
+        free(a); // GOOD
+    }
+    free(b); // GOOD
+}
+
+void test_realloc3(void *a) {
+    void *b = realloc(a, 100);
+    if (b) free(b); // GOOD
+    if (!b) {
+        free(a); // GOOD
+    }
+}
+
+void test_ptr_deref(void ** a) {
+    free(*a);
+    *a = malloc(10);
+    free(*a); // GOOD
+    free(*a); // BAD [NOT DETECTED]
+    *a = malloc(10);
+    free(a[0]); // GOOD
+    free(a[1]); // GOOD
+}
+
+struct list {
+    struct list *next;
+    void* data;
+};
+
+void test_loop1(struct list ** list_ptr) {
+    struct list *next;
+    while (*list_ptr) { // GOOD
+        free((*list_ptr)->data); // GOOD
+        next = (*list_ptr)->next; // GOOD
+        free(*list_ptr); // GOOD
+        *list_ptr = next; // GOOD
+    }
+    free(list_ptr); // GOOD
+}
+
+void test_use_after_free8(struct list * a) {
+    if (condition()) free(a);
+    a->data = malloc(10); // BAD
+    free(a); // BAD
+}
+
+void test_loop2(char ** a) {
+    while (*a) { // GOOD
+        free(*a); // GOOD
+        a++;
+    }
+    free(a); // GOOD
+}
+
+void* test_realloc4() {
+    void *a = 0;
+    void *b = realloc(a, 10); // BAD for cpp/memory-never-freed
+    if (!b) { return a; }
+    return b;
+}
+
+void test_sizeof(int *a) {
+    free(a);
+    int x = sizeof(a[0]); // GOOD
+}
+
+void call_by_reference(char * &a);
+int custom_alloc_func(char ** a);
+
+void test_reassign(char *a) {
+    free(a); // GOOD
+    asprintf(&a, "Hello world"); // GOOD
+    free(a); //GOOD
+    call_by_reference(a); // GOOD
+    free(a); // GOOD
+    int v;
+    if (v = custom_alloc_func(&a)) return;
+    free(a); // GOOD
+}
+
+char* test_return1(char *a) {
+    int ret = condition();
+    if (!ret) free(a);
+    return (ret ? a : 0);
+}
+
+char* test_return2(char *a) {
+    int ret = condition();
+    if (!ret) free(a);
+    if (ret) return a;
+    else return 0;
+}
+
+void test_condition1(char *a) {
+    free(a);
+    if (asprintf(&a, "Hello world") || condition());
+    free(a); //GOOD
+    if (condition() || asprintf(&a, "Hello world"));
+    free(a); // BAD
+}
+
+void test_condition2(char *a) {
+    free(a);
+    if (condition()) a = (char*) malloc(10);
+    else custom_alloc_func(&a);
+    free(a); // GOOD
+}
+
+void* test_return1(void *a) {
+    free(a);
+    return a;
+}
+
+void MmFreePagesFromMdl(void*);
+void ExFreePool(void*);
+void test_ms_free(void * memory_descriptor_list) {
+    MmFreePagesFromMdl(memory_descriptor_list); //GOOD
+    ExFreePool(memory_descriptor_list); // GOOD
+}
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/UseAfterFree.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/UseAfterFree.expected
index ba5cf94b5b1..e95af7ceb10 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/UseAfterFree.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/UseAfterFree.expected
@@ -1,9 +1,74 @@
-| test.cpp:36:6:36:9 | data | Memory pointed to by 'data' may have $@. | test.cpp:35:2:35:5 | call to free | been previously freed |
-| test.cpp:70:7:70:10 | data | Memory pointed to by 'data' may have $@. | test.cpp:67:2:67:5 | call to free | been previously freed |
-| test.cpp:107:6:107:9 | data | Memory pointed to by 'data' may have $@. | test.cpp:105:2:105:5 | call to free | been previously freed |
-| test.cpp:117:6:117:9 | data | Memory pointed to by 'data' may have $@. | test.cpp:115:2:115:5 | call to free | been previously freed |
-| test.cpp:150:2:150:2 | c | Memory pointed to by 'c' may have $@. | test.cpp:149:2:149:10 | delete | been previously freed |
-| test.cpp:151:4:151:4 | c | Memory pointed to by 'c' may have $@. | test.cpp:149:2:149:10 | delete | been previously freed |
-| test.cpp:170:6:170:9 | data | Memory pointed to by 'data' may have $@. | test.cpp:165:2:165:5 | call to free | been previously freed |
-| test.cpp:193:6:193:9 | data | Memory pointed to by 'data' may have $@. | test.cpp:191:3:191:6 | call to free | been previously freed |
-| test.cpp:201:6:201:6 | x | Memory pointed to by 'x' may have $@. | test.cpp:200:2:200:9 | delete | been previously freed |
+edges
+| test.cpp:39:7:39:10 | data | test.cpp:41:6:41:9 | data |
+| test.cpp:39:7:39:10 | data | test.cpp:41:6:41:9 | data |
+| test.cpp:75:7:75:10 | data | test.cpp:79:7:79:10 | data |
+| test.cpp:75:7:75:10 | data | test.cpp:79:7:79:10 | data |
+| test.cpp:106:7:106:10 | data | test.cpp:108:6:108:9 | data |
+| test.cpp:106:7:106:10 | data | test.cpp:108:6:108:9 | data |
+| test.cpp:116:7:116:10 | data | test.cpp:119:6:119:9 | data |
+| test.cpp:116:7:116:10 | data | test.cpp:119:6:119:9 | data |
+| test.cpp:127:7:127:10 | data | test.cpp:130:6:130:9 | data |
+| test.cpp:127:7:127:10 | data | test.cpp:130:6:130:9 | data |
+| test.cpp:138:7:138:10 | data | test.cpp:141:6:141:9 | data |
+| test.cpp:138:7:138:10 | data | test.cpp:141:6:141:9 | data |
+| test.cpp:181:7:181:10 | data | test.cpp:186:6:186:9 | data |
+| test.cpp:181:7:181:10 | data | test.cpp:186:6:186:9 | data |
+| test.cpp:192:7:192:10 | data | test.cpp:197:6:197:9 | data |
+| test.cpp:192:7:192:10 | data | test.cpp:197:6:197:9 | data |
+| test.cpp:203:7:203:10 | data | test.cpp:209:6:209:9 | data |
+| test.cpp:203:7:203:10 | data | test.cpp:209:6:209:9 | data |
+| test.cpp:207:8:207:11 | data | test.cpp:209:6:209:9 | data |
+| test.cpp:207:8:207:11 | data | test.cpp:209:6:209:9 | data |
+nodes
+| test.cpp:39:7:39:10 | data | semmle.label | data |
+| test.cpp:39:7:39:10 | data | semmle.label | data |
+| test.cpp:41:6:41:9 | data | semmle.label | data |
+| test.cpp:75:7:75:10 | data | semmle.label | data |
+| test.cpp:75:7:75:10 | data | semmle.label | data |
+| test.cpp:79:7:79:10 | data | semmle.label | data |
+| test.cpp:106:7:106:10 | data | semmle.label | data |
+| test.cpp:106:7:106:10 | data | semmle.label | data |
+| test.cpp:108:6:108:9 | data | semmle.label | data |
+| test.cpp:116:7:116:10 | data | semmle.label | data |
+| test.cpp:116:7:116:10 | data | semmle.label | data |
+| test.cpp:119:6:119:9 | data | semmle.label | data |
+| test.cpp:127:7:127:10 | data | semmle.label | data |
+| test.cpp:127:7:127:10 | data | semmle.label | data |
+| test.cpp:130:6:130:9 | data | semmle.label | data |
+| test.cpp:138:7:138:10 | data | semmle.label | data |
+| test.cpp:138:7:138:10 | data | semmle.label | data |
+| test.cpp:141:6:141:9 | data | semmle.label | data |
+| test.cpp:181:7:181:10 | data | semmle.label | data |
+| test.cpp:181:7:181:10 | data | semmle.label | data |
+| test.cpp:186:6:186:9 | data | semmle.label | data |
+| test.cpp:192:7:192:10 | data | semmle.label | data |
+| test.cpp:192:7:192:10 | data | semmle.label | data |
+| test.cpp:197:6:197:9 | data | semmle.label | data |
+| test.cpp:203:7:203:10 | data | semmle.label | data |
+| test.cpp:203:7:203:10 | data | semmle.label | data |
+| test.cpp:207:8:207:11 | data | semmle.label | data |
+| test.cpp:207:8:207:11 | data | semmle.label | data |
+| test.cpp:209:6:209:9 | data | semmle.label | data |
+| test.cpp:209:6:209:9 | data | semmle.label | data |
+subpaths
+#select
+| test.cpp:41:6:41:9 | data | test.cpp:39:7:39:10 | data | test.cpp:41:6:41:9 | data | Memory may have been previously freed by $@. | test.cpp:39:2:39:5 | call to free | call to free |
+| test.cpp:41:6:41:9 | data | test.cpp:39:7:39:10 | data | test.cpp:41:6:41:9 | data | Memory may have been previously freed by $@. | test.cpp:39:2:39:5 | call to free | call to free |
+| test.cpp:79:7:79:10 | data | test.cpp:75:7:75:10 | data | test.cpp:79:7:79:10 | data | Memory may have been previously freed by $@. | test.cpp:75:2:75:5 | call to free | call to free |
+| test.cpp:79:7:79:10 | data | test.cpp:75:7:75:10 | data | test.cpp:79:7:79:10 | data | Memory may have been previously freed by $@. | test.cpp:75:2:75:5 | call to free | call to free |
+| test.cpp:108:6:108:9 | data | test.cpp:106:7:106:10 | data | test.cpp:108:6:108:9 | data | Memory may have been previously freed by $@. | test.cpp:106:2:106:5 | call to free | call to free |
+| test.cpp:108:6:108:9 | data | test.cpp:106:7:106:10 | data | test.cpp:108:6:108:9 | data | Memory may have been previously freed by $@. | test.cpp:106:2:106:5 | call to free | call to free |
+| test.cpp:119:6:119:9 | data | test.cpp:116:7:116:10 | data | test.cpp:119:6:119:9 | data | Memory may have been previously freed by $@. | test.cpp:116:2:116:5 | call to free | call to free |
+| test.cpp:119:6:119:9 | data | test.cpp:116:7:116:10 | data | test.cpp:119:6:119:9 | data | Memory may have been previously freed by $@. | test.cpp:116:2:116:5 | call to free | call to free |
+| test.cpp:130:6:130:9 | data | test.cpp:127:7:127:10 | data | test.cpp:130:6:130:9 | data | Memory may have been previously freed by $@. | test.cpp:127:2:127:5 | call to free | call to free |
+| test.cpp:130:6:130:9 | data | test.cpp:127:7:127:10 | data | test.cpp:130:6:130:9 | data | Memory may have been previously freed by $@. | test.cpp:127:2:127:5 | call to free | call to free |
+| test.cpp:141:6:141:9 | data | test.cpp:138:7:138:10 | data | test.cpp:141:6:141:9 | data | Memory may have been previously freed by $@. | test.cpp:138:2:138:5 | call to free | call to free |
+| test.cpp:141:6:141:9 | data | test.cpp:138:7:138:10 | data | test.cpp:141:6:141:9 | data | Memory may have been previously freed by $@. | test.cpp:138:2:138:5 | call to free | call to free |
+| test.cpp:186:6:186:9 | data | test.cpp:181:7:181:10 | data | test.cpp:186:6:186:9 | data | Memory may have been previously freed by $@. | test.cpp:181:2:181:5 | call to free | call to free |
+| test.cpp:186:6:186:9 | data | test.cpp:181:7:181:10 | data | test.cpp:186:6:186:9 | data | Memory may have been previously freed by $@. | test.cpp:181:2:181:5 | call to free | call to free |
+| test.cpp:197:6:197:9 | data | test.cpp:192:7:192:10 | data | test.cpp:197:6:197:9 | data | Memory may have been previously freed by $@. | test.cpp:192:2:192:5 | call to free | call to free |
+| test.cpp:197:6:197:9 | data | test.cpp:192:7:192:10 | data | test.cpp:197:6:197:9 | data | Memory may have been previously freed by $@. | test.cpp:192:2:192:5 | call to free | call to free |
+| test.cpp:209:6:209:9 | data | test.cpp:203:7:203:10 | data | test.cpp:209:6:209:9 | data | Memory may have been previously freed by $@. | test.cpp:203:2:203:5 | call to free | call to free |
+| test.cpp:209:6:209:9 | data | test.cpp:203:7:203:10 | data | test.cpp:209:6:209:9 | data | Memory may have been previously freed by $@. | test.cpp:203:2:203:5 | call to free | call to free |
+| test.cpp:209:6:209:9 | data | test.cpp:207:8:207:11 | data | test.cpp:209:6:209:9 | data | Memory may have been previously freed by $@. | test.cpp:207:3:207:6 | call to free | call to free |
+| test.cpp:209:6:209:9 | data | test.cpp:207:8:207:11 | data | test.cpp:209:6:209:9 | data | Memory may have been previously freed by $@. | test.cpp:207:3:207:6 | call to free | call to free |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/test.cpp b/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/test.cpp
index 7018af457ba..1d15293e3ee 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/test.cpp
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-416/semmle/tests/test.cpp
@@ -6,14 +6,18 @@ typedef unsigned long size_t;
 void *malloc(size_t size);
 void free(void *ptr);
 
-void useExternal(char* data);
+void useExternal(...);
 
-void use(char* data)
+void use_if_nonzero(char* data)
 {
 	if (data)
 		useExternal(data);
 }
 
+void use(char* data) {
+	useExternal(*data);
+}
+
 [[noreturn]]
 void noReturn();
 
@@ -31,8 +35,9 @@ void test1()
 {
 	char* data;
 	data = (char *)malloc(100*sizeof(char));
-	use(data); // GOOD
+	use_if_nonzero(data); // GOOD
 	free(data);
+	use_if_nonzero(data); // BAD [NOT DETECTED]
 	use(data); // BAD
 }
 
@@ -42,9 +47,11 @@ void test2()
 	data = (char *)malloc(100*sizeof(char));
 	free(data);
 	myMalloc(&data);
+	use_if_nonzero(data); // GOOD
 	use(data); // GOOD
 	free(data);
 	myMalloc2(data);
+	use_if_nonzero(data); // GOOD
 	use(data); // GOOD
 }
 
@@ -56,6 +63,7 @@ void test3()
 	data = NULL;
 	if (data)
 	{
+		use_if_nonzero(data); // GOOD
 		use(data); // GOOD
 	}
 }
@@ -67,6 +75,7 @@ void test4()
 	free(data);
 	if (data)
 	{
+		use_if_nonzero(data); // BAD [NOT DETECTED]
 		use(data); // BAD
 	}
 }
@@ -85,7 +94,8 @@ char* returnsFreedData(int i)
 void test5()
 {
 	char* data = returnsFreedData(1);
-	use(data); // BAD (NOT REPORTED)
+	use_if_nonzero(data); // BAD [NOT DETECTED]
+	use(data); // BAD [NOT DETECTED]
 }
 
 void test6()
@@ -94,7 +104,8 @@ void test6()
 	data = (char *)malloc(100*sizeof(char));
 	data2 = data;
 	free(data);
-	use(data2); // BAD (NOT REPORTED)
+	use_if_nonzero(data2); // BAD [NOT DETECTED]
+	use(data); // BAD
 }
 
 void test7()
@@ -104,6 +115,7 @@ void test7()
 	data2 = data;
 	free(data);
 	data2 = NULL;
+	use_if_nonzero(data); // BAD [NOT DETECTED]
 	use(data); // BAD
 }
 
@@ -114,6 +126,7 @@ void test8()
 	data = data2;
 	free(data);
 	data2 = NULL;
+	use_if_nonzero(data); // BAD [NOT DETECTED]
 	use(data); // BAD
 }
 
@@ -124,13 +137,15 @@ void test9()
 	char *data, *data2;
 	free(data);
 	noReturnWrapper();
-	use(data); // GOOD
+	use_if_nonzero(data); // GOOD
+	use(data); // GOOD [FALSE POSITIVE]
 }
 
 void test10()
 {
 	for (char *data; true; data = NULL)
 	{
+		use_if_nonzero(data); // GOOD
 		use(data); // GOOD
 		free(data);
 	}
@@ -140,7 +155,7 @@ class myClass
 {
 public:
 	myClass() { }
-	
+
 	void myMethod() { }
 };
 
@@ -156,7 +171,8 @@ template<class T> T test()
 	T* x;
 	use(x); // GOOD
 	delete x;
-	use(x); // BAD
+	use_if_nonzero(x); // BAD [NOT DETECTED]
+	use(x); // BAD [NOT DETECTED]
 }
 
 void test12(int count)
@@ -178,7 +194,7 @@ void test13()
 	{
 		data = NULL;
 	}
-	use(data); // GOOD
+	use(data); // GOOD [FALSE POSITIVE]
 }
 
 void test14()
@@ -198,7 +214,7 @@ template<class T> T test15()
 	T* x;
 	use(x); // GOOD
 	delete x;
-	use(x); // BAD
+	use(x); // BAD [NOT DETECTED]
 }
 void test15runner(void)
 {