diff --git a/cpp/ql/src/semmle/code/cpp/controlflow/BasicBlocks.qll b/cpp/ql/src/semmle/code/cpp/controlflow/BasicBlocks.qll
index 681d0b710f60..16947019f544 100644
--- a/cpp/ql/src/semmle/code/cpp/controlflow/BasicBlocks.qll
+++ b/cpp/ql/src/semmle/code/cpp/controlflow/BasicBlocks.qll
@@ -1,3 +1,8 @@
+/**
+ * Provides a library for reasoning about control flow at the granularity of basic blocks.
+ * This is usually much more efficient than reasoning directly at the level of `ControlFlowNode`s.
+ */
+
 import cpp
 private import internal.PrimitiveBasicBlocks
 private import internal.ConstantExprs
@@ -148,22 +153,37 @@ predicate bb_successor = bb_successor_cached/2;
 class BasicBlock extends ControlFlowNodeBase {
   BasicBlock() { basic_block_entry_node(this) }
 
+  /** Holds if this basic block contains `node`. */
   predicate contains(ControlFlowNode node) { basic_block_member(node, this, _) }
 
+  /** Gets the `ControlFlowNode` at position `pos` in this basic block. */
   ControlFlowNode getNode(int pos) { basic_block_member(result, this, pos) }
 
+  /** Gets a `ControlFlowNode` in this basic block. */
   ControlFlowNode getANode() { basic_block_member(result, this, _) }
 
+  /** Gets a `BasicBlock` that is a direct successor of this basic block. */
   BasicBlock getASuccessor() { bb_successor(this, result) }
 
+  /** Gets a `BasicBlock` that is a direct predecessor of this basic block. */
   BasicBlock getAPredecessor() { bb_successor(result, this) }
 
+  /**
+   * Gets a `BasicBlock` such that the control-flow edge `(this, result)` may be taken
+   * when the outgoing edge of this basic block is an expression that is true.
+   */
   BasicBlock getATrueSuccessor() { result.getStart() = this.getEnd().getATrueSuccessor() }
 
+  /**
+   * Gets a `BasicBlock` such that the control-flow edge `(this, result)` may be taken
+   * when the outgoing edge of this basic block is an expression that is false.
+   */
   BasicBlock getAFalseSuccessor() { result.getStart() = this.getEnd().getAFalseSuccessor() }
 
+  /** Gets the final `ControlFlowNode` of this basic block. */
   ControlFlowNode getEnd() { basic_block_member(result, this, bb_length(this) - 1) }
 
+  /** Gets the first `ControlFlowNode` of this basic block. */
   ControlFlowNode getStart() { result = this }
 
   /** Gets the number of `ControlFlowNode`s in this basic block. */
@@ -192,6 +212,7 @@ class BasicBlock extends ControlFlowNodeBase {
     this.getEnd().getLocation().hasLocationInfo(endf, _, _, endl, endc)
   }
 
+  /** Gets the function containing this basic block. */
   Function getEnclosingFunction() { result = this.getStart().getControlFlowScope() }
 
   /**
diff --git a/cpp/ql/src/semmle/code/cpp/controlflow/ControlFlowGraph.qll b/cpp/ql/src/semmle/code/cpp/controlflow/ControlFlowGraph.qll
index 9174f474a8f2..1f79d6c5bc20 100644
--- a/cpp/ql/src/semmle/code/cpp/controlflow/ControlFlowGraph.qll
+++ b/cpp/ql/src/semmle/code/cpp/controlflow/ControlFlowGraph.qll
@@ -1,3 +1,8 @@
+/**
+ * Provides a library for reasoning about control flow at the granularity of
+ * individual nodes in the control-flow graph.
+ */
+
 import cpp
 import BasicBlocks
 private import semmle.code.cpp.controlflow.internal.ConstantExprs
@@ -29,8 +34,10 @@ private import semmle.code.cpp.controlflow.internal.CFG
  * `Handler`. There are no edges from function calls to `Handler`s.
  */
 class ControlFlowNode extends Locatable, ControlFlowNodeBase {
+  /** Gets a direct successor of this control-flow node, if any. */
   ControlFlowNode getASuccessor() { successors_adapted(this, result) }
 
+  /** Gets a direct predecessor of this control-flow node, if any. */
   ControlFlowNode getAPredecessor() { this = result.getASuccessor() }
 
   /** Gets the function containing this control-flow node. */
@@ -71,6 +78,7 @@ class ControlFlowNode extends Locatable, ControlFlowNodeBase {
     result = getASuccessor()
   }
 
+  /** Gets the `BasicBlock` containing this control-flow node. */
   BasicBlock getBasicBlock() { result.getANode() = this }
 }
 
@@ -86,10 +94,18 @@ import ControlFlowGraphPublic
  */
 class ControlFlowNodeBase extends ElementBase, @cfgnode { }
 
+/**
+ * Holds when `n2` is a control-flow node such that the control-flow
+ * edge `(n1, n2)` may be taken when `n1` is an expression that is true.
+ */
 predicate truecond_base(ControlFlowNodeBase n1, ControlFlowNodeBase n2) {
   qlCFGTrueSuccessor(n1, n2)
 }
 
+/**
+ * Holds when `n2` is a control-flow node such that the control-flow
+ * edge `(n1, n2)` may be taken when `n1` is an expression that is false.
+ */
 predicate falsecond_base(ControlFlowNodeBase n1, ControlFlowNodeBase n2) {
   qlCFGFalseSuccessor(n1, n2)
 }
diff --git a/cpp/ql/src/semmle/code/cpp/controlflow/Dataflow.qll b/cpp/ql/src/semmle/code/cpp/controlflow/Dataflow.qll
index 99fb69660994..1a5d81ee9f30 100644
--- a/cpp/ql/src/semmle/code/cpp/controlflow/Dataflow.qll
+++ b/cpp/ql/src/semmle/code/cpp/controlflow/Dataflow.qll
@@ -15,14 +15,25 @@ import Dereferenced
 abstract class DataflowAnnotation extends string {
   DataflowAnnotation() { this = "pointer-null" or this = "pointer-valid" }
 
+  /** Holds if this annotation is the default annotation. */
   abstract predicate isDefault();
 
+  /** Holds if this annotation is generated when analyzing expression `e`. */
   abstract predicate generatedOn(Expr e);
 
+  /**
+   * Holds if this annotation is generated for the variable `v` when
+   * the control-flow edge `(src, dest)` is taken.
+   */
   abstract predicate generatedBy(LocalScopeVariable v, ControlFlowNode src, ControlFlowNode dest);
 
+  /**
+   * Holds if this annotation is removed for the variable `v` when
+   * the control-flow edge `(src, dest)` is taken.
+   */
   abstract predicate killedBy(LocalScopeVariable v, ControlFlowNode src, ControlFlowNode dest);
 
+  /** Holds if expression `e` is given this annotation. */
   predicate marks(Expr e) {
     this.generatedOn(e) and reachable(e)
     or
@@ -31,6 +42,7 @@ abstract class DataflowAnnotation extends string {
     exists(LocalScopeVariable v | this.marks(v, e) and e = v.getAnAccess())
   }
 
+  /** Holds if the variable `v` accessed in control-flow node `n` is given this annotation. */
   predicate marks(LocalScopeVariable v, ControlFlowNode n) {
     v.getAnAccess().getEnclosingFunction().getBlock() = n and
     this.isDefault()
@@ -57,6 +69,10 @@ abstract class DataflowAnnotation extends string {
     )
   }
 
+  /**
+   * Holds if the variable `v` preserves this annotation when the control-flow
+   * edge `(src, dest)` is taken.
+   */
   predicate preservedBy(LocalScopeVariable v, ControlFlowNode src, ControlFlowNode dest) {
     this.marks(v, src) and
     src.getASuccessor() = dest and
@@ -64,6 +80,10 @@ abstract class DataflowAnnotation extends string {
     not v.getAnAssignment() = src
   }
 
+  /**
+   * Holds if the variable `v` is assigned this annotation when `src` is an assignment
+   * expression that assigns to `v` and the control-flow edge `(src, dest)` is taken.
+   */
   predicate assignedBy(LocalScopeVariable v, ControlFlowNode src, ControlFlowNode dest) {
     this.marks(src.(AssignExpr).getRValue()) and
     src = v.getAnAssignment() and