C++: Add extensible predicate for deallocation.

cpp/ql/lib/semmle/code/cpp/models/implementations/Deallocation.qll

@@ -64,6 +64,45 @@ private class StandardDeallocationFunction extends DeallocationFunction {
   override int getFreedArg() { result = freedArg }
 }
 
+/**
+ * Holds if `f` is an deallocation function according to the
+ * extensible `deallocationFunctionModel` predicate.
+ */
+private predicate isDeallocationFunctionFromModel(
+  Function f, string namespace, string type, string name
+) {
+  exists(boolean subtypes | deallocationFunctionModel(namespace, type, subtypes, name, _) |
+    if type = ""
+    then f.hasQualifiedName(namespace, "", name)
+    else
+      exists(Class c |
+        c.hasQualifiedName(namespace, type) and f.hasQualifiedName(namespace, _, name)
+      |
+        if subtypes = true
+        then f = c.getADerivedClass*().getAMemberFunction()
+        else f = c.getAMemberFunction()
+      )
+  )
+}
+
+/**
+ * A deallocation function modeled via the extensible `deallocationFunctionModel` predicate.
+ */
+private class DeallocationFunctionFromModel extends DeallocationFunction {
+  string namespace;
+  string type;
+  string name;
+
+  DeallocationFunctionFromModel() { isDeallocationFunctionFromModel(this, namespace, type, name) }
+
+  final override int getFreedArg() {
+    exists(string freedArg |
+      deallocationFunctionModel(namespace, type, _, name, freedArg) and
+      result = freedArg.toInt()
+    )
+  }
+}
+
 /**
  * An deallocation expression that is a function call, such as call to `free`.
  */

cpp/ql/lib/semmle/code/cpp/models/interfaces/Deallocation.qll

@@ -34,6 +34,13 @@ abstract class DeallocationFunction extends Function {
   int getFreedArg() { none() }
 }
 
+/**
+ * Holds if an external deallocation model exists for the given parameters.
+ */
+extensible predicate deallocationFunctionModel(
+  string namespace, string type, boolean subtypes, string name, string freedArg
+);
+
 /**
  * An `operator delete` or `operator delete[]` function that may be associated
  * with `delete` or `delete[]` expressions.  Note that `delete` and `delete[]`