diff --git a/config/identical-files.json b/config/identical-files.json
index 709f78868eb..e57bf00ca23 100644
--- a/config/identical-files.json
+++ b/config/identical-files.json
@@ -82,6 +82,14 @@
     "cpp/ql/src/semmle/code/cpp/ir/implementation/IRType.qll",
     "csharp/ql/src/semmle/code/csharp/ir/implementation/IRType.qll"
   ],
+  "IR IRConfiguration": [
+    "cpp/ql/src/semmle/code/cpp/ir/implementation/IRConfiguration.qll",
+    "csharp/ql/src/semmle/code/csharp/ir/implementation/IRConfiguration.qll"
+  ],
+  "IR UseSoundEscapeAnalysis": [
+    "cpp/ql/src/semmle/code/cpp/ir/implementation/UseSoundEscapeAnalysis.qll",
+    "csharp/ql/src/semmle/code/csharp/ir/implementation/UseSoundEscapeAnalysis.qll"
+  ],
   "IR Operand Tag": [
     "cpp/ql/src/semmle/code/cpp/ir/implementation/internal/OperandTag.qll",
     "csharp/ql/src/semmle/code/csharp/ir/implementation/internal/OperandTag.qll"
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/IRConfiguration.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/IRConfiguration.qll
index c7133c21798..c0a489ef0c6 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/IRConfiguration.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/IRConfiguration.qll
@@ -1,3 +1,7 @@
+/**
+ * Module used to configure the IR generation process.
+ */
+
 private import internal.IRConfigurationInternal
 
 private newtype TIRConfiguration = MkIRConfiguration()
@@ -13,3 +17,18 @@ class IRConfiguration extends TIRConfiguration {
    */
   predicate shouldCreateIRForFunction(Language::Function func) { any() }
 }
+
+private newtype TIREscapeAnalysisConfiguration = MkIREscapeAnalysisConfiguration()
+
+/**
+ * The query can extend this class to control what escape analysis is used when generating SSA.
+ */
+class IREscapeAnalysisConfiguration extends TIREscapeAnalysisConfiguration {
+  string toString() { result = "IREscapeAnalysisConfiguration" }
+
+  /**
+   * Holds if the escape analysis done by SSA construction should be sound. By default, the SSA is
+   * built assuming that no variable's address ever escapes.
+   */
+  predicate useSoundEscapeAnalysis() { none() }
+}
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/UseSoundEscapeAnalysis.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/UseSoundEscapeAnalysis.qll
new file mode 100644
index 00000000000..b9b1dc243b1
--- /dev/null
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/UseSoundEscapeAnalysis.qll
@@ -0,0 +1,9 @@
+import IRConfiguration
+
+/**
+ * Overrides the default IR configuration to use sound escape analysis, instead of assuming that
+ * variable addresses never escape.
+ */
+class SoundEscapeAnalysisConfiguration extends IREscapeAnalysisConfiguration {
+  override predicate useSoundEscapeAnalysis() { any() }
+}
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll
index 18e449294f8..99f6b545806 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll
@@ -2,6 +2,7 @@ private import AliasAnalysisInternal
 private import cpp
 private import InputIR
 private import semmle.code.cpp.ir.internal.IntegerConstant as Ints
+private import semmle.code.cpp.ir.implementation.IRConfiguration
 private import semmle.code.cpp.models.interfaces.Alias
 
 private class IntValue = Ints::IntValue;
@@ -277,9 +278,14 @@ private predicate automaticVariableAddressEscapes(IRAutomaticVariable var) {
  * analysis.
  */
 predicate variableAddressEscapes(IRVariable var) {
-  automaticVariableAddressEscapes(var.(IRAutomaticVariable))
+  exists(IREscapeAnalysisConfiguration config |
+    config.useSoundEscapeAnalysis() and
+    automaticVariableAddressEscapes(var.(IRAutomaticVariable))
+  )
   or
-  // All variables with static storage duration have their address escape.
+  // All variables with static storage duration have their address escape, even when escape analysis
+  // is allowed to be unsound. Otherwise, we won't have a definition for any non-escaped global
+  // variable. Normally, we rely on `AliasedDefinition` to handle that.
   not var instanceof IRAutomaticVariable
 }
 
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll
index 23121523a6b..94470fe8584 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll
@@ -107,7 +107,7 @@ class PropertyProvider extends IRPropertyProvider {
     exists(
       MemoryLocation useLocation, IRBlock predBlock, IRBlock defBlock, int defIndex, Overlap overlap
     |
-      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex, overlap) and
+      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex) and
       key = "PhiUse[" + useLocation.toString() + " from " + predBlock.getDisplayIndex().toString() +
           "]" and
       result = defBlock.getDisplayIndex().toString() + "_" + defIndex + " (" + overlap.toString() +
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
index 87fd781fd95..fa2d3da59a4 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
@@ -43,93 +43,34 @@ abstract class TranslatedDeclarationEntry extends TranslatedElement, TTranslated
  * Represents the IR translation of the declaration of a local variable,
  * including its initialization, if any.
  */
-abstract class TranslatedVariableDeclaration extends TranslatedElement, InitializationContext {
+abstract class TranslatedLocalVariableDeclaration extends TranslatedVariableInitialization {
   /**
    * Gets the local variable being declared.
    */
   abstract LocalVariable getVariable();
 
-  override TranslatedElement getChild(int id) { id = 0 and result = getInitialization() }
+  final override Type getTargetType() { result = getVariableType(getVariable()) }
 
-  override Instruction getFirstInstruction() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
-  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
-    tag = InitializerVariableAddressTag() and
-    opcode instanceof Opcode::VariableAddress and
-    resultType = getTypeForGLValue(getVariableType(getVariable()))
-    or
-    hasUninitializedInstruction() and
-    tag = InitializerStoreTag() and
-    opcode instanceof Opcode::Uninitialized and
-    resultType = getTypeForPRValue(getVariableType(getVariable()))
-  }
-
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
-    (
-      tag = InitializerVariableAddressTag() and
-      kind instanceof GotoEdge and
-      if hasUninitializedInstruction()
-      then result = getInstruction(InitializerStoreTag())
-      else result = getInitialization().getFirstInstruction()
-    )
-    or
-    hasUninitializedInstruction() and
-    kind instanceof GotoEdge and
-    tag = InitializerStoreTag() and
-    (
-      result = getInitialization().getFirstInstruction()
-      or
-      not exists(getInitialization()) and result = getParent().getChildSuccessor(this)
-    )
-  }
-
-  override Instruction getChildSuccessor(TranslatedElement child) {
-    child = getInitialization() and result = getParent().getChildSuccessor(this)
-  }
-
-  override IRVariable getInstructionVariable(InstructionTag tag) {
-    (
-      tag = InitializerVariableAddressTag()
-      or
-      hasUninitializedInstruction() and tag = InitializerStoreTag()
-    ) and
-    result = getIRUserVariable(getFunction(), getVariable())
-  }
-
-  override Instruction getInstructionOperand(InstructionTag tag, OperandTag operandTag) {
-    hasUninitializedInstruction() and
-    tag = InitializerStoreTag() and
-    operandTag instanceof AddressOperandTag and
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
-  override Instruction getTargetAddress() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
-  override Type getTargetType() { result = getVariableType(getVariable()) }
-
-  private TranslatedInitialization getInitialization() {
+  final override TranslatedInitialization getInitialization() {
     result = getTranslatedInitialization(getVariable()
             .getInitializer()
             .getExpr()
             .getFullyConverted())
   }
 
-  private predicate hasUninitializedInstruction() {
-    not exists(getInitialization()) or
-    getInitialization() instanceof TranslatedListInitialization or
-    getInitialization() instanceof TranslatedConstructorInitialization or
-    getInitialization().(TranslatedStringLiteralInitialization).zeroInitRange(_, _)
+  final override Instruction getInitializationSuccessor() {
+    result = getParent().getChildSuccessor(this)
+  }
+
+  final override IRVariable getIRVariable() {
+    result = getIRUserVariable(getFunction(), getVariable())
   }
 }
 
 /**
  * Represents the IR translation of a local variable declaration within a declaration statement.
  */
-class TranslatedVariableDeclarationEntry extends TranslatedVariableDeclaration,
+class TranslatedVariableDeclarationEntry extends TranslatedLocalVariableDeclaration,
   TranslatedDeclarationEntry {
   LocalVariable var;
 
@@ -151,7 +92,7 @@ TranslatedRangeBasedForVariableDeclaration getTranslatedRangeBasedForVariableDec
 /**
  * Represents the IR translation of a compiler-generated variable in a range-based `for` loop.
  */
-class TranslatedRangeBasedForVariableDeclaration extends TranslatedVariableDeclaration,
+class TranslatedRangeBasedForVariableDeclaration extends TranslatedLocalVariableDeclaration,
   TTranslatedRangeBasedForVariableDeclaration {
   RangeBasedForStmt forStmt;
   LocalVariable var;
@@ -181,7 +122,7 @@ TranslatedConditionDecl getTranslatedConditionDecl(ConditionDeclExpr expr) {
  * }
  * ```
  */
-class TranslatedConditionDecl extends TranslatedVariableDeclaration, TTranslatedConditionDecl {
+class TranslatedConditionDecl extends TranslatedLocalVariableDeclaration, TTranslatedConditionDecl {
   ConditionDeclExpr conditionDeclExpr;
 
   TranslatedConditionDecl() { this = TTranslatedConditionDecl(conditionDeclExpr) }
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 9db42c742ac..84e3802c4a5 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -1932,40 +1932,22 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
  * IR translation of a `throw` expression with an argument
  * (e.g. `throw std::bad_alloc()`).
  */
-class TranslatedThrowValueExpr extends TranslatedThrowExpr, InitializationContext {
+class TranslatedThrowValueExpr extends TranslatedThrowExpr, TranslatedVariableInitialization {
   TranslatedThrowValueExpr() { not expr instanceof ReThrowExpr }
 
-  override TranslatedElement getChild(int id) { id = 0 and result = getInitialization() }
-
-  override Instruction getFirstInstruction() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     TranslatedThrowExpr.super.hasInstruction(opcode, tag, resultType)
     or
-    tag = InitializerVariableAddressTag() and
-    opcode instanceof Opcode::VariableAddress and
-    resultType = getTypeForGLValue(getExceptionType())
+    TranslatedVariableInitialization.super.hasInstruction(opcode, tag, resultType)
   }
 
   override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
     result = TranslatedThrowExpr.super.getInstructionSuccessor(tag, kind)
     or
-    tag = InitializerVariableAddressTag() and
-    result = getInitialization().getFirstInstruction() and
-    kind instanceof GotoEdge
+    result = TranslatedVariableInitialization.super.getInstructionSuccessor(tag, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child) {
-    child = getInitialization() and
-    result = getInstruction(ThrowTag())
-  }
-
-  override IRVariable getInstructionVariable(InstructionTag tag) {
-    tag = InitializerVariableAddressTag() and
-    result = getIRTempVariable(expr, ThrowTempVar())
-  }
+  final override Instruction getInitializationSuccessor() { result = getInstruction(ThrowTag()) }
 
   final override predicate hasTempVariable(TempVariableTag tag, CppType type) {
     tag = ThrowTempVar() and
@@ -1973,6 +1955,8 @@ class TranslatedThrowValueExpr extends TranslatedThrowExpr, InitializationContex
   }
 
   final override Instruction getInstructionOperand(InstructionTag tag, OperandTag operandTag) {
+    result = TranslatedVariableInitialization.super.getInstructionOperand(tag, operandTag)
+    or
     tag = ThrowTag() and
     (
       operandTag instanceof AddressOperandTag and
@@ -1989,16 +1973,14 @@ class TranslatedThrowValueExpr extends TranslatedThrowExpr, InitializationContex
     result = getTypeForPRValue(getExceptionType())
   }
 
-  override Instruction getTargetAddress() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
   override Type getTargetType() { result = getExceptionType() }
 
-  TranslatedInitialization getInitialization() {
+  final override TranslatedInitialization getInitialization() {
     result = getTranslatedInitialization(expr.getExpr().getFullyConverted())
   }
 
+  final override IRVariable getIRVariable() { result = getIRTempVariable(expr, ThrowTempVar()) }
+
   final override Opcode getThrowOpcode() { result instanceof Opcode::ThrowValue }
 
   private Type getExceptionType() { result = expr.getType() }
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 609f8276640..4c86f0b8194 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -30,6 +30,98 @@ abstract class InitializationContext extends TranslatedElement {
   abstract Type getTargetType();
 }
 
+/**
+ * Base class for any element that initializes a stack variable. Examples include local variable
+ * declarations, `return` statements, and `throw` expressions.
+ */
+abstract class TranslatedVariableInitialization extends TranslatedElement, InitializationContext {
+  final override TranslatedElement getChild(int id) { id = 0 and result = getInitialization() }
+
+  final override Instruction getFirstInstruction() {
+    result = getInstruction(InitializerVariableAddressTag())
+  }
+
+  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
+    tag = InitializerVariableAddressTag() and
+    opcode instanceof Opcode::VariableAddress and
+    resultType = getTypeForGLValue(getTargetType())
+    or
+    hasUninitializedInstruction() and
+    tag = InitializerStoreTag() and
+    opcode instanceof Opcode::Uninitialized and
+    resultType = getTypeForPRValue(getTargetType())
+  }
+
+  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+    (
+      tag = InitializerVariableAddressTag() and
+      kind instanceof GotoEdge and
+      if hasUninitializedInstruction()
+      then result = getInstruction(InitializerStoreTag())
+      else result = getInitialization().getFirstInstruction()
+    )
+    or
+    hasUninitializedInstruction() and
+    kind instanceof GotoEdge and
+    tag = InitializerStoreTag() and
+    (
+      result = getInitialization().getFirstInstruction()
+      or
+      not exists(getInitialization()) and result = getInitializationSuccessor()
+    )
+  }
+
+  final override Instruction getChildSuccessor(TranslatedElement child) {
+    child = getInitialization() and result = getInitializationSuccessor()
+  }
+
+  override Instruction getInstructionOperand(InstructionTag tag, OperandTag operandTag) {
+    hasUninitializedInstruction() and
+    tag = InitializerStoreTag() and
+    operandTag instanceof AddressOperandTag and
+    result = getInstruction(InitializerVariableAddressTag())
+  }
+
+  final override IRVariable getInstructionVariable(InstructionTag tag) {
+    (
+      tag = InitializerVariableAddressTag()
+      or
+      hasUninitializedInstruction() and tag = InitializerStoreTag()
+    ) and
+    result = getIRVariable()
+  }
+
+  final override Instruction getTargetAddress() {
+    result = getInstruction(InitializerVariableAddressTag())
+  }
+
+  /**
+   * Get the initialization for the variable.
+   */
+  abstract TranslatedInitialization getInitialization();
+
+  /**
+   * Get the `IRVariable` to be initialized. This may be an `IRTempVariable`.
+   */
+  abstract IRVariable getIRVariable();
+
+  /**
+   * Gets the `Instruction` to be executed immediately after the initialization.
+   */
+  abstract Instruction getInitializationSuccessor();
+
+  /**
+   * Holds if this initialization requires an `Uninitialized` instruction to be emitted before
+   * evaluating the initializer.
+   */
+  final predicate hasUninitializedInstruction() {
+    not exists(getInitialization()) or
+    getInitialization() instanceof TranslatedListInitialization or
+    getInitialization() instanceof TranslatedConstructorInitialization or
+    getInitialization().(TranslatedStringLiteralInitialization).zeroInitRange(_, _)
+  }
+}
+
 /**
  * Represents the IR translation of any initialization, whether from an
  * initializer list or from a direct initializer.
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index 62cbba8604b..8bb5961248f 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -130,46 +130,20 @@ abstract class TranslatedReturnStmt extends TranslatedStmt {
   }
 }
 
-class TranslatedReturnValueStmt extends TranslatedReturnStmt, InitializationContext {
+class TranslatedReturnValueStmt extends TranslatedReturnStmt, TranslatedVariableInitialization {
   TranslatedReturnValueStmt() { stmt.hasExpr() }
 
-  override TranslatedElement getChild(int id) { id = 0 and result = getInitialization() }
-
-  override Instruction getFirstInstruction() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
-  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
-    tag = InitializerVariableAddressTag() and
-    opcode instanceof Opcode::VariableAddress and
-    resultType = getTypeForGLValue(getEnclosingFunction().getReturnType())
-  }
-
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
-    tag = InitializerVariableAddressTag() and
-    result = getInitialization().getFirstInstruction() and
-    kind instanceof GotoEdge
-  }
-
-  override Instruction getChildSuccessor(TranslatedElement child) {
-    child = getInitialization() and
+  final override Instruction getInitializationSuccessor() {
     result = getEnclosingFunction().getReturnSuccessorInstruction()
   }
 
-  override IRVariable getInstructionVariable(InstructionTag tag) {
-    tag = InitializerVariableAddressTag() and
-    result = getEnclosingFunction().getReturnVariable()
-  }
+  final override Type getTargetType() { result = getEnclosingFunction().getReturnType() }
 
-  override Instruction getTargetAddress() {
-    result = getInstruction(InitializerVariableAddressTag())
-  }
-
-  override Type getTargetType() { result = getEnclosingFunction().getReturnType() }
-
-  TranslatedInitialization getInitialization() {
+  final override TranslatedInitialization getInitialization() {
     result = getTranslatedInitialization(stmt.getExpr().getFullyConverted())
   }
+
+  final override IRVariable getIRVariable() { result = getEnclosingFunction().getReturnVariable() }
 }
 
 class TranslatedReturnVoidStmt extends TranslatedReturnStmt {
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll
index 18e449294f8..99f6b545806 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll
@@ -2,6 +2,7 @@ private import AliasAnalysisInternal
 private import cpp
 private import InputIR
 private import semmle.code.cpp.ir.internal.IntegerConstant as Ints
+private import semmle.code.cpp.ir.implementation.IRConfiguration
 private import semmle.code.cpp.models.interfaces.Alias
 
 private class IntValue = Ints::IntValue;
@@ -277,9 +278,14 @@ private predicate automaticVariableAddressEscapes(IRAutomaticVariable var) {
  * analysis.
  */
 predicate variableAddressEscapes(IRVariable var) {
-  automaticVariableAddressEscapes(var.(IRAutomaticVariable))
+  exists(IREscapeAnalysisConfiguration config |
+    config.useSoundEscapeAnalysis() and
+    automaticVariableAddressEscapes(var.(IRAutomaticVariable))
+  )
   or
-  // All variables with static storage duration have their address escape.
+  // All variables with static storage duration have their address escape, even when escape analysis
+  // is allowed to be unsound. Otherwise, we won't have a definition for any non-escaped global
+  // variable. Normally, we rely on `AliasedDefinition` to handle that.
   not var instanceof IRAutomaticVariable
 }
 
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
index 23121523a6b..94470fe8584 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
@@ -107,7 +107,7 @@ class PropertyProvider extends IRPropertyProvider {
     exists(
       MemoryLocation useLocation, IRBlock predBlock, IRBlock defBlock, int defIndex, Overlap overlap
     |
-      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex, overlap) and
+      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex) and
       key = "PhiUse[" + useLocation.toString() + " from " + predBlock.getDisplayIndex().toString() +
           "]" and
       result = defBlock.getDisplayIndex().toString() + "_" + defIndex + " (" + overlap.toString() +
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_diff.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_diff.expected
index 716212bf449..e40505722af 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_diff.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_diff.expected
@@ -1,7 +1,6 @@
 | BarrierGuard.cpp:60:11:60:16 | BarrierGuard.cpp:62:14:62:14 | AST only |
 | BarrierGuard.cpp:60:11:60:16 | BarrierGuard.cpp:64:14:64:14 | AST only |
 | BarrierGuard.cpp:60:11:60:16 | BarrierGuard.cpp:66:14:66:14 | AST only |
-| clang.cpp:12:9:12:20 | clang.cpp:18:8:18:19 | AST only |
 | clang.cpp:12:9:12:20 | clang.cpp:22:8:22:20 | AST only |
 | clang.cpp:28:27:28:32 | clang.cpp:29:27:29:28 | AST only |
 | clang.cpp:28:27:28:32 | clang.cpp:30:27:30:34 | AST only |
@@ -24,7 +23,6 @@
 | lambdas.cpp:8:10:8:15 | lambdas.cpp:18:8:18:8 | AST only |
 | lambdas.cpp:8:10:8:15 | lambdas.cpp:21:3:21:6 | AST only |
 | lambdas.cpp:8:10:8:15 | lambdas.cpp:29:3:29:6 | AST only |
-| lambdas.cpp:8:10:8:15 | lambdas.cpp:35:8:35:8 | AST only |
 | lambdas.cpp:8:10:8:15 | lambdas.cpp:41:8:41:8 | AST only |
 | lambdas.cpp:43:7:43:12 | lambdas.cpp:46:7:46:7 | AST only |
 | ref.cpp:29:11:29:16 | ref.cpp:62:10:62:11 | AST only |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_ir.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_ir.expected
index 25edb3e5b7d..0e67184f477 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_ir.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test_ir.expected
@@ -7,6 +7,8 @@
 | BarrierGuard.cpp:55:13:55:13 | x | BarrierGuard.cpp:49:10:49:15 | call to source |
 | acrossLinkTargets.cpp:12:8:12:8 | (int)... | acrossLinkTargets.cpp:19:27:19:32 | call to source |
 | acrossLinkTargets.cpp:12:8:12:8 | x | acrossLinkTargets.cpp:19:27:19:32 | call to source |
+| clang.cpp:18:8:18:19 | (const int *)... | clang.cpp:12:9:12:20 | sourceArray1 |
+| clang.cpp:18:8:18:19 | sourceArray1 | clang.cpp:12:9:12:20 | sourceArray1 |
 | clang.cpp:37:10:37:11 | m2 | clang.cpp:34:32:34:37 | call to source |
 | clang.cpp:41:18:41:19 | m2 | clang.cpp:39:42:39:47 | call to source |
 | clang.cpp:45:17:45:18 | m2 | clang.cpp:43:35:43:40 | call to source |
@@ -30,6 +32,7 @@
 | dispatch.cpp:96:8:96:8 | x | dispatch.cpp:107:17:107:22 | call to source |
 | dispatch.cpp:96:8:96:8 | x | dispatch.cpp:140:8:140:13 | call to source |
 | dispatch.cpp:96:8:96:8 | x | dispatch.cpp:144:8:144:13 | call to source |
+| lambdas.cpp:35:8:35:8 | a | lambdas.cpp:8:10:8:15 | call to source |
 | test.cpp:7:8:7:9 | t1 | test.cpp:6:12:6:17 | call to source |
 | test.cpp:9:8:9:9 | t1 | test.cpp:6:12:6:17 | call to source |
 | test.cpp:10:8:10:9 | t2 | test.cpp:6:12:6:17 | call to source |
diff --git a/cpp/ql/test/library-tests/dataflow/taint-tests/test_diff.expected b/cpp/ql/test/library-tests/dataflow/taint-tests/test_diff.expected
index 9354f098533..1d875493db0 100644
--- a/cpp/ql/test/library-tests/dataflow/taint-tests/test_diff.expected
+++ b/cpp/ql/test/library-tests/dataflow/taint-tests/test_diff.expected
@@ -13,13 +13,11 @@
 | taint.cpp:181:8:181:9 | taint.cpp:185:11:185:16 | AST only |
 | taint.cpp:195:7:195:7 | taint.cpp:192:23:192:28 | AST only |
 | taint.cpp:195:7:195:7 | taint.cpp:193:6:193:6 | AST only |
-| taint.cpp:215:7:215:7 | taint.cpp:207:6:207:11 | AST only |
 | taint.cpp:216:7:216:7 | taint.cpp:207:6:207:11 | AST only |
 | taint.cpp:229:3:229:6 | taint.cpp:223:10:223:15 | AST only |
 | taint.cpp:233:8:233:8 | taint.cpp:223:10:223:15 | AST only |
 | taint.cpp:236:3:236:6 | taint.cpp:223:10:223:15 | AST only |
 | taint.cpp:244:3:244:6 | taint.cpp:223:10:223:15 | AST only |
-| taint.cpp:250:8:250:8 | taint.cpp:223:10:223:15 | AST only |
 | taint.cpp:256:8:256:8 | taint.cpp:223:10:223:15 | AST only |
 | taint.cpp:261:7:261:7 | taint.cpp:258:7:258:12 | AST only |
 | taint.cpp:351:7:351:7 | taint.cpp:330:6:330:11 | AST only |
@@ -31,7 +29,6 @@
 | taint.cpp:423:7:423:7 | taint.cpp:422:14:422:19 | AST only |
 | taint.cpp:424:9:424:17 | taint.cpp:422:14:422:19 | AST only |
 | taint.cpp:429:7:429:7 | taint.cpp:428:13:428:18 | IR only |
-| taint.cpp:430:9:430:14 | taint.cpp:428:13:428:18 | AST only |
 | taint.cpp:438:7:438:7 | taint.cpp:437:15:437:20 | AST only |
 | taint.cpp:439:10:439:18 | taint.cpp:437:15:437:20 | AST only |
 | taint.cpp:446:7:446:7 | taint.cpp:445:14:445:28 | AST only |
diff --git a/cpp/ql/test/library-tests/dataflow/taint-tests/test_ir.expected b/cpp/ql/test/library-tests/dataflow/taint-tests/test_ir.expected
index 258a2cca7c5..06010367fd7 100644
--- a/cpp/ql/test/library-tests/dataflow/taint-tests/test_ir.expected
+++ b/cpp/ql/test/library-tests/dataflow/taint-tests/test_ir.expected
@@ -9,6 +9,8 @@
 | taint.cpp:167:8:167:13 | call to source | taint.cpp:167:8:167:13 | call to source |
 | taint.cpp:168:8:168:14 | tainted | taint.cpp:164:19:164:24 | call to source |
 | taint.cpp:210:7:210:7 | x | taint.cpp:207:6:207:11 | call to source |
+| taint.cpp:215:7:215:7 | x | taint.cpp:207:6:207:11 | call to source |
+| taint.cpp:250:8:250:8 | a | taint.cpp:223:10:223:15 | call to source |
 | taint.cpp:280:7:280:7 | t | taint.cpp:275:6:275:11 | call to source |
 | taint.cpp:289:7:289:7 | t | taint.cpp:275:6:275:11 | call to source |
 | taint.cpp:290:7:290:7 | x | taint.cpp:275:6:275:11 | call to source |
@@ -16,3 +18,4 @@
 | taint.cpp:337:7:337:7 | t | taint.cpp:330:6:330:11 | call to source |
 | taint.cpp:350:7:350:7 | t | taint.cpp:330:6:330:11 | call to source |
 | taint.cpp:429:7:429:7 | b | taint.cpp:428:13:428:18 | call to source |
+| taint.cpp:430:9:430:14 | member | taint.cpp:428:13:428:18 | call to source |
diff --git a/cpp/ql/test/library-tests/ir/escape/escape.ql b/cpp/ql/test/library-tests/ir/escape/escape.ql
index 25475252d49..109ff260b7d 100644
--- a/cpp/ql/test/library-tests/ir/escape/escape.ql
+++ b/cpp/ql/test/library-tests/ir/escape/escape.ql
@@ -1,6 +1,7 @@
 import default
 import semmle.code.cpp.ir.implementation.unaliased_ssa.internal.AliasAnalysis
 import semmle.code.cpp.ir.implementation.raw.IR
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
 
 predicate shouldEscape(IRAutomaticUserVariable var) {
   exists(string name |
diff --git a/cpp/ql/test/library-tests/ir/escape/ssa_escape.ql b/cpp/ql/test/library-tests/ir/escape/ssa_escape.ql
index 2ef33ae749f..8025a455fc9 100644
--- a/cpp/ql/test/library-tests/ir/escape/ssa_escape.ql
+++ b/cpp/ql/test/library-tests/ir/escape/ssa_escape.ql
@@ -1,6 +1,7 @@
 import default
 import semmle.code.cpp.ir.implementation.aliased_ssa.internal.AliasAnalysis
 import semmle.code.cpp.ir.implementation.unaliased_ssa.IR
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
 
 predicate shouldEscape(IRAutomaticUserVariable var) {
   exists(string name |
diff --git a/cpp/ql/test/library-tests/ir/ir/PrintAST.expected b/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
index aa56b05163f..7778ebb76c0 100644
--- a/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
+++ b/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
@@ -8056,6 +8056,20 @@ ir.cpp:
 # 1166|       0: [VariableAccess] y
 # 1166|           Type = [IntType] int
 # 1166|           ValueCategory = prvalue(load)
+# 1169| [TopLevelFunction] String ReturnObjectImpl()
+# 1169|   params: 
+# 1169|   body: [Block] { ... }
+# 1170|     0: [ReturnStmt] return ...
+# 1170|       0: [ConstructorCall] call to String
+# 1170|           Type = [Struct] String
+# 1170|           ValueCategory = prvalue
+# 1170|         0: [ArrayToPointerConversion] array to pointer conversion
+# 1170|             Type = [PointerType] const char *
+# 1170|             ValueCategory = prvalue
+# 1170|           expr: foo
+# 1170|               Type = [ArrayType] const char[4]
+# 1170|               Value = [StringLiteral] "foo"
+# 1170|               ValueCategory = lvalue
 perf-regression.cpp:
 #    4| [CopyAssignmentOperator] Big& Big::operator=(Big const&)
 #    4|   params: 
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.ql
new file mode 100644
index 00000000000..74fa11944a6
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.aliased_ssa.IRSanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..e5e666c020b
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.expected
@@ -0,0 +1,26 @@
+missingOperand
+| ir.cpp:809:7:809:13 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:810:7:810:26 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:823:7:823:13 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:824:7:824:26 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+unexpectedOperand
+duplicateOperand
+missingPhiOperand
+missingOperandType
+duplicateChiOperand
+sideEffectWithoutPrimary
+instructionWithoutSuccessor
+ambiguousSuccessors
+unexplainedLoop
+unnecessaryPhiInstruction
+operandAcrossFunctions
+instructionWithoutUniqueBlock
+containsLoopOfForwardEdges
+lostReachability
+backEdgeCountMismatch
+useNotDominatedByDefinition
+missingCanonicalLanguageType
+multipleCanonicalLanguageTypes
+missingIRType
+multipleIRTypes
+missingCppType
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity.ql
new file mode 100644
index 00000000000..b3962e34648
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.aliased_ssa.internal.SSASanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..7c2d1faf639
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity_unsound.expected
@@ -0,0 +1,2 @@
+multipleOperandMemoryLocations
+missingVirtualVariableForMemoryLocation
diff --git a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ir/aliased_ssa_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ir/ir.cpp b/cpp/ql/test/library-tests/ir/ir/ir.cpp
index 7ebd2e22aee..6989287d222 100644
--- a/cpp/ql/test/library-tests/ir/ir/ir.cpp
+++ b/cpp/ql/test/library-tests/ir/ir/ir.cpp
@@ -1166,4 +1166,8 @@ int ModeledCallTarget(int x) {
   return y;
 }
 
+String ReturnObjectImpl() {
+  return String("foo");
+}
+
 // semmle-extractor-options: -std=c++17 --clang
diff --git a/cpp/ql/test/library-tests/ir/ir/raw_ir.expected b/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
index 94c1a433eb8..2583f634374 100644
--- a/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
+++ b/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
@@ -3371,15 +3371,16 @@ ir.cpp:
 
 #  731|   Block 7
 #  731|     r731_11(glval<String>)   = VariableAddress[#throw731:19]   : 
-#  731|     r731_12(glval<unknown>)  = FunctionAddress[String]         : 
-#  731|     r731_13(glval<char[14]>) = StringConstant["String object"] : 
-#  731|     r731_14(char *)          = Convert                         : r731_13
-#  731|     v731_15(void)            = Call                            : func:r731_12, this:r731_11, 0:r731_14
-#  731|     mu731_16(unknown)        = ^CallSideEffect                 : ~mu724_3
-#  731|     mu731_17(String)         = ^IndirectMayWriteSideEffect[-1] : &:r731_11
-#  731|     v731_18(void)            = ^BufferReadSideEffect[0]        : &:r731_14, ~mu724_3
-#  731|     mu731_19(unknown)        = ^BufferMayWriteSideEffect[0]    : &:r731_14
-#  731|     v731_20(void)            = ThrowValue                      : &:r731_11, ~mu724_3
+#  731|     mu731_12(String)         = Uninitialized[#throw731:19]     : &:r731_11
+#  731|     r731_13(glval<unknown>)  = FunctionAddress[String]         : 
+#  731|     r731_14(glval<char[14]>) = StringConstant["String object"] : 
+#  731|     r731_15(char *)          = Convert                         : r731_14
+#  731|     v731_16(void)            = Call                            : func:r731_13, this:r731_11, 0:r731_15
+#  731|     mu731_17(unknown)        = ^CallSideEffect                 : ~mu724_3
+#  731|     mu731_18(String)         = ^IndirectMayWriteSideEffect[-1] : &:r731_11
+#  731|     v731_19(void)            = ^BufferReadSideEffect[0]        : &:r731_15, ~mu724_3
+#  731|     mu731_20(unknown)        = ^BufferMayWriteSideEffect[0]    : &:r731_15
+#  731|     v731_21(void)            = ThrowValue                      : &:r731_11, ~mu724_3
 #-----|   Exception -> Block 9
 
 #  733|   Block 8
@@ -3399,15 +3400,16 @@ ir.cpp:
 #  735|     r735_4(char *)         = Load                            : &:r735_2, ~mu735_3
 #  735|     mu735_5(unknown)       = InitializeIndirection[s]        : &:r735_4
 #  736|     r736_1(glval<String>)  = VariableAddress[#throw736:5]    : 
-#  736|     r736_2(glval<unknown>) = FunctionAddress[String]         : 
-#  736|     r736_3(glval<char *>)  = VariableAddress[s]              : 
-#  736|     r736_4(char *)         = Load                            : &:r736_3, ~mu724_3
-#  736|     v736_5(void)           = Call                            : func:r736_2, this:r736_1, 0:r736_4
-#  736|     mu736_6(unknown)       = ^CallSideEffect                 : ~mu724_3
-#  736|     mu736_7(String)        = ^IndirectMayWriteSideEffect[-1] : &:r736_1
-#  736|     v736_8(void)           = ^BufferReadSideEffect[0]        : &:r736_4, ~mu724_3
-#  736|     mu736_9(unknown)       = ^BufferMayWriteSideEffect[0]    : &:r736_4
-#  736|     v736_10(void)          = ThrowValue                      : &:r736_1, ~mu724_3
+#  736|     mu736_2(String)        = Uninitialized[#throw736:5]      : &:r736_1
+#  736|     r736_3(glval<unknown>) = FunctionAddress[String]         : 
+#  736|     r736_4(glval<char *>)  = VariableAddress[s]              : 
+#  736|     r736_5(char *)         = Load                            : &:r736_4, ~mu724_3
+#  736|     v736_6(void)           = Call                            : func:r736_3, this:r736_1, 0:r736_5
+#  736|     mu736_7(unknown)       = ^CallSideEffect                 : ~mu724_3
+#  736|     mu736_8(String)        = ^IndirectMayWriteSideEffect[-1] : &:r736_1
+#  736|     v736_9(void)           = ^BufferReadSideEffect[0]        : &:r736_5, ~mu724_3
+#  736|     mu736_10(unknown)      = ^BufferMayWriteSideEffect[0]    : &:r736_5
+#  736|     v736_11(void)          = ThrowValue                      : &:r736_1, ~mu724_3
 #-----|   Exception -> Block 2
 
 #  738|   Block 11
@@ -5728,15 +5730,16 @@ ir.cpp:
 
 # 1140|   Block 7
 # 1140|     r1140_11(glval<String>)   = VariableAddress[#throw1140:19]  : 
-# 1140|     r1140_12(glval<unknown>)  = FunctionAddress[String]         : 
-# 1140|     r1140_13(glval<char[14]>) = StringConstant["String object"] : 
-# 1140|     r1140_14(char *)          = Convert                         : r1140_13
-# 1140|     v1140_15(void)            = Call                            : func:r1140_12, this:r1140_11, 0:r1140_14
-# 1140|     mu1140_16(unknown)        = ^CallSideEffect                 : ~mu1133_3
-# 1140|     mu1140_17(String)         = ^IndirectMayWriteSideEffect[-1] : &:r1140_11
-# 1140|     v1140_18(void)            = ^BufferReadSideEffect[0]        : &:r1140_14, ~mu1133_3
-# 1140|     mu1140_19(unknown)        = ^BufferMayWriteSideEffect[0]    : &:r1140_14
-# 1140|     v1140_20(void)            = ThrowValue                      : &:r1140_11, ~mu1133_3
+# 1140|     mu1140_12(String)         = Uninitialized[#throw1140:19]    : &:r1140_11
+# 1140|     r1140_13(glval<unknown>)  = FunctionAddress[String]         : 
+# 1140|     r1140_14(glval<char[14]>) = StringConstant["String object"] : 
+# 1140|     r1140_15(char *)          = Convert                         : r1140_14
+# 1140|     v1140_16(void)            = Call                            : func:r1140_13, this:r1140_11, 0:r1140_15
+# 1140|     mu1140_17(unknown)        = ^CallSideEffect                 : ~mu1133_3
+# 1140|     mu1140_18(String)         = ^IndirectMayWriteSideEffect[-1] : &:r1140_11
+# 1140|     v1140_19(void)            = ^BufferReadSideEffect[0]        : &:r1140_15, ~mu1133_3
+# 1140|     mu1140_20(unknown)        = ^BufferMayWriteSideEffect[0]    : &:r1140_15
+# 1140|     v1140_21(void)            = ThrowValue                      : &:r1140_11, ~mu1133_3
 #-----|   Exception -> Block 9
 
 # 1142|   Block 8
@@ -5756,15 +5759,16 @@ ir.cpp:
 # 1144|     r1144_4(char *)         = Load                            : &:r1144_2, ~mu1144_3
 # 1144|     mu1144_5(unknown)       = InitializeIndirection[s]        : &:r1144_4
 # 1145|     r1145_1(glval<String>)  = VariableAddress[#throw1145:5]   : 
-# 1145|     r1145_2(glval<unknown>) = FunctionAddress[String]         : 
-# 1145|     r1145_3(glval<char *>)  = VariableAddress[s]              : 
-# 1145|     r1145_4(char *)         = Load                            : &:r1145_3, ~mu1133_3
-# 1145|     v1145_5(void)           = Call                            : func:r1145_2, this:r1145_1, 0:r1145_4
-# 1145|     mu1145_6(unknown)       = ^CallSideEffect                 : ~mu1133_3
-# 1145|     mu1145_7(String)        = ^IndirectMayWriteSideEffect[-1] : &:r1145_1
-# 1145|     v1145_8(void)           = ^BufferReadSideEffect[0]        : &:r1145_4, ~mu1133_3
-# 1145|     mu1145_9(unknown)       = ^BufferMayWriteSideEffect[0]    : &:r1145_4
-# 1145|     v1145_10(void)          = ThrowValue                      : &:r1145_1, ~mu1133_3
+# 1145|     mu1145_2(String)        = Uninitialized[#throw1145:5]     : &:r1145_1
+# 1145|     r1145_3(glval<unknown>) = FunctionAddress[String]         : 
+# 1145|     r1145_4(glval<char *>)  = VariableAddress[s]              : 
+# 1145|     r1145_5(char *)         = Load                            : &:r1145_4, ~mu1133_3
+# 1145|     v1145_6(void)           = Call                            : func:r1145_3, this:r1145_1, 0:r1145_5
+# 1145|     mu1145_7(unknown)       = ^CallSideEffect                 : ~mu1133_3
+# 1145|     mu1145_8(String)        = ^IndirectMayWriteSideEffect[-1] : &:r1145_1
+# 1145|     v1145_9(void)           = ^BufferReadSideEffect[0]        : &:r1145_5, ~mu1133_3
+# 1145|     mu1145_10(unknown)      = ^BufferMayWriteSideEffect[0]    : &:r1145_5
+# 1145|     v1145_11(void)          = ThrowValue                      : &:r1145_1, ~mu1133_3
 #-----|   Exception -> Block 2
 
 # 1147|   Block 11
@@ -5878,6 +5882,27 @@ ir.cpp:
 # 1163|     v1163_9(void)           = AliasedUse                         : ~mu1163_3
 # 1163|     v1163_10(void)          = ExitFunction                       : 
 
+# 1169| String ReturnObjectImpl()
+# 1169|   Block 0
+# 1169|     v1169_1(void)           = EnterFunction                   : 
+# 1169|     mu1169_2(unknown)       = AliasedDefinition               : 
+# 1169|     mu1169_3(unknown)       = UnmodeledDefinition             : 
+# 1170|     r1170_1(glval<String>)  = VariableAddress[#return]        : 
+# 1170|     mu1170_2(String)        = Uninitialized[#return]          : &:r1170_1
+# 1170|     r1170_3(glval<unknown>) = FunctionAddress[String]         : 
+# 1170|     r1170_4(glval<char[4]>) = StringConstant["foo"]           : 
+# 1170|     r1170_5(char *)         = Convert                         : r1170_4
+# 1170|     r1170_6(String)         = Call                            : func:r1170_3, this:r1170_1, 0:r1170_5
+# 1170|     mu1170_7(unknown)       = ^CallSideEffect                 : ~mu1169_3
+# 1170|     mu1170_8(String)        = ^IndirectMayWriteSideEffect[-1] : &:r1170_1
+# 1170|     v1170_9(void)           = ^BufferReadSideEffect[0]        : &:r1170_5, ~mu1169_3
+# 1170|     mu1170_10(unknown)      = ^BufferMayWriteSideEffect[0]    : &:r1170_5
+# 1169|     r1169_4(glval<String>)  = VariableAddress[#return]        : 
+# 1169|     v1169_5(void)           = ReturnValue                     : &:r1169_4, ~mu1169_3
+# 1169|     v1169_6(void)           = UnmodeledUse                    : mu*
+# 1169|     v1169_7(void)           = AliasedUse                      : ~mu1169_3
+# 1169|     v1169_8(void)           = ExitFunction                    : 
+
 perf-regression.cpp:
 #    6| void Big::Big()
 #    6|   Block 0
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.ql
new file mode 100644
index 00000000000..c7d0ba957af
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.unaliased_ssa.IRSanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..e5e666c020b
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.expected
@@ -0,0 +1,26 @@
+missingOperand
+| ir.cpp:809:7:809:13 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:810:7:810:26 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:823:7:823:13 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+| ir.cpp:824:7:824:26 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
+unexpectedOperand
+duplicateOperand
+missingPhiOperand
+missingOperandType
+duplicateChiOperand
+sideEffectWithoutPrimary
+instructionWithoutSuccessor
+ambiguousSuccessors
+unexplainedLoop
+unnecessaryPhiInstruction
+operandAcrossFunctions
+instructionWithoutUniqueBlock
+containsLoopOfForwardEdges
+lostReachability
+backEdgeCountMismatch
+useNotDominatedByDefinition
+missingCanonicalLanguageType
+multipleCanonicalLanguageTypes
+missingIRType
+multipleIRTypes
+missingCppType
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity.ql
new file mode 100644
index 00000000000..120881bf018
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.unaliased_ssa.internal.SSASanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..7c2d1faf639
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity_unsound.expected
@@ -0,0 +1,2 @@
+multipleOperandMemoryLocations
+missingVirtualVariableForMemoryLocation
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ir/unaliased_ssa_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.ql b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.ql
new file mode 100644
index 00000000000..d8b68d0d72e
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.ql
@@ -0,0 +1,6 @@
+/**
+ * @kind graph
+ */
+
+import semmle.code.cpp.ir.implementation.aliased_ssa.PrintIR
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.expected
new file mode 100644
index 00000000000..b1a174f2b0b
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.expected
@@ -0,0 +1,1085 @@
+ssa.cpp:
+#   13| int ChiPhiNode(Point*, bool, bool)
+#   13|   Block 0
+#   13|     v13_1(void)           = EnterFunction               : 
+#   13|     m13_2(unknown)        = AliasedDefinition           : 
+#   13|     mu13_3(unknown)       = UnmodeledDefinition         : 
+#   13|     r13_4(glval<Point *>) = VariableAddress[p]          : 
+#   13|     m13_5(Point *)        = InitializeParameter[p]      : &:r13_4
+#   13|     r13_6(Point *)        = Load                        : &:r13_4, m13_5
+#   13|     m13_7(unknown)        = InitializeIndirection[p]    : &:r13_6
+#   13|     m13_8(unknown)        = Chi                         : total:m13_2, partial:m13_7
+#   13|     r13_9(glval<bool>)    = VariableAddress[which1]     : 
+#   13|     m13_10(bool)          = InitializeParameter[which1] : &:r13_9
+#   13|     r13_11(glval<bool>)   = VariableAddress[which2]     : 
+#   13|     m13_12(bool)          = InitializeParameter[which2] : &:r13_11
+#   14|     r14_1(glval<bool>)    = VariableAddress[which1]     : 
+#   14|     r14_2(bool)           = Load                        : &:r14_1, m13_10
+#   14|     v14_3(void)           = ConditionalBranch           : r14_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   15|   Block 1
+#   15|     r15_1(glval<Point *>) = VariableAddress[p] : 
+#   15|     r15_2(Point *)        = Load               : &:r15_1, m13_5
+#   15|     r15_3(glval<int>)     = FieldAddress[x]    : r15_2
+#   15|     r15_4(int)            = Load               : &:r15_3, ~m13_8
+#   15|     r15_5(int)            = Constant[1]        : 
+#   15|     r15_6(int)            = Add                : r15_4, r15_5
+#   15|     m15_7(int)            = Store              : &:r15_3, r15_6
+#   15|     m15_8(unknown)        = Chi                : total:m13_8, partial:m15_7
+#-----|   Goto -> Block 3
+
+#   18|   Block 2
+#   18|     r18_1(glval<Point *>) = VariableAddress[p] : 
+#   18|     r18_2(Point *)        = Load               : &:r18_1, m13_5
+#   18|     r18_3(glval<int>)     = FieldAddress[y]    : r18_2
+#   18|     r18_4(int)            = Load               : &:r18_3, ~m13_8
+#   18|     r18_5(int)            = Constant[1]        : 
+#   18|     r18_6(int)            = Add                : r18_4, r18_5
+#   18|     m18_7(int)            = Store              : &:r18_3, r18_6
+#   18|     m18_8(unknown)        = Chi                : total:m13_8, partial:m18_7
+#-----|   Goto -> Block 3
+
+#   21|   Block 3
+#   21|     m21_1(unknown)     = Phi                     : from 1:~m15_8, from 2:~m18_8
+#   21|     r21_2(glval<bool>) = VariableAddress[which2] : 
+#   21|     r21_3(bool)        = Load                    : &:r21_2, m13_12
+#   21|     v21_4(void)        = ConditionalBranch       : r21_3
+#-----|   False -> Block 5
+#-----|   True -> Block 4
+
+#   22|   Block 4
+#   22|     r22_1(glval<Point *>) = VariableAddress[p] : 
+#   22|     r22_2(Point *)        = Load               : &:r22_1, m13_5
+#   22|     r22_3(glval<int>)     = FieldAddress[x]    : r22_2
+#   22|     r22_4(int)            = Load               : &:r22_3, ~m21_1
+#   22|     r22_5(int)            = Constant[1]        : 
+#   22|     r22_6(int)            = Add                : r22_4, r22_5
+#   22|     m22_7(int)            = Store              : &:r22_3, r22_6
+#   22|     m22_8(unknown)        = Chi                : total:m21_1, partial:m22_7
+#-----|   Goto -> Block 6
+
+#   25|   Block 5
+#   25|     r25_1(glval<Point *>) = VariableAddress[p] : 
+#   25|     r25_2(Point *)        = Load               : &:r25_1, m13_5
+#   25|     r25_3(glval<int>)     = FieldAddress[y]    : r25_2
+#   25|     r25_4(int)            = Load               : &:r25_3, ~m21_1
+#   25|     r25_5(int)            = Constant[1]        : 
+#   25|     r25_6(int)            = Add                : r25_4, r25_5
+#   25|     m25_7(int)            = Store              : &:r25_3, r25_6
+#   25|     m25_8(unknown)        = Chi                : total:m21_1, partial:m25_7
+#-----|   Goto -> Block 6
+
+#   28|   Block 6
+#   28|     m28_1(unknown)        = Phi                      : from 4:~m22_8, from 5:~m25_8
+#   28|     r28_2(glval<int>)     = VariableAddress[#return] : 
+#   28|     r28_3(glval<Point *>) = VariableAddress[p]       : 
+#   28|     r28_4(Point *)        = Load                     : &:r28_3, m13_5
+#   28|     r28_5(glval<int>)     = FieldAddress[x]          : r28_4
+#   28|     r28_6(int)            = Load                     : &:r28_5, ~m28_1
+#   28|     r28_7(glval<Point *>) = VariableAddress[p]       : 
+#   28|     r28_8(Point *)        = Load                     : &:r28_7, m13_5
+#   28|     r28_9(glval<int>)     = FieldAddress[y]          : r28_8
+#   28|     r28_10(int)           = Load                     : &:r28_9, ~m28_1
+#   28|     r28_11(int)           = Add                      : r28_6, r28_10
+#   28|     m28_12(int)           = Store                    : &:r28_2, r28_11
+#   13|     v13_13(void)          = ReturnIndirection        : &:r13_6, ~m28_1
+#   13|     r13_14(glval<int>)    = VariableAddress[#return] : 
+#   13|     v13_15(void)          = ReturnValue              : &:r13_14, m28_12
+#   13|     v13_16(void)          = UnmodeledUse             : mu*
+#   13|     v13_17(void)          = AliasedUse               : ~m28_1
+#   13|     v13_18(void)          = ExitFunction             : 
+
+#   31| int UnreachableViaGoto()
+#   31|   Block 0
+#   31|     v31_1(void)       = EnterFunction            : 
+#   31|     m31_2(unknown)    = AliasedDefinition        : 
+#   31|     mu31_3(unknown)   = UnmodeledDefinition      : 
+#   32|     v32_1(void)       = NoOp                     : 
+#   34|     v34_1(void)       = NoOp                     : 
+#   35|     r35_1(glval<int>) = VariableAddress[#return] : 
+#   35|     r35_2(int)        = Constant[0]              : 
+#   35|     m35_3(int)        = Store                    : &:r35_1, r35_2
+#   31|     r31_4(glval<int>) = VariableAddress[#return] : 
+#   31|     v31_5(void)       = ReturnValue              : &:r31_4, m35_3
+#   31|     v31_6(void)       = UnmodeledUse             : mu*
+#   31|     v31_7(void)       = AliasedUse               : ~m31_2
+#   31|     v31_8(void)       = ExitFunction             : 
+
+#   38| int UnreachableIf(bool)
+#   38|   Block 0
+#   38|     v38_1(void)        = EnterFunction          : 
+#   38|     m38_2(unknown)     = AliasedDefinition      : 
+#   38|     mu38_3(unknown)    = UnmodeledDefinition    : 
+#   38|     r38_4(glval<bool>) = VariableAddress[b]     : 
+#   38|     m38_5(bool)        = InitializeParameter[b] : &:r38_4
+#   39|     r39_1(glval<int>)  = VariableAddress[x]     : 
+#   39|     r39_2(int)         = Constant[5]            : 
+#   39|     m39_3(int)         = Store                  : &:r39_1, r39_2
+#   40|     r40_1(glval<int>)  = VariableAddress[y]     : 
+#   40|     r40_2(int)         = Constant[10]           : 
+#   40|     m40_3(int)         = Store                  : &:r40_1, r40_2
+#   41|     r41_1(glval<bool>) = VariableAddress[b]     : 
+#   41|     r41_2(bool)        = Load                   : &:r41_1, m38_5
+#   41|     v41_3(void)        = ConditionalBranch      : r41_2
+#-----|   False -> Block 4
+#-----|   True -> Block 2
+
+#   38|   Block 1
+#   38|     m38_6(int)        = Phi                      : from 3:m46_3, from 5:m51_3
+#   38|     r38_7(glval<int>) = VariableAddress[#return] : 
+#   38|     v38_8(void)       = ReturnValue              : &:r38_7, m38_6
+#   38|     v38_9(void)       = UnmodeledUse             : mu*
+#   38|     v38_10(void)      = AliasedUse               : ~m38_2
+#   38|     v38_11(void)      = ExitFunction             : 
+
+#   42|   Block 2
+#   42|     r42_1(glval<int>) = VariableAddress[x] : 
+#   42|     r42_2(int)        = Load               : &:r42_1, m39_3
+#   42|     r42_3(glval<int>) = VariableAddress[y] : 
+#   42|     r42_4(int)        = Load               : &:r42_3, m40_3
+#   42|     r42_5(bool)       = CompareEQ          : r42_2, r42_4
+#   42|     v42_6(void)       = ConditionalBranch  : r42_5
+#-----|   False -> Block 3
+#-----|   True -> Block 6
+
+#   46|   Block 3
+#   46|     r46_1(glval<int>) = VariableAddress[#return] : 
+#   46|     r46_2(int)        = Constant[0]              : 
+#   46|     m46_3(int)        = Store                    : &:r46_1, r46_2
+#-----|   Goto -> Block 1
+
+#   50|   Block 4
+#   50|     r50_1(glval<int>) = VariableAddress[x] : 
+#   50|     r50_2(int)        = Load               : &:r50_1, m39_3
+#   50|     r50_3(glval<int>) = VariableAddress[y] : 
+#   50|     r50_4(int)        = Load               : &:r50_3, m40_3
+#   50|     r50_5(bool)       = CompareLT          : r50_2, r50_4
+#   50|     v50_6(void)       = ConditionalBranch  : r50_5
+#-----|   False -> Block 6
+#-----|   True -> Block 5
+
+#   51|   Block 5
+#   51|     r51_1(glval<int>) = VariableAddress[#return] : 
+#   51|     r51_2(int)        = Constant[0]              : 
+#   51|     m51_3(int)        = Store                    : &:r51_1, r51_2
+#-----|   Goto -> Block 1
+
+#   38|   Block 6
+#   38|     v38_12(void) = Unreached : 
+
+#   59| int DoWhileFalse()
+#   59|   Block 0
+#   59|     v59_1(void)       = EnterFunction       : 
+#   59|     m59_2(unknown)    = AliasedDefinition   : 
+#   59|     mu59_3(unknown)   = UnmodeledDefinition : 
+#   60|     r60_1(glval<int>) = VariableAddress[i]  : 
+#   60|     r60_2(int)        = Constant[0]         : 
+#   60|     m60_3(int)        = Store               : &:r60_1, r60_2
+#   62|     r62_1(glval<int>) = VariableAddress[i]  : 
+#   62|     r62_2(int)        = Load                : &:r62_1, m60_3
+#   62|     r62_3(int)        = Constant[1]         : 
+#   62|     r62_4(int)        = Add                 : r62_2, r62_3
+#   62|     m62_5(int)        = Store               : &:r62_1, r62_4
+#   63|     r63_1(bool)       = Constant[0]         : 
+#   63|     v63_2(void)       = ConditionalBranch   : r63_1
+#-----|   False -> Block 1
+#-----|   True -> Block 2
+
+#   65|   Block 1
+#   65|     r65_1(glval<int>) = VariableAddress[#return] : 
+#   65|     r65_2(glval<int>) = VariableAddress[i]       : 
+#   65|     r65_3(int)        = Load                     : &:r65_2, m62_5
+#   65|     m65_4(int)        = Store                    : &:r65_1, r65_3
+#   59|     r59_4(glval<int>) = VariableAddress[#return] : 
+#   59|     v59_5(void)       = ReturnValue              : &:r59_4, m65_4
+#   59|     v59_6(void)       = UnmodeledUse             : mu*
+#   59|     v59_7(void)       = AliasedUse               : ~m59_2
+#   59|     v59_8(void)       = ExitFunction             : 
+
+#   59|   Block 2
+#   59|     v59_9(void) = Unreached : 
+
+#   68| void chiNodeAtEndOfLoop(int, char*)
+#   68|   Block 0
+#   68|     v68_1(void)          = EnterFunction            : 
+#   68|     m68_2(unknown)       = AliasedDefinition        : 
+#   68|     mu68_3(unknown)      = UnmodeledDefinition      : 
+#   68|     r68_4(glval<int>)    = VariableAddress[n]       : 
+#   68|     m68_5(int)           = InitializeParameter[n]   : &:r68_4
+#   68|     r68_6(glval<char *>) = VariableAddress[p]       : 
+#   68|     m68_7(char *)        = InitializeParameter[p]   : &:r68_6
+#   68|     r68_8(char *)        = Load                     : &:r68_6, m68_7
+#   68|     m68_9(unknown)       = InitializeIndirection[p] : &:r68_8
+#   68|     m68_10(unknown)      = Chi                      : total:m68_2, partial:m68_9
+#-----|   Goto -> Block 3
+
+#   70|   Block 1
+#   70|     r70_1(char)          = Constant[0]        : 
+#   70|     r70_2(glval<char *>) = VariableAddress[p] : 
+#   70|     r70_3(char *)        = Load               : &:r70_2, m69_1
+#   70|     r70_4(int)           = Constant[1]        : 
+#   70|     r70_5(char *)        = PointerAdd[1]      : r70_3, r70_4
+#   70|     m70_6(char *)        = Store              : &:r70_2, r70_5
+#   70|     r70_7(glval<char>)   = CopyValue          : r70_3
+#   70|     m70_8(char)          = Store              : &:r70_7, r70_1
+#   70|     m70_9(unknown)       = Chi                : total:m69_3, partial:m70_8
+#-----|   Goto (back edge) -> Block 3
+
+#   71|   Block 2
+#   71|     v71_1(void)  = NoOp              : 
+#   68|     v68_11(void) = ReturnIndirection : &:r68_8, ~m69_3
+#   68|     v68_12(void) = ReturnVoid        : 
+#   68|     v68_13(void) = UnmodeledUse      : mu*
+#   68|     v68_14(void) = AliasedUse        : ~m69_3
+#   68|     v68_15(void) = ExitFunction      : 
+
+#   69|   Block 3
+#   69|     m69_1(char *)     = Phi                : from 0:m68_7, from 1:m70_6
+#   69|     m69_2(int)        = Phi                : from 0:m68_5, from 1:m69_8
+#   69|     m69_3(unknown)    = Phi                : from 0:~m68_10, from 1:~m70_9
+#   69|     r69_4(glval<int>) = VariableAddress[n] : 
+#   69|     r69_5(int)        = Load               : &:r69_4, m69_2
+#   69|     r69_6(int)        = Constant[1]        : 
+#   69|     r69_7(int)        = Sub                : r69_5, r69_6
+#   69|     m69_8(int)        = Store              : &:r69_4, r69_7
+#   69|     r69_9(int)        = Constant[0]        : 
+#   69|     r69_10(bool)      = CompareGT          : r69_5, r69_9
+#   69|     v69_11(void)      = ConditionalBranch  : r69_10
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   75| void ScalarPhi(bool)
+#   75|   Block 0
+#   75|     v75_1(void)        = EnterFunction          : 
+#   75|     m75_2(unknown)     = AliasedDefinition      : 
+#   75|     mu75_3(unknown)    = UnmodeledDefinition    : 
+#   75|     r75_4(glval<bool>) = VariableAddress[b]     : 
+#   75|     m75_5(bool)        = InitializeParameter[b] : &:r75_4
+#   76|     r76_1(glval<int>)  = VariableAddress[x]     : 
+#   76|     r76_2(int)         = Constant[0]            : 
+#   76|     m76_3(int)         = Store                  : &:r76_1, r76_2
+#   77|     r77_1(glval<int>)  = VariableAddress[y]     : 
+#   77|     r77_2(int)         = Constant[1]            : 
+#   77|     m77_3(int)         = Store                  : &:r77_1, r77_2
+#   78|     r78_1(glval<int>)  = VariableAddress[z]     : 
+#   78|     r78_2(int)         = Constant[2]            : 
+#   78|     m78_3(int)         = Store                  : &:r78_1, r78_2
+#   79|     r79_1(glval<bool>) = VariableAddress[b]     : 
+#   79|     r79_2(bool)        = Load                   : &:r79_1, m75_5
+#   79|     v79_3(void)        = ConditionalBranch      : r79_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   80|   Block 1
+#   80|     r80_1(int)        = Constant[3]        : 
+#   80|     r80_2(glval<int>) = VariableAddress[x] : 
+#   80|     m80_3(int)        = Store              : &:r80_2, r80_1
+#   81|     r81_1(int)        = Constant[4]        : 
+#   81|     r81_2(glval<int>) = VariableAddress[y] : 
+#   81|     m81_3(int)        = Store              : &:r81_2, r81_1
+#-----|   Goto -> Block 3
+
+#   84|   Block 2
+#   84|     r84_1(int)        = Constant[5]        : 
+#   84|     r84_2(glval<int>) = VariableAddress[x] : 
+#   84|     m84_3(int)        = Store              : &:r84_2, r84_1
+#-----|   Goto -> Block 3
+
+#   86|   Block 3
+#   86|     m86_1(int)        = Phi                      : from 1:m81_3, from 2:m77_3
+#   86|     m86_2(int)        = Phi                      : from 1:m80_3, from 2:m84_3
+#   86|     r86_3(glval<int>) = VariableAddress[x_merge] : 
+#   86|     r86_4(glval<int>) = VariableAddress[x]       : 
+#   86|     r86_5(int)        = Load                     : &:r86_4, m86_2
+#   86|     m86_6(int)        = Store                    : &:r86_3, r86_5
+#   87|     r87_1(glval<int>) = VariableAddress[y_merge] : 
+#   87|     r87_2(glval<int>) = VariableAddress[y]       : 
+#   87|     r87_3(int)        = Load                     : &:r87_2, m86_1
+#   87|     m87_4(int)        = Store                    : &:r87_1, r87_3
+#   88|     r88_1(glval<int>) = VariableAddress[z_merge] : 
+#   88|     r88_2(glval<int>) = VariableAddress[z]       : 
+#   88|     r88_3(int)        = Load                     : &:r88_2, m78_3
+#   88|     m88_4(int)        = Store                    : &:r88_1, r88_3
+#   89|     v89_1(void)       = NoOp                     : 
+#   75|     v75_6(void)       = ReturnVoid               : 
+#   75|     v75_7(void)       = UnmodeledUse             : mu*
+#   75|     v75_8(void)       = AliasedUse               : ~m75_2
+#   75|     v75_9(void)       = ExitFunction             : 
+
+#   91| void MustExactlyOverlap(Point)
+#   91|   Block 0
+#   91|     v91_1(void)         = EnterFunction          : 
+#   91|     m91_2(unknown)      = AliasedDefinition      : 
+#   91|     mu91_3(unknown)     = UnmodeledDefinition    : 
+#   91|     r91_4(glval<Point>) = VariableAddress[a]     : 
+#   91|     m91_5(Point)        = InitializeParameter[a] : &:r91_4
+#   92|     r92_1(glval<Point>) = VariableAddress[b]     : 
+#   92|     r92_2(glval<Point>) = VariableAddress[a]     : 
+#   92|     r92_3(Point)        = Load                   : &:r92_2, m91_5
+#   92|     m92_4(Point)        = Store                  : &:r92_1, r92_3
+#   93|     v93_1(void)         = NoOp                   : 
+#   91|     v91_6(void)         = ReturnVoid             : 
+#   91|     v91_7(void)         = UnmodeledUse           : mu*
+#   91|     v91_8(void)         = AliasedUse             : ~m91_2
+#   91|     v91_9(void)         = ExitFunction           : 
+
+#   95| void MustExactlyOverlapEscaped(Point)
+#   95|   Block 0
+#   95|     v95_1(void)           = EnterFunction                : 
+#   95|     m95_2(unknown)        = AliasedDefinition            : 
+#   95|     mu95_3(unknown)       = UnmodeledDefinition          : 
+#   95|     r95_4(glval<Point>)   = VariableAddress[a]           : 
+#   95|     m95_5(Point)          = InitializeParameter[a]       : &:r95_4
+#   96|     r96_1(glval<Point>)   = VariableAddress[b]           : 
+#   96|     r96_2(glval<Point>)   = VariableAddress[a]           : 
+#   96|     r96_3(Point)          = Load                         : &:r96_2, m95_5
+#   96|     m96_4(Point)          = Store                        : &:r96_1, r96_3
+#   97|     r97_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#   97|     r97_2(glval<Point>)   = VariableAddress[a]           : 
+#   97|     r97_3(Point *)        = CopyValue                    : r97_2
+#   97|     r97_4(void *)         = Convert                      : r97_3
+#   97|     v97_5(void)           = Call                         : func:r97_1, 0:r97_4
+#   97|     m97_6(unknown)        = ^CallSideEffect              : ~m95_2
+#   97|     m97_7(unknown)        = Chi                          : total:m95_2, partial:m97_6
+#   97|     v97_8(void)           = ^BufferReadSideEffect[0]     : &:r97_4, ~m95_5
+#   97|     m97_9(unknown)        = ^BufferMayWriteSideEffect[0] : &:r97_4
+#   97|     m97_10(Point)         = Chi                          : total:m95_5, partial:m97_9
+#   98|     v98_1(void)           = NoOp                         : 
+#   95|     v95_6(void)           = ReturnVoid                   : 
+#   95|     v95_7(void)           = UnmodeledUse                 : mu*
+#   95|     v95_8(void)           = AliasedUse                   : ~m97_7
+#   95|     v95_9(void)           = ExitFunction                 : 
+
+#  100| void MustTotallyOverlap(Point)
+#  100|   Block 0
+#  100|     v100_1(void)         = EnterFunction          : 
+#  100|     m100_2(unknown)      = AliasedDefinition      : 
+#  100|     mu100_3(unknown)     = UnmodeledDefinition    : 
+#  100|     r100_4(glval<Point>) = VariableAddress[a]     : 
+#  100|     m100_5(Point)        = InitializeParameter[a] : &:r100_4
+#  101|     r101_1(glval<int>)   = VariableAddress[x]     : 
+#  101|     r101_2(glval<Point>) = VariableAddress[a]     : 
+#  101|     r101_3(glval<int>)   = FieldAddress[x]        : r101_2
+#  101|     r101_4(int)          = Load                   : &:r101_3, ~m100_5
+#  101|     m101_5(int)          = Store                  : &:r101_1, r101_4
+#  102|     r102_1(glval<int>)   = VariableAddress[y]     : 
+#  102|     r102_2(glval<Point>) = VariableAddress[a]     : 
+#  102|     r102_3(glval<int>)   = FieldAddress[y]        : r102_2
+#  102|     r102_4(int)          = Load                   : &:r102_3, ~m100_5
+#  102|     m102_5(int)          = Store                  : &:r102_1, r102_4
+#  103|     v103_1(void)         = NoOp                   : 
+#  100|     v100_6(void)         = ReturnVoid             : 
+#  100|     v100_7(void)         = UnmodeledUse           : mu*
+#  100|     v100_8(void)         = AliasedUse             : ~m100_2
+#  100|     v100_9(void)         = ExitFunction           : 
+
+#  105| void MustTotallyOverlapEscaped(Point)
+#  105|   Block 0
+#  105|     v105_1(void)           = EnterFunction                : 
+#  105|     m105_2(unknown)        = AliasedDefinition            : 
+#  105|     mu105_3(unknown)       = UnmodeledDefinition          : 
+#  105|     r105_4(glval<Point>)   = VariableAddress[a]           : 
+#  105|     m105_5(Point)          = InitializeParameter[a]       : &:r105_4
+#  106|     r106_1(glval<int>)     = VariableAddress[x]           : 
+#  106|     r106_2(glval<Point>)   = VariableAddress[a]           : 
+#  106|     r106_3(glval<int>)     = FieldAddress[x]              : r106_2
+#  106|     r106_4(int)            = Load                         : &:r106_3, ~m105_5
+#  106|     m106_5(int)            = Store                        : &:r106_1, r106_4
+#  107|     r107_1(glval<int>)     = VariableAddress[y]           : 
+#  107|     r107_2(glval<Point>)   = VariableAddress[a]           : 
+#  107|     r107_3(glval<int>)     = FieldAddress[y]              : r107_2
+#  107|     r107_4(int)            = Load                         : &:r107_3, ~m105_5
+#  107|     m107_5(int)            = Store                        : &:r107_1, r107_4
+#  108|     r108_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#  108|     r108_2(glval<Point>)   = VariableAddress[a]           : 
+#  108|     r108_3(Point *)        = CopyValue                    : r108_2
+#  108|     r108_4(void *)         = Convert                      : r108_3
+#  108|     v108_5(void)           = Call                         : func:r108_1, 0:r108_4
+#  108|     m108_6(unknown)        = ^CallSideEffect              : ~m105_2
+#  108|     m108_7(unknown)        = Chi                          : total:m105_2, partial:m108_6
+#  108|     v108_8(void)           = ^BufferReadSideEffect[0]     : &:r108_4, ~m105_5
+#  108|     m108_9(unknown)        = ^BufferMayWriteSideEffect[0] : &:r108_4
+#  108|     m108_10(Point)         = Chi                          : total:m105_5, partial:m108_9
+#  109|     v109_1(void)           = NoOp                         : 
+#  105|     v105_6(void)           = ReturnVoid                   : 
+#  105|     v105_7(void)           = UnmodeledUse                 : mu*
+#  105|     v105_8(void)           = AliasedUse                   : ~m108_7
+#  105|     v105_9(void)           = ExitFunction                 : 
+
+#  111| void MayPartiallyOverlap(int, int)
+#  111|   Block 0
+#  111|     v111_1(void)         = EnterFunction          : 
+#  111|     m111_2(unknown)      = AliasedDefinition      : 
+#  111|     mu111_3(unknown)     = UnmodeledDefinition    : 
+#  111|     r111_4(glval<int>)   = VariableAddress[x]     : 
+#  111|     m111_5(int)          = InitializeParameter[x] : &:r111_4
+#  111|     r111_6(glval<int>)   = VariableAddress[y]     : 
+#  111|     m111_7(int)          = InitializeParameter[y] : &:r111_6
+#  112|     r112_1(glval<Point>) = VariableAddress[a]     : 
+#  112|     m112_2(Point)        = Uninitialized[a]       : &:r112_1
+#  112|     r112_3(glval<int>)   = FieldAddress[x]        : r112_1
+#  112|     r112_4(glval<int>)   = VariableAddress[x]     : 
+#  112|     r112_5(int)          = Load                   : &:r112_4, m111_5
+#  112|     m112_6(int)          = Store                  : &:r112_3, r112_5
+#  112|     m112_7(Point)        = Chi                    : total:m112_2, partial:m112_6
+#  112|     r112_8(glval<int>)   = FieldAddress[y]        : r112_1
+#  112|     r112_9(glval<int>)   = VariableAddress[y]     : 
+#  112|     r112_10(int)         = Load                   : &:r112_9, m111_7
+#  112|     m112_11(int)         = Store                  : &:r112_8, r112_10
+#  112|     m112_12(Point)       = Chi                    : total:m112_7, partial:m112_11
+#  113|     r113_1(glval<Point>) = VariableAddress[b]     : 
+#  113|     r113_2(glval<Point>) = VariableAddress[a]     : 
+#  113|     r113_3(Point)        = Load                   : &:r113_2, ~m112_12
+#  113|     m113_4(Point)        = Store                  : &:r113_1, r113_3
+#  114|     v114_1(void)         = NoOp                   : 
+#  111|     v111_8(void)         = ReturnVoid             : 
+#  111|     v111_9(void)         = UnmodeledUse           : mu*
+#  111|     v111_10(void)        = AliasedUse             : ~m111_2
+#  111|     v111_11(void)        = ExitFunction           : 
+
+#  116| void MayPartiallyOverlapEscaped(int, int)
+#  116|   Block 0
+#  116|     v116_1(void)           = EnterFunction                : 
+#  116|     m116_2(unknown)        = AliasedDefinition            : 
+#  116|     mu116_3(unknown)       = UnmodeledDefinition          : 
+#  116|     r116_4(glval<int>)     = VariableAddress[x]           : 
+#  116|     m116_5(int)            = InitializeParameter[x]       : &:r116_4
+#  116|     r116_6(glval<int>)     = VariableAddress[y]           : 
+#  116|     m116_7(int)            = InitializeParameter[y]       : &:r116_6
+#  117|     r117_1(glval<Point>)   = VariableAddress[a]           : 
+#  117|     m117_2(Point)          = Uninitialized[a]             : &:r117_1
+#  117|     r117_3(glval<int>)     = FieldAddress[x]              : r117_1
+#  117|     r117_4(glval<int>)     = VariableAddress[x]           : 
+#  117|     r117_5(int)            = Load                         : &:r117_4, m116_5
+#  117|     m117_6(int)            = Store                        : &:r117_3, r117_5
+#  117|     m117_7(Point)          = Chi                          : total:m117_2, partial:m117_6
+#  117|     r117_8(glval<int>)     = FieldAddress[y]              : r117_1
+#  117|     r117_9(glval<int>)     = VariableAddress[y]           : 
+#  117|     r117_10(int)           = Load                         : &:r117_9, m116_7
+#  117|     m117_11(int)           = Store                        : &:r117_8, r117_10
+#  117|     m117_12(Point)         = Chi                          : total:m117_7, partial:m117_11
+#  118|     r118_1(glval<Point>)   = VariableAddress[b]           : 
+#  118|     r118_2(glval<Point>)   = VariableAddress[a]           : 
+#  118|     r118_3(Point)          = Load                         : &:r118_2, ~m117_12
+#  118|     m118_4(Point)          = Store                        : &:r118_1, r118_3
+#  119|     r119_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#  119|     r119_2(glval<Point>)   = VariableAddress[a]           : 
+#  119|     r119_3(Point *)        = CopyValue                    : r119_2
+#  119|     r119_4(void *)         = Convert                      : r119_3
+#  119|     v119_5(void)           = Call                         : func:r119_1, 0:r119_4
+#  119|     m119_6(unknown)        = ^CallSideEffect              : ~m116_2
+#  119|     m119_7(unknown)        = Chi                          : total:m116_2, partial:m119_6
+#  119|     v119_8(void)           = ^BufferReadSideEffect[0]     : &:r119_4, ~m117_12
+#  119|     m119_9(unknown)        = ^BufferMayWriteSideEffect[0] : &:r119_4
+#  119|     m119_10(Point)         = Chi                          : total:m117_12, partial:m119_9
+#  120|     v120_1(void)           = NoOp                         : 
+#  116|     v116_8(void)           = ReturnVoid                   : 
+#  116|     v116_9(void)           = UnmodeledUse                 : mu*
+#  116|     v116_10(void)          = AliasedUse                   : ~m119_7
+#  116|     v116_11(void)          = ExitFunction                 : 
+
+#  122| void MergeMustExactlyOverlap(bool, int, int)
+#  122|   Block 0
+#  122|     v122_1(void)         = EnterFunction           : 
+#  122|     m122_2(unknown)      = AliasedDefinition       : 
+#  122|     mu122_3(unknown)     = UnmodeledDefinition     : 
+#  122|     r122_4(glval<bool>)  = VariableAddress[c]      : 
+#  122|     m122_5(bool)         = InitializeParameter[c]  : &:r122_4
+#  122|     r122_6(glval<int>)   = VariableAddress[x1]     : 
+#  122|     m122_7(int)          = InitializeParameter[x1] : &:r122_6
+#  122|     r122_8(glval<int>)   = VariableAddress[x2]     : 
+#  122|     m122_9(int)          = InitializeParameter[x2] : &:r122_8
+#  123|     r123_1(glval<Point>) = VariableAddress[a]      : 
+#  123|     m123_2(Point)        = Uninitialized[a]        : &:r123_1
+#  123|     r123_3(glval<int>)   = FieldAddress[x]         : r123_1
+#  123|     r123_4(int)          = Constant[0]             : 
+#  123|     m123_5(int)          = Store                   : &:r123_3, r123_4
+#  123|     m123_6(Point)        = Chi                     : total:m123_2, partial:m123_5
+#  123|     r123_7(glval<int>)   = FieldAddress[y]         : r123_1
+#  123|     r123_8(int)          = Constant[0]             : 
+#  123|     m123_9(int)          = Store                   : &:r123_7, r123_8
+#  123|     m123_10(Point)       = Chi                     : total:m123_6, partial:m123_9
+#  124|     r124_1(glval<bool>)  = VariableAddress[c]      : 
+#  124|     r124_2(bool)         = Load                    : &:r124_1, m122_5
+#  124|     v124_3(void)         = ConditionalBranch       : r124_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  125|   Block 1
+#  125|     r125_1(glval<int>)   = VariableAddress[x1] : 
+#  125|     r125_2(int)          = Load                : &:r125_1, m122_7
+#  125|     r125_3(glval<Point>) = VariableAddress[a]  : 
+#  125|     r125_4(glval<int>)   = FieldAddress[x]     : r125_3
+#  125|     m125_5(int)          = Store               : &:r125_4, r125_2
+#  125|     m125_6(Point)        = Chi                 : total:m123_10, partial:m125_5
+#-----|   Goto -> Block 3
+
+#  128|   Block 2
+#  128|     r128_1(glval<int>)   = VariableAddress[x2] : 
+#  128|     r128_2(int)          = Load                : &:r128_1, m122_9
+#  128|     r128_3(glval<Point>) = VariableAddress[a]  : 
+#  128|     r128_4(glval<int>)   = FieldAddress[x]     : r128_3
+#  128|     m128_5(int)          = Store               : &:r128_4, r128_2
+#  128|     m128_6(Point)        = Chi                 : total:m123_10, partial:m128_5
+#-----|   Goto -> Block 3
+
+#  130|   Block 3
+#  130|     m130_1(int)          = Phi                : from 1:m125_5, from 2:m128_5
+#  130|     m130_2(Point)        = Phi                : from 1:m125_6, from 2:m128_6
+#  130|     r130_3(glval<int>)   = VariableAddress[x] : 
+#  130|     r130_4(glval<Point>) = VariableAddress[a] : 
+#  130|     r130_5(glval<int>)   = FieldAddress[x]    : r130_4
+#  130|     r130_6(int)          = Load               : &:r130_5, m130_1
+#  130|     m130_7(int)          = Store              : &:r130_3, r130_6
+#  131|     r131_1(glval<Point>) = VariableAddress[b] : 
+#  131|     r131_2(glval<Point>) = VariableAddress[a] : 
+#  131|     r131_3(Point)        = Load               : &:r131_2, m130_2
+#  131|     m131_4(Point)        = Store              : &:r131_1, r131_3
+#  132|     v132_1(void)         = NoOp               : 
+#  122|     v122_10(void)        = ReturnVoid         : 
+#  122|     v122_11(void)        = UnmodeledUse       : mu*
+#  122|     v122_12(void)        = AliasedUse         : ~m122_2
+#  122|     v122_13(void)        = ExitFunction       : 
+
+#  134| void MergeMustExactlyWithMustTotallyOverlap(bool, Point, int)
+#  134|   Block 0
+#  134|     v134_1(void)         = EnterFunction           : 
+#  134|     m134_2(unknown)      = AliasedDefinition       : 
+#  134|     mu134_3(unknown)     = UnmodeledDefinition     : 
+#  134|     r134_4(glval<bool>)  = VariableAddress[c]      : 
+#  134|     m134_5(bool)         = InitializeParameter[c]  : &:r134_4
+#  134|     r134_6(glval<Point>) = VariableAddress[p]      : 
+#  134|     m134_7(Point)        = InitializeParameter[p]  : &:r134_6
+#  134|     r134_8(glval<int>)   = VariableAddress[x1]     : 
+#  134|     m134_9(int)          = InitializeParameter[x1] : &:r134_8
+#  135|     r135_1(glval<Point>) = VariableAddress[a]      : 
+#  135|     m135_2(Point)        = Uninitialized[a]        : &:r135_1
+#  135|     r135_3(glval<int>)   = FieldAddress[x]         : r135_1
+#  135|     r135_4(int)          = Constant[0]             : 
+#  135|     m135_5(int)          = Store                   : &:r135_3, r135_4
+#  135|     m135_6(Point)        = Chi                     : total:m135_2, partial:m135_5
+#  135|     r135_7(glval<int>)   = FieldAddress[y]         : r135_1
+#  135|     r135_8(int)          = Constant[0]             : 
+#  135|     m135_9(int)          = Store                   : &:r135_7, r135_8
+#  135|     m135_10(Point)       = Chi                     : total:m135_6, partial:m135_9
+#  136|     r136_1(glval<bool>)  = VariableAddress[c]      : 
+#  136|     r136_2(bool)         = Load                    : &:r136_1, m134_5
+#  136|     v136_3(void)         = ConditionalBranch       : r136_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  137|   Block 1
+#  137|     r137_1(glval<int>)   = VariableAddress[x1] : 
+#  137|     r137_2(int)          = Load                : &:r137_1, m134_9
+#  137|     r137_3(glval<Point>) = VariableAddress[a]  : 
+#  137|     r137_4(glval<int>)   = FieldAddress[x]     : r137_3
+#  137|     m137_5(int)          = Store               : &:r137_4, r137_2
+#  137|     m137_6(Point)        = Chi                 : total:m135_10, partial:m137_5
+#-----|   Goto -> Block 3
+
+#  140|   Block 2
+#  140|     r140_1(glval<Point>) = VariableAddress[p] : 
+#  140|     r140_2(Point)        = Load               : &:r140_1, m134_7
+#  140|     r140_3(glval<Point>) = VariableAddress[a] : 
+#  140|     m140_4(Point)        = Store              : &:r140_3, r140_2
+#-----|   Goto -> Block 3
+
+#  142|   Block 3
+#  142|     m142_1(int)          = Phi                : from 1:m137_5, from 2:~m140_4
+#  142|     m142_2(Point)        = Phi                : from 1:m137_6, from 2:m140_4
+#  142|     r142_3(glval<int>)   = VariableAddress[x] : 
+#  142|     r142_4(glval<Point>) = VariableAddress[a] : 
+#  142|     r142_5(glval<int>)   = FieldAddress[x]    : r142_4
+#  142|     r142_6(int)          = Load               : &:r142_5, m142_1
+#  142|     m142_7(int)          = Store              : &:r142_3, r142_6
+#  143|     v143_1(void)         = NoOp               : 
+#  134|     v134_10(void)        = ReturnVoid         : 
+#  134|     v134_11(void)        = UnmodeledUse       : mu*
+#  134|     v134_12(void)        = AliasedUse         : ~m134_2
+#  134|     v134_13(void)        = ExitFunction       : 
+
+#  145| void MergeMustExactlyWithMayPartiallyOverlap(bool, Point, int)
+#  145|   Block 0
+#  145|     v145_1(void)         = EnterFunction           : 
+#  145|     m145_2(unknown)      = AliasedDefinition       : 
+#  145|     mu145_3(unknown)     = UnmodeledDefinition     : 
+#  145|     r145_4(glval<bool>)  = VariableAddress[c]      : 
+#  145|     m145_5(bool)         = InitializeParameter[c]  : &:r145_4
+#  145|     r145_6(glval<Point>) = VariableAddress[p]      : 
+#  145|     m145_7(Point)        = InitializeParameter[p]  : &:r145_6
+#  145|     r145_8(glval<int>)   = VariableAddress[x1]     : 
+#  145|     m145_9(int)          = InitializeParameter[x1] : &:r145_8
+#  146|     r146_1(glval<Point>) = VariableAddress[a]      : 
+#  146|     m146_2(Point)        = Uninitialized[a]        : &:r146_1
+#  146|     r146_3(glval<int>)   = FieldAddress[x]         : r146_1
+#  146|     r146_4(int)          = Constant[0]             : 
+#  146|     m146_5(int)          = Store                   : &:r146_3, r146_4
+#  146|     m146_6(Point)        = Chi                     : total:m146_2, partial:m146_5
+#  146|     r146_7(glval<int>)   = FieldAddress[y]         : r146_1
+#  146|     r146_8(int)          = Constant[0]             : 
+#  146|     m146_9(int)          = Store                   : &:r146_7, r146_8
+#  146|     m146_10(Point)       = Chi                     : total:m146_6, partial:m146_9
+#  147|     r147_1(glval<bool>)  = VariableAddress[c]      : 
+#  147|     r147_2(bool)         = Load                    : &:r147_1, m145_5
+#  147|     v147_3(void)         = ConditionalBranch       : r147_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  148|   Block 1
+#  148|     r148_1(glval<int>)   = VariableAddress[x1] : 
+#  148|     r148_2(int)          = Load                : &:r148_1, m145_9
+#  148|     r148_3(glval<Point>) = VariableAddress[a]  : 
+#  148|     r148_4(glval<int>)   = FieldAddress[x]     : r148_3
+#  148|     m148_5(int)          = Store               : &:r148_4, r148_2
+#  148|     m148_6(Point)        = Chi                 : total:m146_10, partial:m148_5
+#-----|   Goto -> Block 3
+
+#  151|   Block 2
+#  151|     r151_1(glval<Point>) = VariableAddress[p] : 
+#  151|     r151_2(Point)        = Load               : &:r151_1, m145_7
+#  151|     r151_3(glval<Point>) = VariableAddress[a] : 
+#  151|     m151_4(Point)        = Store              : &:r151_3, r151_2
+#-----|   Goto -> Block 3
+
+#  153|   Block 3
+#  153|     m153_1(Point)        = Phi                : from 1:m148_6, from 2:m151_4
+#  153|     r153_2(glval<Point>) = VariableAddress[b] : 
+#  153|     r153_3(glval<Point>) = VariableAddress[a] : 
+#  153|     r153_4(Point)        = Load               : &:r153_3, m153_1
+#  153|     m153_5(Point)        = Store              : &:r153_2, r153_4
+#  154|     v154_1(void)         = NoOp               : 
+#  145|     v145_10(void)        = ReturnVoid         : 
+#  145|     v145_11(void)        = UnmodeledUse       : mu*
+#  145|     v145_12(void)        = AliasedUse         : ~m145_2
+#  145|     v145_13(void)        = ExitFunction       : 
+
+#  156| void MergeMustTotallyOverlapWithMayPartiallyOverlap(bool, Rect, int)
+#  156|   Block 0
+#  156|     v156_1(void)         = EnterFunction             : 
+#  156|     m156_2(unknown)      = AliasedDefinition         : 
+#  156|     mu156_3(unknown)     = UnmodeledDefinition       : 
+#  156|     r156_4(glval<bool>)  = VariableAddress[c]        : 
+#  156|     m156_5(bool)         = InitializeParameter[c]    : &:r156_4
+#  156|     r156_6(glval<Rect>)  = VariableAddress[r]        : 
+#  156|     m156_7(Rect)         = InitializeParameter[r]    : &:r156_6
+#  156|     r156_8(glval<int>)   = VariableAddress[x1]       : 
+#  156|     m156_9(int)          = InitializeParameter[x1]   : &:r156_8
+#  157|     r157_1(glval<Rect>)  = VariableAddress[a]        : 
+#  157|     m157_2(Rect)         = Uninitialized[a]          : &:r157_1
+#  157|     r157_3(glval<Point>) = FieldAddress[topLeft]     : r157_1
+#  157|     r157_4(Point)        = Constant[0]               : 
+#  157|     m157_5(Point)        = Store                     : &:r157_3, r157_4
+#  157|     m157_6(Rect)         = Chi                       : total:m157_2, partial:m157_5
+#  157|     r157_7(glval<Point>) = FieldAddress[bottomRight] : r157_1
+#  157|     r157_8(Point)        = Constant[0]               : 
+#  157|     m157_9(Point)        = Store                     : &:r157_7, r157_8
+#  157|     m157_10(Rect)        = Chi                       : total:m157_6, partial:m157_9
+#  158|     r158_1(glval<bool>)  = VariableAddress[c]        : 
+#  158|     r158_2(bool)         = Load                      : &:r158_1, m156_5
+#  158|     v158_3(void)         = ConditionalBranch         : r158_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  159|   Block 1
+#  159|     r159_1(glval<int>)   = VariableAddress[x1]   : 
+#  159|     r159_2(int)          = Load                  : &:r159_1, m156_9
+#  159|     r159_3(glval<Rect>)  = VariableAddress[a]    : 
+#  159|     r159_4(glval<Point>) = FieldAddress[topLeft] : r159_3
+#  159|     r159_5(glval<int>)   = FieldAddress[x]       : r159_4
+#  159|     m159_6(int)          = Store                 : &:r159_5, r159_2
+#  159|     m159_7(Rect)         = Chi                   : total:m157_10, partial:m159_6
+#-----|   Goto -> Block 3
+
+#  162|   Block 2
+#  162|     r162_1(glval<Rect>) = VariableAddress[r] : 
+#  162|     r162_2(Rect)        = Load               : &:r162_1, m156_7
+#  162|     r162_3(glval<Rect>) = VariableAddress[a] : 
+#  162|     m162_4(Rect)        = Store              : &:r162_3, r162_2
+#-----|   Goto -> Block 3
+
+#  164|   Block 3
+#  164|     m164_1(Rect)         = Phi                   : from 1:m159_7, from 2:m162_4
+#  164|     r164_2(glval<Point>) = VariableAddress[b]    : 
+#  164|     r164_3(glval<Rect>)  = VariableAddress[a]    : 
+#  164|     r164_4(glval<Point>) = FieldAddress[topLeft] : r164_3
+#  164|     r164_5(Point)        = Load                  : &:r164_4, ~m164_1
+#  164|     m164_6(Point)        = Store                 : &:r164_2, r164_5
+#  165|     v165_1(void)         = NoOp                  : 
+#  156|     v156_10(void)        = ReturnVoid            : 
+#  156|     v156_11(void)        = UnmodeledUse          : mu*
+#  156|     v156_12(void)        = AliasedUse            : ~m156_2
+#  156|     v156_13(void)        = ExitFunction          : 
+
+#  171| void WrapperStruct(Wrapper)
+#  171|   Block 0
+#  171|     v171_1(void)           = EnterFunction          : 
+#  171|     m171_2(unknown)        = AliasedDefinition      : 
+#  171|     mu171_3(unknown)       = UnmodeledDefinition    : 
+#  171|     r171_4(glval<Wrapper>) = VariableAddress[w]     : 
+#  171|     m171_5(Wrapper)        = InitializeParameter[w] : &:r171_4
+#  172|     r172_1(glval<Wrapper>) = VariableAddress[x]     : 
+#  172|     r172_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  172|     r172_3(Wrapper)        = Load                   : &:r172_2, m171_5
+#  172|     m172_4(Wrapper)        = Store                  : &:r172_1, r172_3
+#  173|     r173_1(glval<int>)     = VariableAddress[a]     : 
+#  173|     r173_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  173|     r173_3(glval<int>)     = FieldAddress[f]        : r173_2
+#  173|     r173_4(int)            = Load                   : &:r173_3, ~m171_5
+#  173|     m173_5(int)            = Store                  : &:r173_1, r173_4
+#  174|     r174_1(int)            = Constant[5]            : 
+#  174|     r174_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  174|     r174_3(glval<int>)     = FieldAddress[f]        : r174_2
+#  174|     m174_4(int)            = Store                  : &:r174_3, r174_1
+#  175|     r175_1(glval<Wrapper>) = VariableAddress[w]     : 
+#  175|     r175_2(glval<int>)     = FieldAddress[f]        : r175_1
+#  175|     r175_3(int)            = Load                   : &:r175_2, m174_4
+#  175|     r175_4(glval<int>)     = VariableAddress[a]     : 
+#  175|     m175_5(int)            = Store                  : &:r175_4, r175_3
+#  176|     r176_1(glval<Wrapper>) = VariableAddress[w]     : 
+#  176|     r176_2(Wrapper)        = Load                   : &:r176_1, ~m174_4
+#  176|     r176_3(glval<Wrapper>) = VariableAddress[x]     : 
+#  176|     m176_4(Wrapper)        = Store                  : &:r176_3, r176_2
+#  177|     v177_1(void)           = NoOp                   : 
+#  171|     v171_6(void)           = ReturnVoid             : 
+#  171|     v171_7(void)           = UnmodeledUse           : mu*
+#  171|     v171_8(void)           = AliasedUse             : ~m171_2
+#  171|     v171_9(void)           = ExitFunction           : 
+
+#  179| int AsmStmt(int*)
+#  179|   Block 0
+#  179|     v179_1(void)         = EnterFunction            : 
+#  179|     m179_2(unknown)      = AliasedDefinition        : 
+#  179|     mu179_3(unknown)     = UnmodeledDefinition      : 
+#  179|     r179_4(glval<int *>) = VariableAddress[p]       : 
+#  179|     m179_5(int *)        = InitializeParameter[p]   : &:r179_4
+#  179|     r179_6(int *)        = Load                     : &:r179_4, m179_5
+#  179|     m179_7(unknown)      = InitializeIndirection[p] : &:r179_6
+#  179|     m179_8(unknown)      = Chi                      : total:m179_2, partial:m179_7
+#  180|     m180_1(unknown)      = InlineAsm                : ~m179_8
+#  180|     m180_2(unknown)      = Chi                      : total:m179_8, partial:m180_1
+#  181|     r181_1(glval<int>)   = VariableAddress[#return] : 
+#  181|     r181_2(glval<int *>) = VariableAddress[p]       : 
+#  181|     r181_3(int *)        = Load                     : &:r181_2, m179_5
+#  181|     r181_4(int)          = Load                     : &:r181_3, ~m180_2
+#  181|     m181_5(int)          = Store                    : &:r181_1, r181_4
+#  179|     v179_9(void)         = ReturnIndirection        : &:r179_6, ~m180_2
+#  179|     r179_10(glval<int>)  = VariableAddress[#return] : 
+#  179|     v179_11(void)        = ReturnValue              : &:r179_10, m181_5
+#  179|     v179_12(void)        = UnmodeledUse             : mu*
+#  179|     v179_13(void)        = AliasedUse               : ~m180_2
+#  179|     v179_14(void)        = ExitFunction             : 
+
+#  184| void AsmStmtWithOutputs(unsigned int&, unsigned int&, unsigned int&, unsigned int&)
+#  184|   Block 0
+#  184|     v184_1(void)                   = EnterFunction            : 
+#  184|     m184_2(unknown)                = AliasedDefinition        : 
+#  184|     mu184_3(unknown)               = UnmodeledDefinition      : 
+#  184|     r184_4(glval<unsigned int &>)  = VariableAddress[a]       : 
+#  184|     m184_5(unsigned int &)         = InitializeParameter[a]   : &:r184_4
+#  184|     r184_6(unsigned int &)         = Load                     : &:r184_4, m184_5
+#  184|     m184_7(unknown)                = InitializeIndirection[a] : &:r184_6
+#  184|     m184_8(unknown)                = Chi                      : total:m184_2, partial:m184_7
+#  184|     r184_9(glval<unsigned int &>)  = VariableAddress[b]       : 
+#  184|     m184_10(unsigned int &)        = InitializeParameter[b]   : &:r184_9
+#  184|     r184_11(unsigned int &)        = Load                     : &:r184_9, m184_10
+#  184|     m184_12(unknown)               = InitializeIndirection[b] : &:r184_11
+#  184|     m184_13(unknown)               = Chi                      : total:m184_8, partial:m184_12
+#  184|     r184_14(glval<unsigned int &>) = VariableAddress[c]       : 
+#  184|     m184_15(unsigned int &)        = InitializeParameter[c]   : &:r184_14
+#  184|     r184_16(unsigned int &)        = Load                     : &:r184_14, m184_15
+#  184|     m184_17(unknown)               = InitializeIndirection[c] : &:r184_16
+#  184|     m184_18(unknown)               = Chi                      : total:m184_13, partial:m184_17
+#  184|     r184_19(glval<unsigned int &>) = VariableAddress[d]       : 
+#  184|     m184_20(unsigned int &)        = InitializeParameter[d]   : &:r184_19
+#  184|     r184_21(unsigned int &)        = Load                     : &:r184_19, m184_20
+#  184|     m184_22(unknown)               = InitializeIndirection[d] : &:r184_21
+#  184|     m184_23(unknown)               = Chi                      : total:m184_18, partial:m184_22
+#  189|     r189_1(glval<unsigned int &>)  = VariableAddress[a]       : 
+#  189|     r189_2(unsigned int &)         = Load                     : &:r189_1, m184_5
+#  189|     r189_3(glval<unsigned int>)    = CopyValue                : r189_2
+#  189|     r189_4(glval<unsigned int &>)  = VariableAddress[b]       : 
+#  189|     r189_5(unsigned int &)         = Load                     : &:r189_4, m184_10
+#  189|     r189_6(glval<unsigned int>)    = CopyValue                : r189_5
+#  190|     r190_1(glval<unsigned int &>)  = VariableAddress[c]       : 
+#  190|     r190_2(unsigned int &)         = Load                     : &:r190_1, m184_15
+#  190|     r190_3(unsigned int)           = Load                     : &:r190_2, ~m184_23
+#  190|     r190_4(glval<unsigned int &>)  = VariableAddress[d]       : 
+#  190|     r190_5(unsigned int &)         = Load                     : &:r190_4, m184_20
+#  190|     r190_6(unsigned int)           = Load                     : &:r190_5, ~m184_23
+#  186|     m186_1(unknown)                = InlineAsm                : ~m184_23, 0:r189_3, 1:r189_6, 2:r190_3, 3:r190_6
+#  186|     m186_2(unknown)                = Chi                      : total:m184_23, partial:m186_1
+#  192|     v192_1(void)                   = NoOp                     : 
+#  184|     v184_24(void)                  = ReturnIndirection        : &:r184_6, ~m186_2
+#  184|     v184_25(void)                  = ReturnIndirection        : &:r184_11, ~m186_2
+#  184|     v184_26(void)                  = ReturnIndirection        : &:r184_16, ~m186_2
+#  184|     v184_27(void)                  = ReturnIndirection        : &:r184_21, ~m186_2
+#  184|     v184_28(void)                  = ReturnVoid               : 
+#  184|     v184_29(void)                  = UnmodeledUse             : mu*
+#  184|     v184_30(void)                  = AliasedUse               : ~m186_2
+#  184|     v184_31(void)                  = ExitFunction             : 
+
+#  198| int PureFunctions(char*, char*, int)
+#  198|   Block 0
+#  198|     v198_1(void)           = EnterFunction               : 
+#  198|     m198_2(unknown)        = AliasedDefinition           : 
+#  198|     mu198_3(unknown)       = UnmodeledDefinition         : 
+#  198|     r198_4(glval<char *>)  = VariableAddress[str1]       : 
+#  198|     m198_5(char *)         = InitializeParameter[str1]   : &:r198_4
+#  198|     r198_6(char *)         = Load                        : &:r198_4, m198_5
+#  198|     m198_7(unknown)        = InitializeIndirection[str1] : &:r198_6
+#  198|     m198_8(unknown)        = Chi                         : total:m198_2, partial:m198_7
+#  198|     r198_9(glval<char *>)  = VariableAddress[str2]       : 
+#  198|     m198_10(char *)        = InitializeParameter[str2]   : &:r198_9
+#  198|     r198_11(char *)        = Load                        : &:r198_9, m198_10
+#  198|     m198_12(unknown)       = InitializeIndirection[str2] : &:r198_11
+#  198|     m198_13(unknown)       = Chi                         : total:m198_8, partial:m198_12
+#  198|     r198_14(glval<int>)    = VariableAddress[x]          : 
+#  198|     m198_15(int)           = InitializeParameter[x]      : &:r198_14
+#  199|     r199_1(glval<int>)     = VariableAddress[ret]        : 
+#  199|     r199_2(glval<unknown>) = FunctionAddress[strcmp]     : 
+#  199|     r199_3(glval<char *>)  = VariableAddress[str1]       : 
+#  199|     r199_4(char *)         = Load                        : &:r199_3, m198_5
+#  199|     r199_5(char *)         = Convert                     : r199_4
+#  199|     r199_6(glval<char *>)  = VariableAddress[str2]       : 
+#  199|     r199_7(char *)         = Load                        : &:r199_6, m198_10
+#  199|     r199_8(char *)         = Convert                     : r199_7
+#  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
+#  199|     v199_10(void)          = ^CallReadSideEffect         : ~m198_13
+#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~m198_13
+#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~m198_13
+#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
+#  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
+#  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
+#  200|     r200_3(char *)         = Load                        : &:r200_2, m198_5
+#  200|     r200_4(char *)         = Convert                     : r200_3
+#  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
+#  200|     v200_6(void)           = ^CallReadSideEffect         : ~m198_13
+#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~m198_13
+#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
+#  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
+#  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
+#  201|     r201_3(int)            = Load                        : &:r201_2, m198_15
+#  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
+#  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_7(int)            = Add                         : r201_6, r201_4
+#  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
+#  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 
+#  202|     r202_2(glval<int>)     = VariableAddress[ret]        : 
+#  202|     r202_3(int)            = Load                        : &:r202_2, m201_8
+#  202|     m202_4(int)            = Store                       : &:r202_1, r202_3
+#  198|     v198_16(void)          = ReturnIndirection           : &:r198_6, ~m198_13
+#  198|     v198_17(void)          = ReturnIndirection           : &:r198_11, ~m198_13
+#  198|     r198_18(glval<int>)    = VariableAddress[#return]    : 
+#  198|     v198_19(void)          = ReturnValue                 : &:r198_18, m202_4
+#  198|     v198_20(void)          = UnmodeledUse                : mu*
+#  198|     v198_21(void)          = AliasedUse                  : ~m198_13
+#  198|     v198_22(void)          = ExitFunction                : 
+
+#  207| int ModeledCallTarget(int)
+#  207|   Block 0
+#  207|     v207_1(void)           = EnterFunction                      : 
+#  207|     m207_2(unknown)        = AliasedDefinition                  : 
+#  207|     mu207_3(unknown)       = UnmodeledDefinition                : 
+#  207|     r207_4(glval<int>)     = VariableAddress[x]                 : 
+#  207|     m207_5(int)            = InitializeParameter[x]             : &:r207_4
+#  208|     r208_1(glval<int>)     = VariableAddress[y]                 : 
+#  208|     m208_2(int)            = Uninitialized[y]                   : &:r208_1
+#  209|     r209_1(glval<unknown>) = FunctionAddress[memcpy]            : 
+#  209|     r209_2(glval<int>)     = VariableAddress[y]                 : 
+#  209|     r209_3(int *)          = CopyValue                          : r209_2
+#  209|     r209_4(void *)         = Convert                            : r209_3
+#  209|     r209_5(glval<int>)     = VariableAddress[x]                 : 
+#  209|     r209_6(int *)          = CopyValue                          : r209_5
+#  209|     r209_7(void *)         = Convert                            : r209_6
+#  209|     r209_8(int)            = Constant[4]                        : 
+#  209|     r209_9(void *)         = Call                               : func:r209_1, 0:r209_4, 1:r209_7, 2:r209_8
+#  209|     v209_10(void)          = ^SizedBufferReadSideEffect[1]      : &:r209_7, r209_8, ~m207_5
+#  209|     m209_11(unknown)       = ^SizedBufferMustWriteSideEffect[0] : &:r209_4, r209_8
+#  209|     m209_12(int)           = Chi                                : total:m208_2, partial:m209_11
+#  210|     r210_1(glval<int>)     = VariableAddress[#return]           : 
+#  210|     r210_2(glval<int>)     = VariableAddress[y]                 : 
+#  210|     r210_3(int)            = Load                               : &:r210_2, ~m209_12
+#  210|     m210_4(int)            = Store                              : &:r210_1, r210_3
+#  207|     r207_6(glval<int>)     = VariableAddress[#return]           : 
+#  207|     v207_7(void)           = ReturnValue                        : &:r207_6, m210_4
+#  207|     v207_8(void)           = UnmodeledUse                       : mu*
+#  207|     v207_9(void)           = AliasedUse                         : ~m207_2
+#  207|     v207_10(void)          = ExitFunction                       : 
+
+#  213| void InitArray()
+#  213|   Block 0
+#  213|     v213_1(void)            = EnterFunction            : 
+#  213|     m213_2(unknown)         = AliasedDefinition        : 
+#  213|     mu213_3(unknown)        = UnmodeledDefinition      : 
+#  214|     r214_1(glval<char[32]>) = VariableAddress[a_pad]   : 
+#  214|     r214_2(glval<char[32]>) = StringConstant[""]       : 
+#  214|     r214_3(char[32])        = Load                     : &:r214_2, ~m213_2
+#  214|     m214_4(char[32])        = Store                    : &:r214_1, r214_3
+#  215|     r215_1(glval<char[4]>)  = VariableAddress[a_nopad] : 
+#  215|     r215_2(glval<char[4]>)  = StringConstant["foo"]    : 
+#  215|     r215_3(char[4])         = Load                     : &:r215_2, ~m213_2
+#  215|     m215_4(char[4])         = Store                    : &:r215_1, r215_3
+#  216|     r216_1(glval<char[5]>)  = VariableAddress[a_infer] : 
+#  216|     r216_2(glval<char[5]>)  = StringConstant["blah"]   : 
+#  216|     r216_3(char[5])         = Load                     : &:r216_2, ~m213_2
+#  216|     m216_4(char[5])         = Store                    : &:r216_1, r216_3
+#  217|     r217_1(glval<char[2]>)  = VariableAddress[b]       : 
+#  217|     m217_2(char[2])         = Uninitialized[b]         : &:r217_1
+#  218|     r218_1(glval<char[2]>)  = VariableAddress[c]       : 
+#  218|     m218_2(char[2])         = Uninitialized[c]         : &:r218_1
+#  218|     r218_3(int)             = Constant[0]              : 
+#  218|     r218_4(glval<char>)     = PointerAdd[1]            : r218_1, r218_3
+#  218|     r218_5(unknown[2])      = Constant[0]              : 
+#  218|     m218_6(unknown[2])      = Store                    : &:r218_4, r218_5
+#  219|     r219_1(glval<char[2]>)  = VariableAddress[d]       : 
+#  219|     m219_2(char[2])         = Uninitialized[d]         : &:r219_1
+#  219|     r219_3(int)             = Constant[0]              : 
+#  219|     r219_4(glval<char>)     = PointerAdd[1]            : r219_1, r219_3
+#  219|     r219_5(char)            = Constant[0]              : 
+#  219|     m219_6(char)            = Store                    : &:r219_4, r219_5
+#  219|     m219_7(char[2])         = Chi                      : total:m219_2, partial:m219_6
+#  219|     r219_8(int)             = Constant[1]              : 
+#  219|     r219_9(glval<char>)     = PointerAdd[1]            : r219_1, r219_8
+#  219|     r219_10(char)           = Constant[0]              : 
+#  219|     m219_11(char)           = Store                    : &:r219_9, r219_10
+#  219|     m219_12(char[2])        = Chi                      : total:m219_7, partial:m219_11
+#  220|     r220_1(glval<char[2]>)  = VariableAddress[e]       : 
+#  220|     m220_2(char[2])         = Uninitialized[e]         : &:r220_1
+#  220|     r220_3(int)             = Constant[0]              : 
+#  220|     r220_4(glval<char>)     = PointerAdd[1]            : r220_1, r220_3
+#  220|     r220_5(char)            = Constant[0]              : 
+#  220|     m220_6(char)            = Store                    : &:r220_4, r220_5
+#  220|     m220_7(char[2])         = Chi                      : total:m220_2, partial:m220_6
+#  220|     r220_8(int)             = Constant[1]              : 
+#  220|     r220_9(glval<char>)     = PointerAdd[1]            : r220_1, r220_8
+#  220|     r220_10(char)           = Constant[1]              : 
+#  220|     m220_11(char)           = Store                    : &:r220_9, r220_10
+#  220|     m220_12(char[2])        = Chi                      : total:m220_7, partial:m220_11
+#  221|     r221_1(glval<char[3]>)  = VariableAddress[f]       : 
+#  221|     m221_2(char[3])         = Uninitialized[f]         : &:r221_1
+#  221|     r221_3(int)             = Constant[0]              : 
+#  221|     r221_4(glval<char>)     = PointerAdd[1]            : r221_1, r221_3
+#  221|     r221_5(char)            = Constant[0]              : 
+#  221|     m221_6(char)            = Store                    : &:r221_4, r221_5
+#  221|     m221_7(char[3])         = Chi                      : total:m221_2, partial:m221_6
+#  221|     r221_8(int)             = Constant[1]              : 
+#  221|     r221_9(glval<char>)     = PointerAdd[1]            : r221_1, r221_8
+#  221|     r221_10(unknown[2])     = Constant[0]              : 
+#  221|     m221_11(unknown[2])     = Store                    : &:r221_9, r221_10
+#  221|     m221_12(char[3])        = Chi                      : total:m221_7, partial:m221_11
+#  222|     v222_1(void)            = NoOp                     : 
+#  213|     v213_4(void)            = ReturnVoid               : 
+#  213|     v213_5(void)            = UnmodeledUse             : mu*
+#  213|     v213_6(void)            = AliasedUse               : ~m213_2
+#  213|     v213_7(void)            = ExitFunction             : 
+
+#  226| char StringLiteralAliasing()
+#  226|   Block 0
+#  226|     v226_1(void)           = EnterFunction                 : 
+#  226|     m226_2(unknown)        = AliasedDefinition             : 
+#  226|     mu226_3(unknown)       = UnmodeledDefinition           : 
+#  227|     r227_1(glval<unknown>) = FunctionAddress[ExternalFunc] : 
+#  227|     v227_2(void)           = Call                          : func:r227_1
+#  227|     m227_3(unknown)        = ^CallSideEffect               : ~m226_2
+#  227|     m227_4(unknown)        = Chi                           : total:m226_2, partial:m227_3
+#  229|     r229_1(glval<char *>)  = VariableAddress[s]            : 
+#  229|     r229_2(glval<char[8]>) = StringConstant["Literal"]     : 
+#  229|     r229_3(char *)         = Convert                       : r229_2
+#  229|     m229_4(char *)         = Store                         : &:r229_1, r229_3
+#  230|     r230_1(glval<char>)    = VariableAddress[#return]      : 
+#  230|     r230_2(glval<char *>)  = VariableAddress[s]            : 
+#  230|     r230_3(char *)         = Load                          : &:r230_2, m229_4
+#  230|     r230_4(int)            = Constant[2]                   : 
+#  230|     r230_5(glval<char>)    = PointerAdd[1]                 : r230_3, r230_4
+#  230|     r230_6(char)           = Load                          : &:r230_5, ~m226_2
+#  230|     m230_7(char)           = Store                         : &:r230_1, r230_6
+#  226|     r226_4(glval<char>)    = VariableAddress[#return]      : 
+#  226|     v226_5(void)           = ReturnValue                   : &:r226_4, m230_7
+#  226|     v226_6(void)           = UnmodeledUse                  : mu*
+#  226|     v226_7(void)           = AliasedUse                    : ~m227_4
+#  226|     v226_8(void)           = ExitFunction                  : 
+
+#  235| void Constructible::Constructible(int)
+#  235|   Block 0
+#  235|     v235_1(void)                 = EnterFunction          : 
+#  235|     m235_2(unknown)              = AliasedDefinition      : 
+#  235|     mu235_3(unknown)             = UnmodeledDefinition    : 
+#  235|     r235_4(glval<Constructible>) = InitializeThis         : 
+#  235|     r235_5(glval<int>)           = VariableAddress[x]     : 
+#  235|     m235_6(int)                  = InitializeParameter[x] : &:r235_5
+#  235|     v235_7(void)                 = NoOp                   : 
+#  235|     v235_8(void)                 = ReturnVoid             : 
+#  235|     v235_9(void)                 = UnmodeledUse           : mu*
+#  235|     v235_10(void)                = AliasedUse             : ~m235_2
+#  235|     v235_11(void)                = ExitFunction           : 
+
+#  236| void Constructible::g()
+#  236|   Block 0
+#  236|     v236_1(void)                 = EnterFunction       : 
+#  236|     m236_2(unknown)              = AliasedDefinition   : 
+#  236|     mu236_3(unknown)             = UnmodeledDefinition : 
+#  236|     r236_4(glval<Constructible>) = InitializeThis      : 
+#  236|     v236_5(void)                 = NoOp                : 
+#  236|     v236_6(void)                 = ReturnVoid          : 
+#  236|     v236_7(void)                 = UnmodeledUse        : mu*
+#  236|     v236_8(void)                 = AliasedUse          : ~m236_2
+#  236|     v236_9(void)                 = ExitFunction        : 
+
+#  239| void ExplicitConstructorCalls()
+#  239|   Block 0
+#  239|     v239_1(void)                 = EnterFunction                   : 
+#  239|     m239_2(unknown)              = AliasedDefinition               : 
+#  239|     mu239_3(unknown)             = UnmodeledDefinition             : 
+#  240|     r240_1(glval<Constructible>) = VariableAddress[c]              : 
+#  240|     m240_2(Constructible)        = Uninitialized[c]                : &:r240_1
+#  240|     r240_3(glval<unknown>)       = FunctionAddress[Constructible]  : 
+#  240|     r240_4(int)                  = Constant[1]                     : 
+#  240|     v240_5(void)                 = Call                            : func:r240_3, this:r240_1, 0:r240_4
+#  240|     m240_6(unknown)              = ^CallSideEffect                 : ~m239_2
+#  240|     m240_7(unknown)              = Chi                             : total:m239_2, partial:m240_6
+#  240|     m240_8(Constructible)        = ^IndirectMayWriteSideEffect[-1] : &:r240_1
+#  240|     m240_9(Constructible)        = Chi                             : total:m240_2, partial:m240_8
+#  241|     r241_1(glval<Constructible>) = VariableAddress[c]              : 
+#  241|     r241_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  241|     v241_3(void)                 = Call                            : func:r241_2, this:r241_1
+#  241|     m241_4(unknown)              = ^CallSideEffect                 : ~m240_7
+#  241|     m241_5(unknown)              = Chi                             : total:m240_7, partial:m241_4
+#  241|     v241_6(void)                 = ^BufferReadSideEffect[-1]       : &:r241_1, ~m240_9
+#  241|     m241_7(Constructible)        = ^IndirectMayWriteSideEffect[-1] : &:r241_1
+#  241|     m241_8(Constructible)        = Chi                             : total:m240_9, partial:m241_7
+#  242|     r242_1(glval<Constructible>) = VariableAddress[c]              : 
+#  242|     r242_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  242|     v242_3(void)                 = Call                            : func:r242_2, this:r242_1
+#  242|     m242_4(unknown)              = ^CallSideEffect                 : ~m241_5
+#  242|     m242_5(unknown)              = Chi                             : total:m241_5, partial:m242_4
+#  242|     v242_6(void)                 = ^BufferReadSideEffect[-1]       : &:r242_1, ~m241_8
+#  242|     m242_7(Constructible)        = ^IndirectMayWriteSideEffect[-1] : &:r242_1
+#  242|     m242_8(Constructible)        = Chi                             : total:m241_8, partial:m242_7
+#  243|     r243_1(glval<Constructible>) = VariableAddress[c2]             : 
+#  243|     m243_2(Constructible)        = Uninitialized[c2]               : &:r243_1
+#  243|     r243_3(glval<unknown>)       = FunctionAddress[Constructible]  : 
+#  243|     r243_4(int)                  = Constant[2]                     : 
+#  243|     v243_5(void)                 = Call                            : func:r243_3, this:r243_1, 0:r243_4
+#  243|     m243_6(unknown)              = ^CallSideEffect                 : ~m242_5
+#  243|     m243_7(unknown)              = Chi                             : total:m242_5, partial:m243_6
+#  243|     m243_8(Constructible)        = ^IndirectMayWriteSideEffect[-1] : &:r243_1
+#  243|     m243_9(Constructible)        = Chi                             : total:m243_2, partial:m243_8
+#  244|     r244_1(glval<Constructible>) = VariableAddress[c2]             : 
+#  244|     r244_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  244|     v244_3(void)                 = Call                            : func:r244_2, this:r244_1
+#  244|     m244_4(unknown)              = ^CallSideEffect                 : ~m243_7
+#  244|     m244_5(unknown)              = Chi                             : total:m243_7, partial:m244_4
+#  244|     v244_6(void)                 = ^BufferReadSideEffect[-1]       : &:r244_1, ~m243_9
+#  244|     m244_7(Constructible)        = ^IndirectMayWriteSideEffect[-1] : &:r244_1
+#  244|     m244_8(Constructible)        = Chi                             : total:m243_9, partial:m244_7
+#  245|     v245_1(void)                 = NoOp                            : 
+#  239|     v239_4(void)                 = ReturnVoid                      : 
+#  239|     v239_5(void)                 = UnmodeledUse                    : mu*
+#  239|     v239_6(void)                 = AliasedUse                      : ~m244_5
+#  239|     v239_7(void)                 = ExitFunction                    : 
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.qlref b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.qlref
rename to cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.ql
new file mode 100644
index 00000000000..74fa11944a6
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.aliased_ssa.IRSanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..9769ee11f99
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.expected
@@ -0,0 +1,22 @@
+missingOperand
+unexpectedOperand
+duplicateOperand
+missingPhiOperand
+missingOperandType
+duplicateChiOperand
+sideEffectWithoutPrimary
+instructionWithoutSuccessor
+ambiguousSuccessors
+unexplainedLoop
+unnecessaryPhiInstruction
+operandAcrossFunctions
+instructionWithoutUniqueBlock
+containsLoopOfForwardEdges
+lostReachability
+backEdgeCountMismatch
+useNotDominatedByDefinition
+missingCanonicalLanguageType
+multipleCanonicalLanguageTypes
+missingIRType
+multipleIRTypes
+missingCppType
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity.ql
new file mode 100644
index 00000000000..b3962e34648
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.aliased_ssa.internal.SSASanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..7c2d1faf639
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity_unsound.expected
@@ -0,0 +1,2 @@
+multipleOperandMemoryLocations
+missingVirtualVariableForMemoryLocation
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.ql b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.ql
new file mode 100644
index 00000000000..100f2815a58
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.ql
@@ -0,0 +1,6 @@
+/**
+ * @kind graph
+ */
+
+import semmle.code.cpp.ir.implementation.unaliased_ssa.PrintIR
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.expected
new file mode 100644
index 00000000000..83021d91c9c
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.expected
@@ -0,0 +1,1028 @@
+ssa.cpp:
+#   13| int ChiPhiNode(Point*, bool, bool)
+#   13|   Block 0
+#   13|     v13_1(void)           = EnterFunction               : 
+#   13|     mu13_2(unknown)       = AliasedDefinition           : 
+#   13|     mu13_3(unknown)       = UnmodeledDefinition         : 
+#   13|     r13_4(glval<Point *>) = VariableAddress[p]          : 
+#   13|     m13_5(Point *)        = InitializeParameter[p]      : &:r13_4
+#   13|     r13_6(Point *)        = Load                        : &:r13_4, m13_5
+#   13|     mu13_7(unknown)       = InitializeIndirection[p]    : &:r13_6
+#   13|     r13_8(glval<bool>)    = VariableAddress[which1]     : 
+#   13|     m13_9(bool)           = InitializeParameter[which1] : &:r13_8
+#   13|     r13_10(glval<bool>)   = VariableAddress[which2]     : 
+#   13|     m13_11(bool)          = InitializeParameter[which2] : &:r13_10
+#   14|     r14_1(glval<bool>)    = VariableAddress[which1]     : 
+#   14|     r14_2(bool)           = Load                        : &:r14_1, m13_9
+#   14|     v14_3(void)           = ConditionalBranch           : r14_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   15|   Block 1
+#   15|     r15_1(glval<Point *>) = VariableAddress[p] : 
+#   15|     r15_2(Point *)        = Load               : &:r15_1, m13_5
+#   15|     r15_3(glval<int>)     = FieldAddress[x]    : r15_2
+#   15|     r15_4(int)            = Load               : &:r15_3, ~mu13_3
+#   15|     r15_5(int)            = Constant[1]        : 
+#   15|     r15_6(int)            = Add                : r15_4, r15_5
+#   15|     mu15_7(int)           = Store              : &:r15_3, r15_6
+#-----|   Goto -> Block 3
+
+#   18|   Block 2
+#   18|     r18_1(glval<Point *>) = VariableAddress[p] : 
+#   18|     r18_2(Point *)        = Load               : &:r18_1, m13_5
+#   18|     r18_3(glval<int>)     = FieldAddress[y]    : r18_2
+#   18|     r18_4(int)            = Load               : &:r18_3, ~mu13_3
+#   18|     r18_5(int)            = Constant[1]        : 
+#   18|     r18_6(int)            = Add                : r18_4, r18_5
+#   18|     mu18_7(int)           = Store              : &:r18_3, r18_6
+#-----|   Goto -> Block 3
+
+#   21|   Block 3
+#   21|     r21_1(glval<bool>) = VariableAddress[which2] : 
+#   21|     r21_2(bool)        = Load                    : &:r21_1, m13_11
+#   21|     v21_3(void)        = ConditionalBranch       : r21_2
+#-----|   False -> Block 5
+#-----|   True -> Block 4
+
+#   22|   Block 4
+#   22|     r22_1(glval<Point *>) = VariableAddress[p] : 
+#   22|     r22_2(Point *)        = Load               : &:r22_1, m13_5
+#   22|     r22_3(glval<int>)     = FieldAddress[x]    : r22_2
+#   22|     r22_4(int)            = Load               : &:r22_3, ~mu13_3
+#   22|     r22_5(int)            = Constant[1]        : 
+#   22|     r22_6(int)            = Add                : r22_4, r22_5
+#   22|     mu22_7(int)           = Store              : &:r22_3, r22_6
+#-----|   Goto -> Block 6
+
+#   25|   Block 5
+#   25|     r25_1(glval<Point *>) = VariableAddress[p] : 
+#   25|     r25_2(Point *)        = Load               : &:r25_1, m13_5
+#   25|     r25_3(glval<int>)     = FieldAddress[y]    : r25_2
+#   25|     r25_4(int)            = Load               : &:r25_3, ~mu13_3
+#   25|     r25_5(int)            = Constant[1]        : 
+#   25|     r25_6(int)            = Add                : r25_4, r25_5
+#   25|     mu25_7(int)           = Store              : &:r25_3, r25_6
+#-----|   Goto -> Block 6
+
+#   28|   Block 6
+#   28|     r28_1(glval<int>)     = VariableAddress[#return] : 
+#   28|     r28_2(glval<Point *>) = VariableAddress[p]       : 
+#   28|     r28_3(Point *)        = Load                     : &:r28_2, m13_5
+#   28|     r28_4(glval<int>)     = FieldAddress[x]          : r28_3
+#   28|     r28_5(int)            = Load                     : &:r28_4, ~mu13_3
+#   28|     r28_6(glval<Point *>) = VariableAddress[p]       : 
+#   28|     r28_7(Point *)        = Load                     : &:r28_6, m13_5
+#   28|     r28_8(glval<int>)     = FieldAddress[y]          : r28_7
+#   28|     r28_9(int)            = Load                     : &:r28_8, ~mu13_3
+#   28|     r28_10(int)           = Add                      : r28_5, r28_9
+#   28|     m28_11(int)           = Store                    : &:r28_1, r28_10
+#   13|     v13_12(void)          = ReturnIndirection        : &:r13_6, ~mu13_3
+#   13|     r13_13(glval<int>)    = VariableAddress[#return] : 
+#   13|     v13_14(void)          = ReturnValue              : &:r13_13, m28_11
+#   13|     v13_15(void)          = UnmodeledUse             : mu*
+#   13|     v13_16(void)          = AliasedUse               : ~mu13_3
+#   13|     v13_17(void)          = ExitFunction             : 
+
+#   31| int UnreachableViaGoto()
+#   31|   Block 0
+#   31|     v31_1(void)       = EnterFunction            : 
+#   31|     mu31_2(unknown)   = AliasedDefinition        : 
+#   31|     mu31_3(unknown)   = UnmodeledDefinition      : 
+#   32|     v32_1(void)       = NoOp                     : 
+#   34|     v34_1(void)       = NoOp                     : 
+#   35|     r35_1(glval<int>) = VariableAddress[#return] : 
+#   35|     r35_2(int)        = Constant[0]              : 
+#   35|     m35_3(int)        = Store                    : &:r35_1, r35_2
+#   31|     r31_4(glval<int>) = VariableAddress[#return] : 
+#   31|     v31_5(void)       = ReturnValue              : &:r31_4, m35_3
+#   31|     v31_6(void)       = UnmodeledUse             : mu*
+#   31|     v31_7(void)       = AliasedUse               : ~mu31_3
+#   31|     v31_8(void)       = ExitFunction             : 
+
+#   38| int UnreachableIf(bool)
+#   38|   Block 0
+#   38|     v38_1(void)        = EnterFunction          : 
+#   38|     mu38_2(unknown)    = AliasedDefinition      : 
+#   38|     mu38_3(unknown)    = UnmodeledDefinition    : 
+#   38|     r38_4(glval<bool>) = VariableAddress[b]     : 
+#   38|     m38_5(bool)        = InitializeParameter[b] : &:r38_4
+#   39|     r39_1(glval<int>)  = VariableAddress[x]     : 
+#   39|     r39_2(int)         = Constant[5]            : 
+#   39|     m39_3(int)         = Store                  : &:r39_1, r39_2
+#   40|     r40_1(glval<int>)  = VariableAddress[y]     : 
+#   40|     r40_2(int)         = Constant[10]           : 
+#   40|     m40_3(int)         = Store                  : &:r40_1, r40_2
+#   41|     r41_1(glval<bool>) = VariableAddress[b]     : 
+#   41|     r41_2(bool)        = Load                   : &:r41_1, m38_5
+#   41|     v41_3(void)        = ConditionalBranch      : r41_2
+#-----|   False -> Block 5
+#-----|   True -> Block 2
+
+#   38|   Block 1
+#   38|     m38_6(int)        = Phi                      : from 3:m43_3, from 4:m46_3, from 6:m51_3, from 7:m54_3
+#   38|     r38_7(glval<int>) = VariableAddress[#return] : 
+#   38|     v38_8(void)       = ReturnValue              : &:r38_7, m38_6
+#   38|     v38_9(void)       = UnmodeledUse             : mu*
+#   38|     v38_10(void)      = AliasedUse               : ~mu38_3
+#   38|     v38_11(void)      = ExitFunction             : 
+
+#   42|   Block 2
+#   42|     r42_1(glval<int>) = VariableAddress[x] : 
+#   42|     r42_2(int)        = Load               : &:r42_1, m39_3
+#   42|     r42_3(glval<int>) = VariableAddress[y] : 
+#   42|     r42_4(int)        = Load               : &:r42_3, m40_3
+#   42|     r42_5(bool)       = CompareEQ          : r42_2, r42_4
+#   42|     v42_6(void)       = ConditionalBranch  : r42_5
+#-----|   False -> Block 4
+#-----|   True -> Block 3
+
+#   43|   Block 3
+#   43|     r43_1(glval<int>) = VariableAddress[#return] : 
+#   43|     r43_2(int)        = Constant[1]              : 
+#   43|     m43_3(int)        = Store                    : &:r43_1, r43_2
+#-----|   Goto -> Block 1
+
+#   46|   Block 4
+#   46|     r46_1(glval<int>) = VariableAddress[#return] : 
+#   46|     r46_2(int)        = Constant[0]              : 
+#   46|     m46_3(int)        = Store                    : &:r46_1, r46_2
+#-----|   Goto -> Block 1
+
+#   50|   Block 5
+#   50|     r50_1(glval<int>) = VariableAddress[x] : 
+#   50|     r50_2(int)        = Load               : &:r50_1, m39_3
+#   50|     r50_3(glval<int>) = VariableAddress[y] : 
+#   50|     r50_4(int)        = Load               : &:r50_3, m40_3
+#   50|     r50_5(bool)       = CompareLT          : r50_2, r50_4
+#   50|     v50_6(void)       = ConditionalBranch  : r50_5
+#-----|   False -> Block 7
+#-----|   True -> Block 6
+
+#   51|   Block 6
+#   51|     r51_1(glval<int>) = VariableAddress[#return] : 
+#   51|     r51_2(int)        = Constant[0]              : 
+#   51|     m51_3(int)        = Store                    : &:r51_1, r51_2
+#-----|   Goto -> Block 1
+
+#   54|   Block 7
+#   54|     r54_1(glval<int>) = VariableAddress[#return] : 
+#   54|     r54_2(int)        = Constant[1]              : 
+#   54|     m54_3(int)        = Store                    : &:r54_1, r54_2
+#-----|   Goto -> Block 1
+
+#   59| int DoWhileFalse()
+#   59|   Block 0
+#   59|     v59_1(void)       = EnterFunction       : 
+#   59|     mu59_2(unknown)   = AliasedDefinition   : 
+#   59|     mu59_3(unknown)   = UnmodeledDefinition : 
+#   60|     r60_1(glval<int>) = VariableAddress[i]  : 
+#   60|     r60_2(int)        = Constant[0]         : 
+#   60|     m60_3(int)        = Store               : &:r60_1, r60_2
+#   62|     r62_1(glval<int>) = VariableAddress[i]  : 
+#   62|     r62_2(int)        = Load                : &:r62_1, m60_3
+#   62|     r62_3(int)        = Constant[1]         : 
+#   62|     r62_4(int)        = Add                 : r62_2, r62_3
+#   62|     m62_5(int)        = Store               : &:r62_1, r62_4
+#   63|     r63_1(bool)       = Constant[0]         : 
+#   63|     v63_2(void)       = ConditionalBranch   : r63_1
+#-----|   False -> Block 1
+#-----|   True -> Block 2
+
+#   65|   Block 1
+#   65|     r65_1(glval<int>) = VariableAddress[#return] : 
+#   65|     r65_2(glval<int>) = VariableAddress[i]       : 
+#   65|     r65_3(int)        = Load                     : &:r65_2, m62_5
+#   65|     m65_4(int)        = Store                    : &:r65_1, r65_3
+#   59|     r59_4(glval<int>) = VariableAddress[#return] : 
+#   59|     v59_5(void)       = ReturnValue              : &:r59_4, m65_4
+#   59|     v59_6(void)       = UnmodeledUse             : mu*
+#   59|     v59_7(void)       = AliasedUse               : ~mu59_3
+#   59|     v59_8(void)       = ExitFunction             : 
+
+#   59|   Block 2
+#   59|     v59_9(void) = Unreached : 
+
+#   68| void chiNodeAtEndOfLoop(int, char*)
+#   68|   Block 0
+#   68|     v68_1(void)          = EnterFunction            : 
+#   68|     mu68_2(unknown)      = AliasedDefinition        : 
+#   68|     mu68_3(unknown)      = UnmodeledDefinition      : 
+#   68|     r68_4(glval<int>)    = VariableAddress[n]       : 
+#   68|     m68_5(int)           = InitializeParameter[n]   : &:r68_4
+#   68|     r68_6(glval<char *>) = VariableAddress[p]       : 
+#   68|     m68_7(char *)        = InitializeParameter[p]   : &:r68_6
+#   68|     r68_8(char *)        = Load                     : &:r68_6, m68_7
+#   68|     mu68_9(unknown)      = InitializeIndirection[p] : &:r68_8
+#-----|   Goto -> Block 3
+
+#   70|   Block 1
+#   70|     r70_1(char)          = Constant[0]        : 
+#   70|     r70_2(glval<char *>) = VariableAddress[p] : 
+#   70|     r70_3(char *)        = Load               : &:r70_2, m69_1
+#   70|     r70_4(int)           = Constant[1]        : 
+#   70|     r70_5(char *)        = PointerAdd[1]      : r70_3, r70_4
+#   70|     m70_6(char *)        = Store              : &:r70_2, r70_5
+#   70|     r70_7(glval<char>)   = CopyValue          : r70_3
+#   70|     mu70_8(char)         = Store              : &:r70_7, r70_1
+#-----|   Goto (back edge) -> Block 3
+
+#   71|   Block 2
+#   71|     v71_1(void)  = NoOp              : 
+#   68|     v68_10(void) = ReturnIndirection : &:r68_8, ~mu68_3
+#   68|     v68_11(void) = ReturnVoid        : 
+#   68|     v68_12(void) = UnmodeledUse      : mu*
+#   68|     v68_13(void) = AliasedUse        : ~mu68_3
+#   68|     v68_14(void) = ExitFunction      : 
+
+#   69|   Block 3
+#   69|     m69_1(char *)     = Phi                : from 0:m68_7, from 1:m70_6
+#   69|     m69_2(int)        = Phi                : from 0:m68_5, from 1:m69_7
+#   69|     r69_3(glval<int>) = VariableAddress[n] : 
+#   69|     r69_4(int)        = Load               : &:r69_3, m69_2
+#   69|     r69_5(int)        = Constant[1]        : 
+#   69|     r69_6(int)        = Sub                : r69_4, r69_5
+#   69|     m69_7(int)        = Store              : &:r69_3, r69_6
+#   69|     r69_8(int)        = Constant[0]        : 
+#   69|     r69_9(bool)       = CompareGT          : r69_4, r69_8
+#   69|     v69_10(void)      = ConditionalBranch  : r69_9
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   75| void ScalarPhi(bool)
+#   75|   Block 0
+#   75|     v75_1(void)        = EnterFunction          : 
+#   75|     mu75_2(unknown)    = AliasedDefinition      : 
+#   75|     mu75_3(unknown)    = UnmodeledDefinition    : 
+#   75|     r75_4(glval<bool>) = VariableAddress[b]     : 
+#   75|     m75_5(bool)        = InitializeParameter[b] : &:r75_4
+#   76|     r76_1(glval<int>)  = VariableAddress[x]     : 
+#   76|     r76_2(int)         = Constant[0]            : 
+#   76|     m76_3(int)         = Store                  : &:r76_1, r76_2
+#   77|     r77_1(glval<int>)  = VariableAddress[y]     : 
+#   77|     r77_2(int)         = Constant[1]            : 
+#   77|     m77_3(int)         = Store                  : &:r77_1, r77_2
+#   78|     r78_1(glval<int>)  = VariableAddress[z]     : 
+#   78|     r78_2(int)         = Constant[2]            : 
+#   78|     m78_3(int)         = Store                  : &:r78_1, r78_2
+#   79|     r79_1(glval<bool>) = VariableAddress[b]     : 
+#   79|     r79_2(bool)        = Load                   : &:r79_1, m75_5
+#   79|     v79_3(void)        = ConditionalBranch      : r79_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#   80|   Block 1
+#   80|     r80_1(int)        = Constant[3]        : 
+#   80|     r80_2(glval<int>) = VariableAddress[x] : 
+#   80|     m80_3(int)        = Store              : &:r80_2, r80_1
+#   81|     r81_1(int)        = Constant[4]        : 
+#   81|     r81_2(glval<int>) = VariableAddress[y] : 
+#   81|     m81_3(int)        = Store              : &:r81_2, r81_1
+#-----|   Goto -> Block 3
+
+#   84|   Block 2
+#   84|     r84_1(int)        = Constant[5]        : 
+#   84|     r84_2(glval<int>) = VariableAddress[x] : 
+#   84|     m84_3(int)        = Store              : &:r84_2, r84_1
+#-----|   Goto -> Block 3
+
+#   86|   Block 3
+#   86|     m86_1(int)        = Phi                      : from 1:m81_3, from 2:m77_3
+#   86|     m86_2(int)        = Phi                      : from 1:m80_3, from 2:m84_3
+#   86|     r86_3(glval<int>) = VariableAddress[x_merge] : 
+#   86|     r86_4(glval<int>) = VariableAddress[x]       : 
+#   86|     r86_5(int)        = Load                     : &:r86_4, m86_2
+#   86|     m86_6(int)        = Store                    : &:r86_3, r86_5
+#   87|     r87_1(glval<int>) = VariableAddress[y_merge] : 
+#   87|     r87_2(glval<int>) = VariableAddress[y]       : 
+#   87|     r87_3(int)        = Load                     : &:r87_2, m86_1
+#   87|     m87_4(int)        = Store                    : &:r87_1, r87_3
+#   88|     r88_1(glval<int>) = VariableAddress[z_merge] : 
+#   88|     r88_2(glval<int>) = VariableAddress[z]       : 
+#   88|     r88_3(int)        = Load                     : &:r88_2, m78_3
+#   88|     m88_4(int)        = Store                    : &:r88_1, r88_3
+#   89|     v89_1(void)       = NoOp                     : 
+#   75|     v75_6(void)       = ReturnVoid               : 
+#   75|     v75_7(void)       = UnmodeledUse             : mu*
+#   75|     v75_8(void)       = AliasedUse               : ~mu75_3
+#   75|     v75_9(void)       = ExitFunction             : 
+
+#   91| void MustExactlyOverlap(Point)
+#   91|   Block 0
+#   91|     v91_1(void)         = EnterFunction          : 
+#   91|     mu91_2(unknown)     = AliasedDefinition      : 
+#   91|     mu91_3(unknown)     = UnmodeledDefinition    : 
+#   91|     r91_4(glval<Point>) = VariableAddress[a]     : 
+#   91|     m91_5(Point)        = InitializeParameter[a] : &:r91_4
+#   92|     r92_1(glval<Point>) = VariableAddress[b]     : 
+#   92|     r92_2(glval<Point>) = VariableAddress[a]     : 
+#   92|     r92_3(Point)        = Load                   : &:r92_2, m91_5
+#   92|     m92_4(Point)        = Store                  : &:r92_1, r92_3
+#   93|     v93_1(void)         = NoOp                   : 
+#   91|     v91_6(void)         = ReturnVoid             : 
+#   91|     v91_7(void)         = UnmodeledUse           : mu*
+#   91|     v91_8(void)         = AliasedUse             : ~mu91_3
+#   91|     v91_9(void)         = ExitFunction           : 
+
+#   95| void MustExactlyOverlapEscaped(Point)
+#   95|   Block 0
+#   95|     v95_1(void)           = EnterFunction                : 
+#   95|     mu95_2(unknown)       = AliasedDefinition            : 
+#   95|     mu95_3(unknown)       = UnmodeledDefinition          : 
+#   95|     r95_4(glval<Point>)   = VariableAddress[a]           : 
+#   95|     mu95_5(Point)         = InitializeParameter[a]       : &:r95_4
+#   96|     r96_1(glval<Point>)   = VariableAddress[b]           : 
+#   96|     r96_2(glval<Point>)   = VariableAddress[a]           : 
+#   96|     r96_3(Point)          = Load                         : &:r96_2, ~mu95_3
+#   96|     m96_4(Point)          = Store                        : &:r96_1, r96_3
+#   97|     r97_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#   97|     r97_2(glval<Point>)   = VariableAddress[a]           : 
+#   97|     r97_3(Point *)        = CopyValue                    : r97_2
+#   97|     r97_4(void *)         = Convert                      : r97_3
+#   97|     v97_5(void)           = Call                         : func:r97_1, 0:r97_4
+#   97|     mu97_6(unknown)       = ^CallSideEffect              : ~mu95_3
+#   97|     v97_7(void)           = ^BufferReadSideEffect[0]     : &:r97_4, ~mu95_3
+#   97|     mu97_8(unknown)       = ^BufferMayWriteSideEffect[0] : &:r97_4
+#   98|     v98_1(void)           = NoOp                         : 
+#   95|     v95_6(void)           = ReturnVoid                   : 
+#   95|     v95_7(void)           = UnmodeledUse                 : mu*
+#   95|     v95_8(void)           = AliasedUse                   : ~mu95_3
+#   95|     v95_9(void)           = ExitFunction                 : 
+
+#  100| void MustTotallyOverlap(Point)
+#  100|   Block 0
+#  100|     v100_1(void)         = EnterFunction          : 
+#  100|     mu100_2(unknown)     = AliasedDefinition      : 
+#  100|     mu100_3(unknown)     = UnmodeledDefinition    : 
+#  100|     r100_4(glval<Point>) = VariableAddress[a]     : 
+#  100|     mu100_5(Point)       = InitializeParameter[a] : &:r100_4
+#  101|     r101_1(glval<int>)   = VariableAddress[x]     : 
+#  101|     r101_2(glval<Point>) = VariableAddress[a]     : 
+#  101|     r101_3(glval<int>)   = FieldAddress[x]        : r101_2
+#  101|     r101_4(int)          = Load                   : &:r101_3, ~mu100_3
+#  101|     m101_5(int)          = Store                  : &:r101_1, r101_4
+#  102|     r102_1(glval<int>)   = VariableAddress[y]     : 
+#  102|     r102_2(glval<Point>) = VariableAddress[a]     : 
+#  102|     r102_3(glval<int>)   = FieldAddress[y]        : r102_2
+#  102|     r102_4(int)          = Load                   : &:r102_3, ~mu100_3
+#  102|     m102_5(int)          = Store                  : &:r102_1, r102_4
+#  103|     v103_1(void)         = NoOp                   : 
+#  100|     v100_6(void)         = ReturnVoid             : 
+#  100|     v100_7(void)         = UnmodeledUse           : mu*
+#  100|     v100_8(void)         = AliasedUse             : ~mu100_3
+#  100|     v100_9(void)         = ExitFunction           : 
+
+#  105| void MustTotallyOverlapEscaped(Point)
+#  105|   Block 0
+#  105|     v105_1(void)           = EnterFunction                : 
+#  105|     mu105_2(unknown)       = AliasedDefinition            : 
+#  105|     mu105_3(unknown)       = UnmodeledDefinition          : 
+#  105|     r105_4(glval<Point>)   = VariableAddress[a]           : 
+#  105|     mu105_5(Point)         = InitializeParameter[a]       : &:r105_4
+#  106|     r106_1(glval<int>)     = VariableAddress[x]           : 
+#  106|     r106_2(glval<Point>)   = VariableAddress[a]           : 
+#  106|     r106_3(glval<int>)     = FieldAddress[x]              : r106_2
+#  106|     r106_4(int)            = Load                         : &:r106_3, ~mu105_3
+#  106|     m106_5(int)            = Store                        : &:r106_1, r106_4
+#  107|     r107_1(glval<int>)     = VariableAddress[y]           : 
+#  107|     r107_2(glval<Point>)   = VariableAddress[a]           : 
+#  107|     r107_3(glval<int>)     = FieldAddress[y]              : r107_2
+#  107|     r107_4(int)            = Load                         : &:r107_3, ~mu105_3
+#  107|     m107_5(int)            = Store                        : &:r107_1, r107_4
+#  108|     r108_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#  108|     r108_2(glval<Point>)   = VariableAddress[a]           : 
+#  108|     r108_3(Point *)        = CopyValue                    : r108_2
+#  108|     r108_4(void *)         = Convert                      : r108_3
+#  108|     v108_5(void)           = Call                         : func:r108_1, 0:r108_4
+#  108|     mu108_6(unknown)       = ^CallSideEffect              : ~mu105_3
+#  108|     v108_7(void)           = ^BufferReadSideEffect[0]     : &:r108_4, ~mu105_3
+#  108|     mu108_8(unknown)       = ^BufferMayWriteSideEffect[0] : &:r108_4
+#  109|     v109_1(void)           = NoOp                         : 
+#  105|     v105_6(void)           = ReturnVoid                   : 
+#  105|     v105_7(void)           = UnmodeledUse                 : mu*
+#  105|     v105_8(void)           = AliasedUse                   : ~mu105_3
+#  105|     v105_9(void)           = ExitFunction                 : 
+
+#  111| void MayPartiallyOverlap(int, int)
+#  111|   Block 0
+#  111|     v111_1(void)         = EnterFunction          : 
+#  111|     mu111_2(unknown)     = AliasedDefinition      : 
+#  111|     mu111_3(unknown)     = UnmodeledDefinition    : 
+#  111|     r111_4(glval<int>)   = VariableAddress[x]     : 
+#  111|     m111_5(int)          = InitializeParameter[x] : &:r111_4
+#  111|     r111_6(glval<int>)   = VariableAddress[y]     : 
+#  111|     m111_7(int)          = InitializeParameter[y] : &:r111_6
+#  112|     r112_1(glval<Point>) = VariableAddress[a]     : 
+#  112|     mu112_2(Point)       = Uninitialized[a]       : &:r112_1
+#  112|     r112_3(glval<int>)   = FieldAddress[x]        : r112_1
+#  112|     r112_4(glval<int>)   = VariableAddress[x]     : 
+#  112|     r112_5(int)          = Load                   : &:r112_4, m111_5
+#  112|     mu112_6(int)         = Store                  : &:r112_3, r112_5
+#  112|     r112_7(glval<int>)   = FieldAddress[y]        : r112_1
+#  112|     r112_8(glval<int>)   = VariableAddress[y]     : 
+#  112|     r112_9(int)          = Load                   : &:r112_8, m111_7
+#  112|     mu112_10(int)        = Store                  : &:r112_7, r112_9
+#  113|     r113_1(glval<Point>) = VariableAddress[b]     : 
+#  113|     r113_2(glval<Point>) = VariableAddress[a]     : 
+#  113|     r113_3(Point)        = Load                   : &:r113_2, ~mu111_3
+#  113|     m113_4(Point)        = Store                  : &:r113_1, r113_3
+#  114|     v114_1(void)         = NoOp                   : 
+#  111|     v111_8(void)         = ReturnVoid             : 
+#  111|     v111_9(void)         = UnmodeledUse           : mu*
+#  111|     v111_10(void)        = AliasedUse             : ~mu111_3
+#  111|     v111_11(void)        = ExitFunction           : 
+
+#  116| void MayPartiallyOverlapEscaped(int, int)
+#  116|   Block 0
+#  116|     v116_1(void)           = EnterFunction                : 
+#  116|     mu116_2(unknown)       = AliasedDefinition            : 
+#  116|     mu116_3(unknown)       = UnmodeledDefinition          : 
+#  116|     r116_4(glval<int>)     = VariableAddress[x]           : 
+#  116|     m116_5(int)            = InitializeParameter[x]       : &:r116_4
+#  116|     r116_6(glval<int>)     = VariableAddress[y]           : 
+#  116|     m116_7(int)            = InitializeParameter[y]       : &:r116_6
+#  117|     r117_1(glval<Point>)   = VariableAddress[a]           : 
+#  117|     mu117_2(Point)         = Uninitialized[a]             : &:r117_1
+#  117|     r117_3(glval<int>)     = FieldAddress[x]              : r117_1
+#  117|     r117_4(glval<int>)     = VariableAddress[x]           : 
+#  117|     r117_5(int)            = Load                         : &:r117_4, m116_5
+#  117|     mu117_6(int)           = Store                        : &:r117_3, r117_5
+#  117|     r117_7(glval<int>)     = FieldAddress[y]              : r117_1
+#  117|     r117_8(glval<int>)     = VariableAddress[y]           : 
+#  117|     r117_9(int)            = Load                         : &:r117_8, m116_7
+#  117|     mu117_10(int)          = Store                        : &:r117_7, r117_9
+#  118|     r118_1(glval<Point>)   = VariableAddress[b]           : 
+#  118|     r118_2(glval<Point>)   = VariableAddress[a]           : 
+#  118|     r118_3(Point)          = Load                         : &:r118_2, ~mu116_3
+#  118|     m118_4(Point)          = Store                        : &:r118_1, r118_3
+#  119|     r119_1(glval<unknown>) = FunctionAddress[Escape]      : 
+#  119|     r119_2(glval<Point>)   = VariableAddress[a]           : 
+#  119|     r119_3(Point *)        = CopyValue                    : r119_2
+#  119|     r119_4(void *)         = Convert                      : r119_3
+#  119|     v119_5(void)           = Call                         : func:r119_1, 0:r119_4
+#  119|     mu119_6(unknown)       = ^CallSideEffect              : ~mu116_3
+#  119|     v119_7(void)           = ^BufferReadSideEffect[0]     : &:r119_4, ~mu116_3
+#  119|     mu119_8(unknown)       = ^BufferMayWriteSideEffect[0] : &:r119_4
+#  120|     v120_1(void)           = NoOp                         : 
+#  116|     v116_8(void)           = ReturnVoid                   : 
+#  116|     v116_9(void)           = UnmodeledUse                 : mu*
+#  116|     v116_10(void)          = AliasedUse                   : ~mu116_3
+#  116|     v116_11(void)          = ExitFunction                 : 
+
+#  122| void MergeMustExactlyOverlap(bool, int, int)
+#  122|   Block 0
+#  122|     v122_1(void)         = EnterFunction           : 
+#  122|     mu122_2(unknown)     = AliasedDefinition       : 
+#  122|     mu122_3(unknown)     = UnmodeledDefinition     : 
+#  122|     r122_4(glval<bool>)  = VariableAddress[c]      : 
+#  122|     m122_5(bool)         = InitializeParameter[c]  : &:r122_4
+#  122|     r122_6(glval<int>)   = VariableAddress[x1]     : 
+#  122|     m122_7(int)          = InitializeParameter[x1] : &:r122_6
+#  122|     r122_8(glval<int>)   = VariableAddress[x2]     : 
+#  122|     m122_9(int)          = InitializeParameter[x2] : &:r122_8
+#  123|     r123_1(glval<Point>) = VariableAddress[a]      : 
+#  123|     mu123_2(Point)       = Uninitialized[a]        : &:r123_1
+#  123|     r123_3(glval<int>)   = FieldAddress[x]         : r123_1
+#  123|     r123_4(int)          = Constant[0]             : 
+#  123|     mu123_5(int)         = Store                   : &:r123_3, r123_4
+#  123|     r123_6(glval<int>)   = FieldAddress[y]         : r123_1
+#  123|     r123_7(int)          = Constant[0]             : 
+#  123|     mu123_8(int)         = Store                   : &:r123_6, r123_7
+#  124|     r124_1(glval<bool>)  = VariableAddress[c]      : 
+#  124|     r124_2(bool)         = Load                    : &:r124_1, m122_5
+#  124|     v124_3(void)         = ConditionalBranch       : r124_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  125|   Block 1
+#  125|     r125_1(glval<int>)   = VariableAddress[x1] : 
+#  125|     r125_2(int)          = Load                : &:r125_1, m122_7
+#  125|     r125_3(glval<Point>) = VariableAddress[a]  : 
+#  125|     r125_4(glval<int>)   = FieldAddress[x]     : r125_3
+#  125|     mu125_5(int)         = Store               : &:r125_4, r125_2
+#-----|   Goto -> Block 3
+
+#  128|   Block 2
+#  128|     r128_1(glval<int>)   = VariableAddress[x2] : 
+#  128|     r128_2(int)          = Load                : &:r128_1, m122_9
+#  128|     r128_3(glval<Point>) = VariableAddress[a]  : 
+#  128|     r128_4(glval<int>)   = FieldAddress[x]     : r128_3
+#  128|     mu128_5(int)         = Store               : &:r128_4, r128_2
+#-----|   Goto -> Block 3
+
+#  130|   Block 3
+#  130|     r130_1(glval<int>)   = VariableAddress[x] : 
+#  130|     r130_2(glval<Point>) = VariableAddress[a] : 
+#  130|     r130_3(glval<int>)   = FieldAddress[x]    : r130_2
+#  130|     r130_4(int)          = Load               : &:r130_3, ~mu122_3
+#  130|     m130_5(int)          = Store              : &:r130_1, r130_4
+#  131|     r131_1(glval<Point>) = VariableAddress[b] : 
+#  131|     r131_2(glval<Point>) = VariableAddress[a] : 
+#  131|     r131_3(Point)        = Load               : &:r131_2, ~mu122_3
+#  131|     m131_4(Point)        = Store              : &:r131_1, r131_3
+#  132|     v132_1(void)         = NoOp               : 
+#  122|     v122_10(void)        = ReturnVoid         : 
+#  122|     v122_11(void)        = UnmodeledUse       : mu*
+#  122|     v122_12(void)        = AliasedUse         : ~mu122_3
+#  122|     v122_13(void)        = ExitFunction       : 
+
+#  134| void MergeMustExactlyWithMustTotallyOverlap(bool, Point, int)
+#  134|   Block 0
+#  134|     v134_1(void)         = EnterFunction           : 
+#  134|     mu134_2(unknown)     = AliasedDefinition       : 
+#  134|     mu134_3(unknown)     = UnmodeledDefinition     : 
+#  134|     r134_4(glval<bool>)  = VariableAddress[c]      : 
+#  134|     m134_5(bool)         = InitializeParameter[c]  : &:r134_4
+#  134|     r134_6(glval<Point>) = VariableAddress[p]      : 
+#  134|     m134_7(Point)        = InitializeParameter[p]  : &:r134_6
+#  134|     r134_8(glval<int>)   = VariableAddress[x1]     : 
+#  134|     m134_9(int)          = InitializeParameter[x1] : &:r134_8
+#  135|     r135_1(glval<Point>) = VariableAddress[a]      : 
+#  135|     mu135_2(Point)       = Uninitialized[a]        : &:r135_1
+#  135|     r135_3(glval<int>)   = FieldAddress[x]         : r135_1
+#  135|     r135_4(int)          = Constant[0]             : 
+#  135|     mu135_5(int)         = Store                   : &:r135_3, r135_4
+#  135|     r135_6(glval<int>)   = FieldAddress[y]         : r135_1
+#  135|     r135_7(int)          = Constant[0]             : 
+#  135|     mu135_8(int)         = Store                   : &:r135_6, r135_7
+#  136|     r136_1(glval<bool>)  = VariableAddress[c]      : 
+#  136|     r136_2(bool)         = Load                    : &:r136_1, m134_5
+#  136|     v136_3(void)         = ConditionalBranch       : r136_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  137|   Block 1
+#  137|     r137_1(glval<int>)   = VariableAddress[x1] : 
+#  137|     r137_2(int)          = Load                : &:r137_1, m134_9
+#  137|     r137_3(glval<Point>) = VariableAddress[a]  : 
+#  137|     r137_4(glval<int>)   = FieldAddress[x]     : r137_3
+#  137|     mu137_5(int)         = Store               : &:r137_4, r137_2
+#-----|   Goto -> Block 3
+
+#  140|   Block 2
+#  140|     r140_1(glval<Point>) = VariableAddress[p] : 
+#  140|     r140_2(Point)        = Load               : &:r140_1, m134_7
+#  140|     r140_3(glval<Point>) = VariableAddress[a] : 
+#  140|     mu140_4(Point)       = Store              : &:r140_3, r140_2
+#-----|   Goto -> Block 3
+
+#  142|   Block 3
+#  142|     r142_1(glval<int>)   = VariableAddress[x] : 
+#  142|     r142_2(glval<Point>) = VariableAddress[a] : 
+#  142|     r142_3(glval<int>)   = FieldAddress[x]    : r142_2
+#  142|     r142_4(int)          = Load               : &:r142_3, ~mu134_3
+#  142|     m142_5(int)          = Store              : &:r142_1, r142_4
+#  143|     v143_1(void)         = NoOp               : 
+#  134|     v134_10(void)        = ReturnVoid         : 
+#  134|     v134_11(void)        = UnmodeledUse       : mu*
+#  134|     v134_12(void)        = AliasedUse         : ~mu134_3
+#  134|     v134_13(void)        = ExitFunction       : 
+
+#  145| void MergeMustExactlyWithMayPartiallyOverlap(bool, Point, int)
+#  145|   Block 0
+#  145|     v145_1(void)         = EnterFunction           : 
+#  145|     mu145_2(unknown)     = AliasedDefinition       : 
+#  145|     mu145_3(unknown)     = UnmodeledDefinition     : 
+#  145|     r145_4(glval<bool>)  = VariableAddress[c]      : 
+#  145|     m145_5(bool)         = InitializeParameter[c]  : &:r145_4
+#  145|     r145_6(glval<Point>) = VariableAddress[p]      : 
+#  145|     m145_7(Point)        = InitializeParameter[p]  : &:r145_6
+#  145|     r145_8(glval<int>)   = VariableAddress[x1]     : 
+#  145|     m145_9(int)          = InitializeParameter[x1] : &:r145_8
+#  146|     r146_1(glval<Point>) = VariableAddress[a]      : 
+#  146|     mu146_2(Point)       = Uninitialized[a]        : &:r146_1
+#  146|     r146_3(glval<int>)   = FieldAddress[x]         : r146_1
+#  146|     r146_4(int)          = Constant[0]             : 
+#  146|     mu146_5(int)         = Store                   : &:r146_3, r146_4
+#  146|     r146_6(glval<int>)   = FieldAddress[y]         : r146_1
+#  146|     r146_7(int)          = Constant[0]             : 
+#  146|     mu146_8(int)         = Store                   : &:r146_6, r146_7
+#  147|     r147_1(glval<bool>)  = VariableAddress[c]      : 
+#  147|     r147_2(bool)         = Load                    : &:r147_1, m145_5
+#  147|     v147_3(void)         = ConditionalBranch       : r147_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  148|   Block 1
+#  148|     r148_1(glval<int>)   = VariableAddress[x1] : 
+#  148|     r148_2(int)          = Load                : &:r148_1, m145_9
+#  148|     r148_3(glval<Point>) = VariableAddress[a]  : 
+#  148|     r148_4(glval<int>)   = FieldAddress[x]     : r148_3
+#  148|     mu148_5(int)         = Store               : &:r148_4, r148_2
+#-----|   Goto -> Block 3
+
+#  151|   Block 2
+#  151|     r151_1(glval<Point>) = VariableAddress[p] : 
+#  151|     r151_2(Point)        = Load               : &:r151_1, m145_7
+#  151|     r151_3(glval<Point>) = VariableAddress[a] : 
+#  151|     mu151_4(Point)       = Store              : &:r151_3, r151_2
+#-----|   Goto -> Block 3
+
+#  153|   Block 3
+#  153|     r153_1(glval<Point>) = VariableAddress[b] : 
+#  153|     r153_2(glval<Point>) = VariableAddress[a] : 
+#  153|     r153_3(Point)        = Load               : &:r153_2, ~mu145_3
+#  153|     m153_4(Point)        = Store              : &:r153_1, r153_3
+#  154|     v154_1(void)         = NoOp               : 
+#  145|     v145_10(void)        = ReturnVoid         : 
+#  145|     v145_11(void)        = UnmodeledUse       : mu*
+#  145|     v145_12(void)        = AliasedUse         : ~mu145_3
+#  145|     v145_13(void)        = ExitFunction       : 
+
+#  156| void MergeMustTotallyOverlapWithMayPartiallyOverlap(bool, Rect, int)
+#  156|   Block 0
+#  156|     v156_1(void)         = EnterFunction             : 
+#  156|     mu156_2(unknown)     = AliasedDefinition         : 
+#  156|     mu156_3(unknown)     = UnmodeledDefinition       : 
+#  156|     r156_4(glval<bool>)  = VariableAddress[c]        : 
+#  156|     m156_5(bool)         = InitializeParameter[c]    : &:r156_4
+#  156|     r156_6(glval<Rect>)  = VariableAddress[r]        : 
+#  156|     m156_7(Rect)         = InitializeParameter[r]    : &:r156_6
+#  156|     r156_8(glval<int>)   = VariableAddress[x1]       : 
+#  156|     m156_9(int)          = InitializeParameter[x1]   : &:r156_8
+#  157|     r157_1(glval<Rect>)  = VariableAddress[a]        : 
+#  157|     mu157_2(Rect)        = Uninitialized[a]          : &:r157_1
+#  157|     r157_3(glval<Point>) = FieldAddress[topLeft]     : r157_1
+#  157|     r157_4(Point)        = Constant[0]               : 
+#  157|     mu157_5(Point)       = Store                     : &:r157_3, r157_4
+#  157|     r157_6(glval<Point>) = FieldAddress[bottomRight] : r157_1
+#  157|     r157_7(Point)        = Constant[0]               : 
+#  157|     mu157_8(Point)       = Store                     : &:r157_6, r157_7
+#  158|     r158_1(glval<bool>)  = VariableAddress[c]        : 
+#  158|     r158_2(bool)         = Load                      : &:r158_1, m156_5
+#  158|     v158_3(void)         = ConditionalBranch         : r158_2
+#-----|   False -> Block 2
+#-----|   True -> Block 1
+
+#  159|   Block 1
+#  159|     r159_1(glval<int>)   = VariableAddress[x1]   : 
+#  159|     r159_2(int)          = Load                  : &:r159_1, m156_9
+#  159|     r159_3(glval<Rect>)  = VariableAddress[a]    : 
+#  159|     r159_4(glval<Point>) = FieldAddress[topLeft] : r159_3
+#  159|     r159_5(glval<int>)   = FieldAddress[x]       : r159_4
+#  159|     mu159_6(int)         = Store                 : &:r159_5, r159_2
+#-----|   Goto -> Block 3
+
+#  162|   Block 2
+#  162|     r162_1(glval<Rect>) = VariableAddress[r] : 
+#  162|     r162_2(Rect)        = Load               : &:r162_1, m156_7
+#  162|     r162_3(glval<Rect>) = VariableAddress[a] : 
+#  162|     mu162_4(Rect)       = Store              : &:r162_3, r162_2
+#-----|   Goto -> Block 3
+
+#  164|   Block 3
+#  164|     r164_1(glval<Point>) = VariableAddress[b]    : 
+#  164|     r164_2(glval<Rect>)  = VariableAddress[a]    : 
+#  164|     r164_3(glval<Point>) = FieldAddress[topLeft] : r164_2
+#  164|     r164_4(Point)        = Load                  : &:r164_3, ~mu156_3
+#  164|     m164_5(Point)        = Store                 : &:r164_1, r164_4
+#  165|     v165_1(void)         = NoOp                  : 
+#  156|     v156_10(void)        = ReturnVoid            : 
+#  156|     v156_11(void)        = UnmodeledUse          : mu*
+#  156|     v156_12(void)        = AliasedUse            : ~mu156_3
+#  156|     v156_13(void)        = ExitFunction          : 
+
+#  171| void WrapperStruct(Wrapper)
+#  171|   Block 0
+#  171|     v171_1(void)           = EnterFunction          : 
+#  171|     mu171_2(unknown)       = AliasedDefinition      : 
+#  171|     mu171_3(unknown)       = UnmodeledDefinition    : 
+#  171|     r171_4(glval<Wrapper>) = VariableAddress[w]     : 
+#  171|     mu171_5(Wrapper)       = InitializeParameter[w] : &:r171_4
+#  172|     r172_1(glval<Wrapper>) = VariableAddress[x]     : 
+#  172|     r172_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  172|     r172_3(Wrapper)        = Load                   : &:r172_2, ~mu171_3
+#  172|     m172_4(Wrapper)        = Store                  : &:r172_1, r172_3
+#  173|     r173_1(glval<int>)     = VariableAddress[a]     : 
+#  173|     r173_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  173|     r173_3(glval<int>)     = FieldAddress[f]        : r173_2
+#  173|     r173_4(int)            = Load                   : &:r173_3, ~mu171_3
+#  173|     m173_5(int)            = Store                  : &:r173_1, r173_4
+#  174|     r174_1(int)            = Constant[5]            : 
+#  174|     r174_2(glval<Wrapper>) = VariableAddress[w]     : 
+#  174|     r174_3(glval<int>)     = FieldAddress[f]        : r174_2
+#  174|     mu174_4(int)           = Store                  : &:r174_3, r174_1
+#  175|     r175_1(glval<Wrapper>) = VariableAddress[w]     : 
+#  175|     r175_2(glval<int>)     = FieldAddress[f]        : r175_1
+#  175|     r175_3(int)            = Load                   : &:r175_2, ~mu171_3
+#  175|     r175_4(glval<int>)     = VariableAddress[a]     : 
+#  175|     m175_5(int)            = Store                  : &:r175_4, r175_3
+#  176|     r176_1(glval<Wrapper>) = VariableAddress[w]     : 
+#  176|     r176_2(Wrapper)        = Load                   : &:r176_1, ~mu171_3
+#  176|     r176_3(glval<Wrapper>) = VariableAddress[x]     : 
+#  176|     m176_4(Wrapper)        = Store                  : &:r176_3, r176_2
+#  177|     v177_1(void)           = NoOp                   : 
+#  171|     v171_6(void)           = ReturnVoid             : 
+#  171|     v171_7(void)           = UnmodeledUse           : mu*
+#  171|     v171_8(void)           = AliasedUse             : ~mu171_3
+#  171|     v171_9(void)           = ExitFunction           : 
+
+#  179| int AsmStmt(int*)
+#  179|   Block 0
+#  179|     v179_1(void)         = EnterFunction            : 
+#  179|     mu179_2(unknown)     = AliasedDefinition        : 
+#  179|     mu179_3(unknown)     = UnmodeledDefinition      : 
+#  179|     r179_4(glval<int *>) = VariableAddress[p]       : 
+#  179|     m179_5(int *)        = InitializeParameter[p]   : &:r179_4
+#  179|     r179_6(int *)        = Load                     : &:r179_4, m179_5
+#  179|     mu179_7(unknown)     = InitializeIndirection[p] : &:r179_6
+#  180|     mu180_1(unknown)     = InlineAsm                : ~mu179_3
+#  181|     r181_1(glval<int>)   = VariableAddress[#return] : 
+#  181|     r181_2(glval<int *>) = VariableAddress[p]       : 
+#  181|     r181_3(int *)        = Load                     : &:r181_2, m179_5
+#  181|     r181_4(int)          = Load                     : &:r181_3, ~mu179_3
+#  181|     m181_5(int)          = Store                    : &:r181_1, r181_4
+#  179|     v179_8(void)         = ReturnIndirection        : &:r179_6, ~mu179_3
+#  179|     r179_9(glval<int>)   = VariableAddress[#return] : 
+#  179|     v179_10(void)        = ReturnValue              : &:r179_9, m181_5
+#  179|     v179_11(void)        = UnmodeledUse             : mu*
+#  179|     v179_12(void)        = AliasedUse               : ~mu179_3
+#  179|     v179_13(void)        = ExitFunction             : 
+
+#  184| void AsmStmtWithOutputs(unsigned int&, unsigned int&, unsigned int&, unsigned int&)
+#  184|   Block 0
+#  184|     v184_1(void)                   = EnterFunction            : 
+#  184|     mu184_2(unknown)               = AliasedDefinition        : 
+#  184|     mu184_3(unknown)               = UnmodeledDefinition      : 
+#  184|     r184_4(glval<unsigned int &>)  = VariableAddress[a]       : 
+#  184|     m184_5(unsigned int &)         = InitializeParameter[a]   : &:r184_4
+#  184|     r184_6(unsigned int &)         = Load                     : &:r184_4, m184_5
+#  184|     mu184_7(unknown)               = InitializeIndirection[a] : &:r184_6
+#  184|     r184_8(glval<unsigned int &>)  = VariableAddress[b]       : 
+#  184|     m184_9(unsigned int &)         = InitializeParameter[b]   : &:r184_8
+#  184|     r184_10(unsigned int &)        = Load                     : &:r184_8, m184_9
+#  184|     mu184_11(unknown)              = InitializeIndirection[b] : &:r184_10
+#  184|     r184_12(glval<unsigned int &>) = VariableAddress[c]       : 
+#  184|     m184_13(unsigned int &)        = InitializeParameter[c]   : &:r184_12
+#  184|     r184_14(unsigned int &)        = Load                     : &:r184_12, m184_13
+#  184|     mu184_15(unknown)              = InitializeIndirection[c] : &:r184_14
+#  184|     r184_16(glval<unsigned int &>) = VariableAddress[d]       : 
+#  184|     m184_17(unsigned int &)        = InitializeParameter[d]   : &:r184_16
+#  184|     r184_18(unsigned int &)        = Load                     : &:r184_16, m184_17
+#  184|     mu184_19(unknown)              = InitializeIndirection[d] : &:r184_18
+#  189|     r189_1(glval<unsigned int &>)  = VariableAddress[a]       : 
+#  189|     r189_2(unsigned int &)         = Load                     : &:r189_1, m184_5
+#  189|     r189_3(glval<unsigned int>)    = CopyValue                : r189_2
+#  189|     r189_4(glval<unsigned int &>)  = VariableAddress[b]       : 
+#  189|     r189_5(unsigned int &)         = Load                     : &:r189_4, m184_9
+#  189|     r189_6(glval<unsigned int>)    = CopyValue                : r189_5
+#  190|     r190_1(glval<unsigned int &>)  = VariableAddress[c]       : 
+#  190|     r190_2(unsigned int &)         = Load                     : &:r190_1, m184_13
+#  190|     r190_3(unsigned int)           = Load                     : &:r190_2, ~mu184_3
+#  190|     r190_4(glval<unsigned int &>)  = VariableAddress[d]       : 
+#  190|     r190_5(unsigned int &)         = Load                     : &:r190_4, m184_17
+#  190|     r190_6(unsigned int)           = Load                     : &:r190_5, ~mu184_3
+#  186|     mu186_1(unknown)               = InlineAsm                : ~mu184_3, 0:r189_3, 1:r189_6, 2:r190_3, 3:r190_6
+#  192|     v192_1(void)                   = NoOp                     : 
+#  184|     v184_20(void)                  = ReturnIndirection        : &:r184_6, ~mu184_3
+#  184|     v184_21(void)                  = ReturnIndirection        : &:r184_10, ~mu184_3
+#  184|     v184_22(void)                  = ReturnIndirection        : &:r184_14, ~mu184_3
+#  184|     v184_23(void)                  = ReturnIndirection        : &:r184_18, ~mu184_3
+#  184|     v184_24(void)                  = ReturnVoid               : 
+#  184|     v184_25(void)                  = UnmodeledUse             : mu*
+#  184|     v184_26(void)                  = AliasedUse               : ~mu184_3
+#  184|     v184_27(void)                  = ExitFunction             : 
+
+#  198| int PureFunctions(char*, char*, int)
+#  198|   Block 0
+#  198|     v198_1(void)           = EnterFunction               : 
+#  198|     mu198_2(unknown)       = AliasedDefinition           : 
+#  198|     mu198_3(unknown)       = UnmodeledDefinition         : 
+#  198|     r198_4(glval<char *>)  = VariableAddress[str1]       : 
+#  198|     m198_5(char *)         = InitializeParameter[str1]   : &:r198_4
+#  198|     r198_6(char *)         = Load                        : &:r198_4, m198_5
+#  198|     mu198_7(unknown)       = InitializeIndirection[str1] : &:r198_6
+#  198|     r198_8(glval<char *>)  = VariableAddress[str2]       : 
+#  198|     m198_9(char *)         = InitializeParameter[str2]   : &:r198_8
+#  198|     r198_10(char *)        = Load                        : &:r198_8, m198_9
+#  198|     mu198_11(unknown)      = InitializeIndirection[str2] : &:r198_10
+#  198|     r198_12(glval<int>)    = VariableAddress[x]          : 
+#  198|     m198_13(int)           = InitializeParameter[x]      : &:r198_12
+#  199|     r199_1(glval<int>)     = VariableAddress[ret]        : 
+#  199|     r199_2(glval<unknown>) = FunctionAddress[strcmp]     : 
+#  199|     r199_3(glval<char *>)  = VariableAddress[str1]       : 
+#  199|     r199_4(char *)         = Load                        : &:r199_3, m198_5
+#  199|     r199_5(char *)         = Convert                     : r199_4
+#  199|     r199_6(glval<char *>)  = VariableAddress[str2]       : 
+#  199|     r199_7(char *)         = Load                        : &:r199_6, m198_9
+#  199|     r199_8(char *)         = Convert                     : r199_7
+#  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
+#  199|     v199_10(void)          = ^CallReadSideEffect         : ~mu198_3
+#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~mu198_3
+#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~mu198_3
+#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
+#  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
+#  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
+#  200|     r200_3(char *)         = Load                        : &:r200_2, m198_5
+#  200|     r200_4(char *)         = Convert                     : r200_3
+#  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
+#  200|     v200_6(void)           = ^CallReadSideEffect         : ~mu198_3
+#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~mu198_3
+#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
+#  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
+#  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
+#  201|     r201_3(int)            = Load                        : &:r201_2, m198_13
+#  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
+#  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_7(int)            = Add                         : r201_6, r201_4
+#  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
+#  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 
+#  202|     r202_2(glval<int>)     = VariableAddress[ret]        : 
+#  202|     r202_3(int)            = Load                        : &:r202_2, m201_8
+#  202|     m202_4(int)            = Store                       : &:r202_1, r202_3
+#  198|     v198_14(void)          = ReturnIndirection           : &:r198_6, ~mu198_3
+#  198|     v198_15(void)          = ReturnIndirection           : &:r198_10, ~mu198_3
+#  198|     r198_16(glval<int>)    = VariableAddress[#return]    : 
+#  198|     v198_17(void)          = ReturnValue                 : &:r198_16, m202_4
+#  198|     v198_18(void)          = UnmodeledUse                : mu*
+#  198|     v198_19(void)          = AliasedUse                  : ~mu198_3
+#  198|     v198_20(void)          = ExitFunction                : 
+
+#  207| int ModeledCallTarget(int)
+#  207|   Block 0
+#  207|     v207_1(void)           = EnterFunction                      : 
+#  207|     mu207_2(unknown)       = AliasedDefinition                  : 
+#  207|     mu207_3(unknown)       = UnmodeledDefinition                : 
+#  207|     r207_4(glval<int>)     = VariableAddress[x]                 : 
+#  207|     mu207_5(int)           = InitializeParameter[x]             : &:r207_4
+#  208|     r208_1(glval<int>)     = VariableAddress[y]                 : 
+#  208|     mu208_2(int)           = Uninitialized[y]                   : &:r208_1
+#  209|     r209_1(glval<unknown>) = FunctionAddress[memcpy]            : 
+#  209|     r209_2(glval<int>)     = VariableAddress[y]                 : 
+#  209|     r209_3(int *)          = CopyValue                          : r209_2
+#  209|     r209_4(void *)         = Convert                            : r209_3
+#  209|     r209_5(glval<int>)     = VariableAddress[x]                 : 
+#  209|     r209_6(int *)          = CopyValue                          : r209_5
+#  209|     r209_7(void *)         = Convert                            : r209_6
+#  209|     r209_8(int)            = Constant[4]                        : 
+#  209|     r209_9(void *)         = Call                               : func:r209_1, 0:r209_4, 1:r209_7, 2:r209_8
+#  209|     v209_10(void)          = ^SizedBufferReadSideEffect[1]      : &:r209_7, r209_8, ~mu207_3
+#  209|     mu209_11(unknown)      = ^SizedBufferMustWriteSideEffect[0] : &:r209_4, r209_8
+#  210|     r210_1(glval<int>)     = VariableAddress[#return]           : 
+#  210|     r210_2(glval<int>)     = VariableAddress[y]                 : 
+#  210|     r210_3(int)            = Load                               : &:r210_2, ~mu207_3
+#  210|     m210_4(int)            = Store                              : &:r210_1, r210_3
+#  207|     r207_6(glval<int>)     = VariableAddress[#return]           : 
+#  207|     v207_7(void)           = ReturnValue                        : &:r207_6, m210_4
+#  207|     v207_8(void)           = UnmodeledUse                       : mu*
+#  207|     v207_9(void)           = AliasedUse                         : ~mu207_3
+#  207|     v207_10(void)          = ExitFunction                       : 
+
+#  213| void InitArray()
+#  213|   Block 0
+#  213|     v213_1(void)            = EnterFunction            : 
+#  213|     mu213_2(unknown)        = AliasedDefinition        : 
+#  213|     mu213_3(unknown)        = UnmodeledDefinition      : 
+#  214|     r214_1(glval<char[32]>) = VariableAddress[a_pad]   : 
+#  214|     r214_2(glval<char[32]>) = StringConstant[""]       : 
+#  214|     r214_3(char[32])        = Load                     : &:r214_2, ~mu213_3
+#  214|     m214_4(char[32])        = Store                    : &:r214_1, r214_3
+#  215|     r215_1(glval<char[4]>)  = VariableAddress[a_nopad] : 
+#  215|     r215_2(glval<char[4]>)  = StringConstant["foo"]    : 
+#  215|     r215_3(char[4])         = Load                     : &:r215_2, ~mu213_3
+#  215|     m215_4(char[4])         = Store                    : &:r215_1, r215_3
+#  216|     r216_1(glval<char[5]>)  = VariableAddress[a_infer] : 
+#  216|     r216_2(glval<char[5]>)  = StringConstant["blah"]   : 
+#  216|     r216_3(char[5])         = Load                     : &:r216_2, ~mu213_3
+#  216|     m216_4(char[5])         = Store                    : &:r216_1, r216_3
+#  217|     r217_1(glval<char[2]>)  = VariableAddress[b]       : 
+#  217|     m217_2(char[2])         = Uninitialized[b]         : &:r217_1
+#  218|     r218_1(glval<char[2]>)  = VariableAddress[c]       : 
+#  218|     mu218_2(char[2])        = Uninitialized[c]         : &:r218_1
+#  218|     r218_3(int)             = Constant[0]              : 
+#  218|     r218_4(glval<char>)     = PointerAdd[1]            : r218_1, r218_3
+#  218|     r218_5(unknown[2])      = Constant[0]              : 
+#  218|     mu218_6(unknown[2])     = Store                    : &:r218_4, r218_5
+#  219|     r219_1(glval<char[2]>)  = VariableAddress[d]       : 
+#  219|     mu219_2(char[2])        = Uninitialized[d]         : &:r219_1
+#  219|     r219_3(int)             = Constant[0]              : 
+#  219|     r219_4(glval<char>)     = PointerAdd[1]            : r219_1, r219_3
+#  219|     r219_5(char)            = Constant[0]              : 
+#  219|     mu219_6(char)           = Store                    : &:r219_4, r219_5
+#  219|     r219_7(int)             = Constant[1]              : 
+#  219|     r219_8(glval<char>)     = PointerAdd[1]            : r219_1, r219_7
+#  219|     r219_9(char)            = Constant[0]              : 
+#  219|     mu219_10(char)          = Store                    : &:r219_8, r219_9
+#  220|     r220_1(glval<char[2]>)  = VariableAddress[e]       : 
+#  220|     mu220_2(char[2])        = Uninitialized[e]         : &:r220_1
+#  220|     r220_3(int)             = Constant[0]              : 
+#  220|     r220_4(glval<char>)     = PointerAdd[1]            : r220_1, r220_3
+#  220|     r220_5(char)            = Constant[0]              : 
+#  220|     mu220_6(char)           = Store                    : &:r220_4, r220_5
+#  220|     r220_7(int)             = Constant[1]              : 
+#  220|     r220_8(glval<char>)     = PointerAdd[1]            : r220_1, r220_7
+#  220|     r220_9(char)            = Constant[1]              : 
+#  220|     mu220_10(char)          = Store                    : &:r220_8, r220_9
+#  221|     r221_1(glval<char[3]>)  = VariableAddress[f]       : 
+#  221|     mu221_2(char[3])        = Uninitialized[f]         : &:r221_1
+#  221|     r221_3(int)             = Constant[0]              : 
+#  221|     r221_4(glval<char>)     = PointerAdd[1]            : r221_1, r221_3
+#  221|     r221_5(char)            = Constant[0]              : 
+#  221|     mu221_6(char)           = Store                    : &:r221_4, r221_5
+#  221|     r221_7(int)             = Constant[1]              : 
+#  221|     r221_8(glval<char>)     = PointerAdd[1]            : r221_1, r221_7
+#  221|     r221_9(unknown[2])      = Constant[0]              : 
+#  221|     mu221_10(unknown[2])    = Store                    : &:r221_8, r221_9
+#  222|     v222_1(void)            = NoOp                     : 
+#  213|     v213_4(void)            = ReturnVoid               : 
+#  213|     v213_5(void)            = UnmodeledUse             : mu*
+#  213|     v213_6(void)            = AliasedUse               : ~mu213_3
+#  213|     v213_7(void)            = ExitFunction             : 
+
+#  226| char StringLiteralAliasing()
+#  226|   Block 0
+#  226|     v226_1(void)           = EnterFunction                 : 
+#  226|     mu226_2(unknown)       = AliasedDefinition             : 
+#  226|     mu226_3(unknown)       = UnmodeledDefinition           : 
+#  227|     r227_1(glval<unknown>) = FunctionAddress[ExternalFunc] : 
+#  227|     v227_2(void)           = Call                          : func:r227_1
+#  227|     mu227_3(unknown)       = ^CallSideEffect               : ~mu226_3
+#  229|     r229_1(glval<char *>)  = VariableAddress[s]            : 
+#  229|     r229_2(glval<char[8]>) = StringConstant["Literal"]     : 
+#  229|     r229_3(char *)         = Convert                       : r229_2
+#  229|     m229_4(char *)         = Store                         : &:r229_1, r229_3
+#  230|     r230_1(glval<char>)    = VariableAddress[#return]      : 
+#  230|     r230_2(glval<char *>)  = VariableAddress[s]            : 
+#  230|     r230_3(char *)         = Load                          : &:r230_2, m229_4
+#  230|     r230_4(int)            = Constant[2]                   : 
+#  230|     r230_5(glval<char>)    = PointerAdd[1]                 : r230_3, r230_4
+#  230|     r230_6(char)           = Load                          : &:r230_5, ~mu226_3
+#  230|     m230_7(char)           = Store                         : &:r230_1, r230_6
+#  226|     r226_4(glval<char>)    = VariableAddress[#return]      : 
+#  226|     v226_5(void)           = ReturnValue                   : &:r226_4, m230_7
+#  226|     v226_6(void)           = UnmodeledUse                  : mu*
+#  226|     v226_7(void)           = AliasedUse                    : ~mu226_3
+#  226|     v226_8(void)           = ExitFunction                  : 
+
+#  235| void Constructible::Constructible(int)
+#  235|   Block 0
+#  235|     v235_1(void)                 = EnterFunction          : 
+#  235|     mu235_2(unknown)             = AliasedDefinition      : 
+#  235|     mu235_3(unknown)             = UnmodeledDefinition    : 
+#  235|     r235_4(glval<Constructible>) = InitializeThis         : 
+#  235|     r235_5(glval<int>)           = VariableAddress[x]     : 
+#  235|     m235_6(int)                  = InitializeParameter[x] : &:r235_5
+#  235|     v235_7(void)                 = NoOp                   : 
+#  235|     v235_8(void)                 = ReturnVoid             : 
+#  235|     v235_9(void)                 = UnmodeledUse           : mu*
+#  235|     v235_10(void)                = AliasedUse             : ~mu235_3
+#  235|     v235_11(void)                = ExitFunction           : 
+
+#  236| void Constructible::g()
+#  236|   Block 0
+#  236|     v236_1(void)                 = EnterFunction       : 
+#  236|     mu236_2(unknown)             = AliasedDefinition   : 
+#  236|     mu236_3(unknown)             = UnmodeledDefinition : 
+#  236|     r236_4(glval<Constructible>) = InitializeThis      : 
+#  236|     v236_5(void)                 = NoOp                : 
+#  236|     v236_6(void)                 = ReturnVoid          : 
+#  236|     v236_7(void)                 = UnmodeledUse        : mu*
+#  236|     v236_8(void)                 = AliasedUse          : ~mu236_3
+#  236|     v236_9(void)                 = ExitFunction        : 
+
+#  239| void ExplicitConstructorCalls()
+#  239|   Block 0
+#  239|     v239_1(void)                 = EnterFunction                   : 
+#  239|     mu239_2(unknown)             = AliasedDefinition               : 
+#  239|     mu239_3(unknown)             = UnmodeledDefinition             : 
+#  240|     r240_1(glval<Constructible>) = VariableAddress[c]              : 
+#  240|     mu240_2(Constructible)       = Uninitialized[c]                : &:r240_1
+#  240|     r240_3(glval<unknown>)       = FunctionAddress[Constructible]  : 
+#  240|     r240_4(int)                  = Constant[1]                     : 
+#  240|     v240_5(void)                 = Call                            : func:r240_3, this:r240_1, 0:r240_4
+#  240|     mu240_6(unknown)             = ^CallSideEffect                 : ~mu239_3
+#  240|     mu240_7(Constructible)       = ^IndirectMayWriteSideEffect[-1] : &:r240_1
+#  241|     r241_1(glval<Constructible>) = VariableAddress[c]              : 
+#  241|     r241_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  241|     v241_3(void)                 = Call                            : func:r241_2, this:r241_1
+#  241|     mu241_4(unknown)             = ^CallSideEffect                 : ~mu239_3
+#  241|     v241_5(void)                 = ^BufferReadSideEffect[-1]       : &:r241_1, ~mu239_3
+#  241|     mu241_6(Constructible)       = ^IndirectMayWriteSideEffect[-1] : &:r241_1
+#  242|     r242_1(glval<Constructible>) = VariableAddress[c]              : 
+#  242|     r242_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  242|     v242_3(void)                 = Call                            : func:r242_2, this:r242_1
+#  242|     mu242_4(unknown)             = ^CallSideEffect                 : ~mu239_3
+#  242|     v242_5(void)                 = ^BufferReadSideEffect[-1]       : &:r242_1, ~mu239_3
+#  242|     mu242_6(Constructible)       = ^IndirectMayWriteSideEffect[-1] : &:r242_1
+#  243|     r243_1(glval<Constructible>) = VariableAddress[c2]             : 
+#  243|     mu243_2(Constructible)       = Uninitialized[c2]               : &:r243_1
+#  243|     r243_3(glval<unknown>)       = FunctionAddress[Constructible]  : 
+#  243|     r243_4(int)                  = Constant[2]                     : 
+#  243|     v243_5(void)                 = Call                            : func:r243_3, this:r243_1, 0:r243_4
+#  243|     mu243_6(unknown)             = ^CallSideEffect                 : ~mu239_3
+#  243|     mu243_7(Constructible)       = ^IndirectMayWriteSideEffect[-1] : &:r243_1
+#  244|     r244_1(glval<Constructible>) = VariableAddress[c2]             : 
+#  244|     r244_2(glval<unknown>)       = FunctionAddress[g]              : 
+#  244|     v244_3(void)                 = Call                            : func:r244_2, this:r244_1
+#  244|     mu244_4(unknown)             = ^CallSideEffect                 : ~mu239_3
+#  244|     v244_5(void)                 = ^BufferReadSideEffect[-1]       : &:r244_1, ~mu239_3
+#  244|     mu244_6(Constructible)       = ^IndirectMayWriteSideEffect[-1] : &:r244_1
+#  245|     v245_1(void)                 = NoOp                            : 
+#  239|     v239_4(void)                 = ReturnVoid                      : 
+#  239|     v239_5(void)                 = UnmodeledUse                    : mu*
+#  239|     v239_6(void)                 = AliasedUse                      : ~mu239_3
+#  239|     v239_7(void)                 = ExitFunction                    : 
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.qlref b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.qlref
rename to cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.ql
new file mode 100644
index 00000000000..c7d0ba957af
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.unaliased_ssa.IRSanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..9769ee11f99
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.expected
@@ -0,0 +1,22 @@
+missingOperand
+unexpectedOperand
+duplicateOperand
+missingPhiOperand
+missingOperandType
+duplicateChiOperand
+sideEffectWithoutPrimary
+instructionWithoutSuccessor
+ambiguousSuccessors
+unexplainedLoop
+unnecessaryPhiInstruction
+operandAcrossFunctions
+instructionWithoutUniqueBlock
+containsLoopOfForwardEdges
+lostReachability
+backEdgeCountMismatch
+useNotDominatedByDefinition
+missingCanonicalLanguageType
+multipleCanonicalLanguageTypes
+missingIRType
+multipleIRTypes
+missingCppType
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity.ql b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity.ql
new file mode 100644
index 00000000000..120881bf018
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity.ql
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.unaliased_ssa.internal.SSASanity
+import semmle.code.cpp.ir.implementation.UseSoundEscapeAnalysis
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity_unsound.expected b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity_unsound.expected
new file mode 100644
index 00000000000..7c2d1faf639
--- /dev/null
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity_unsound.expected
@@ -0,0 +1,2 @@
+multipleOperandMemoryLocations
+missingVirtualVariableForMemoryLocation
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity.qlref b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity_unsound.qlref
similarity index 100%
rename from cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity.qlref
rename to cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ssa_sanity_unsound.qlref
diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected
index c8a276b1f63..e4a2cc3d774 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected
+++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected
@@ -16,8 +16,7 @@
 | inline_assembly.c:10:3:10:7 | Store: ... = ... | positive strictlyPositive |
 | inline_assembly.c:10:7:10:7 | Constant: (unsigned int)... | positive strictlyPositive |
 | inline_assembly.c:12:32:12:32 | Load: y | positive strictlyPositive |
-| inline_assembly.c:21:29:21:29 | Load: x | positive |
-| inline_assembly.c:21:32:21:32 | Load: y | positive |
+| inline_assembly.c:21:32:21:32 | Load: y | positive strictlyPositive |
 | minmax.c:16:9:16:10 | Constant: 1 | positive strictlyPositive |
 | minmax.c:16:9:16:10 | Store: 1 | positive strictlyPositive |
 | minmax.c:16:16:16:17 | Constant: 2 | positive strictlyPositive |
diff --git a/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected b/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected
index 2fad91f5f85..ebd22e357c2 100644
--- a/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected
@@ -27,7 +27,6 @@ missingOperand
 | ir.cpp:823:7:823:13 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
 | ir.cpp:824:7:824:26 | IndirectMayWriteSideEffect: call to Base | Instruction 'IndirectMayWriteSideEffect' is missing an expected operand with tag 'Address' in function '$@'. | ir.cpp:799:6:799:25 | IR: HierarchyConversions | void HierarchyConversions() |
 | misc.c:125:5:125:11 | CopyValue: (statement expression) | Instruction 'CopyValue' is missing an expected operand with tag 'Unary' in function '$@'. | misc.c:97:6:97:10 | IR: misc3 | void misc3() |
-| try_catch.cpp:13:5:13:16 | Chi: call to exn1 | Instruction 'Chi' is missing an expected operand with tag 'ChiTotal' in function '$@'. | try_catch.cpp:11:6:11:17 | IR: bypass_catch | void bypass_catch() |
 unexpectedOperand
 duplicateOperand
 missingPhiOperand
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/IRConfiguration.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/IRConfiguration.qll
index 67f9cd5bc62..c0a489ef0c6 100644
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/IRConfiguration.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/IRConfiguration.qll
@@ -17,3 +17,18 @@ class IRConfiguration extends TIRConfiguration {
    */
   predicate shouldCreateIRForFunction(Language::Function func) { any() }
 }
+
+private newtype TIREscapeAnalysisConfiguration = MkIREscapeAnalysisConfiguration()
+
+/**
+ * The query can extend this class to control what escape analysis is used when generating SSA.
+ */
+class IREscapeAnalysisConfiguration extends TIREscapeAnalysisConfiguration {
+  string toString() { result = "IREscapeAnalysisConfiguration" }
+
+  /**
+   * Holds if the escape analysis done by SSA construction should be sound. By default, the SSA is
+   * built assuming that no variable's address ever escapes.
+   */
+  predicate useSoundEscapeAnalysis() { none() }
+}
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/UseSoundEscapeAnalysis.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/UseSoundEscapeAnalysis.qll
new file mode 100644
index 00000000000..b9b1dc243b1
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/UseSoundEscapeAnalysis.qll
@@ -0,0 +1,9 @@
+import IRConfiguration
+
+/**
+ * Overrides the default IR configuration to use sound escape analysis, instead of assuming that
+ * variable addresses never escape.
+ */
+class SoundEscapeAnalysisConfiguration extends IREscapeAnalysisConfiguration {
+  override predicate useSoundEscapeAnalysis() { any() }
+}
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
index 23121523a6b..94470fe8584 100644
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
@@ -107,7 +107,7 @@ class PropertyProvider extends IRPropertyProvider {
     exists(
       MemoryLocation useLocation, IRBlock predBlock, IRBlock defBlock, int defIndex, Overlap overlap
     |
-      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex, overlap) and
+      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex) and
       key = "PhiUse[" + useLocation.toString() + " from " + predBlock.getDisplayIndex().toString() +
           "]" and
       result = defBlock.getDisplayIndex().toString() + "_" + defIndex + " (" + overlap.toString() +