diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll
index 4b993849046f..d058a6c5a3e8 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll
@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll
index 4b993849046f..d058a6c5a3e8 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll
@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**
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 43727b3ff0a8..88a7d4c99ea9 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
@@ -655,6 +655,11 @@ class TranslatedSwitchStmt extends TranslatedStmt {
       kind = getCaseEdge(switchCase) and
       result = getTranslatedStmt(switchCase).getFirstInstruction()
     )
+    or
+    not stmt.hasDefaultCase() and
+    tag = SwitchBranchTag() and
+    kind instanceof DefaultEdge and
+    result = getParent().getChildSuccessor(this)
   }
 
   override Instruction getChildSuccessor(TranslatedElement child) {
diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll
index 4b993849046f..d058a6c5a3e8 100644
--- a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll
@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**
diff --git a/cpp/ql/test/library-tests/ir/ir/PrintAST.expected b/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
index 343ffc27db5d..c2014db4cf88 100644
--- a/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
+++ b/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
@@ -8070,6 +8070,239 @@ ir.cpp:
 # 1170|               Type = [ArrayType] const char[4]
 # 1170|               Value = [StringLiteral] "foo"
 # 1170|               ValueCategory = lvalue
+# 1173| [TopLevelFunction] void switch1Case(int)
+# 1173|   params: 
+# 1173|     0: [Parameter] x
+# 1173|         Type = [IntType] int
+# 1173|   body: [Block] { ... }
+# 1174|     0: [DeclStmt] declaration
+# 1174|       0: [VariableDeclarationEntry] definition of y
+# 1174|           Type = [IntType] int
+# 1174|         init: [Initializer] initializer for y
+# 1174|           expr: [Literal] 0
+# 1174|               Type = [IntType] int
+# 1174|               Value = [Literal] 0
+# 1174|               ValueCategory = prvalue
+# 1175|     1: [SwitchStmt] switch (...) ... 
+# 1175|       0: [VariableAccess] x
+# 1175|           Type = [IntType] int
+# 1175|           ValueCategory = prvalue(load)
+# 1175|       1: [Block] { ... }
+# 1176|         0: [SwitchCase] case ...:
+# 1176|           0: [Literal] 1
+# 1176|               Type = [IntType] int
+# 1176|               Value = [Literal] 1
+# 1176|               ValueCategory = prvalue
+# 1177|         1: [ExprStmt] ExprStmt
+# 1177|           0: [AssignExpr] ... = ...
+# 1177|               Type = [IntType] int
+# 1177|               ValueCategory = lvalue
+# 1177|             0: [VariableAccess] y
+# 1177|                 Type = [IntType] int
+# 1177|                 ValueCategory = lvalue
+# 1177|             1: [Literal] 2
+# 1177|                 Type = [IntType] int
+# 1177|                 Value = [Literal] 2
+# 1177|                 ValueCategory = prvalue
+# 1179|     2: [DeclStmt] declaration
+# 1179|       0: [VariableDeclarationEntry] definition of z
+# 1179|           Type = [IntType] int
+# 1179|         init: [Initializer] initializer for z
+# 1179|           expr: [VariableAccess] y
+# 1179|               Type = [IntType] int
+# 1179|               ValueCategory = prvalue(load)
+# 1180|     3: [ReturnStmt] return ...
+# 1182| [TopLevelFunction] void switch2Case_fallthrough(int)
+# 1182|   params: 
+# 1182|     0: [Parameter] x
+# 1182|         Type = [IntType] int
+# 1182|   body: [Block] { ... }
+# 1183|     0: [DeclStmt] declaration
+# 1183|       0: [VariableDeclarationEntry] definition of y
+# 1183|           Type = [IntType] int
+# 1183|         init: [Initializer] initializer for y
+# 1183|           expr: [Literal] 0
+# 1183|               Type = [IntType] int
+# 1183|               Value = [Literal] 0
+# 1183|               ValueCategory = prvalue
+# 1184|     1: [SwitchStmt] switch (...) ... 
+# 1184|       0: [VariableAccess] x
+# 1184|           Type = [IntType] int
+# 1184|           ValueCategory = prvalue(load)
+# 1184|       1: [Block] { ... }
+# 1185|         0: [SwitchCase] case ...:
+# 1185|           0: [Literal] 1
+# 1185|               Type = [IntType] int
+# 1185|               Value = [Literal] 1
+# 1185|               ValueCategory = prvalue
+# 1186|         1: [ExprStmt] ExprStmt
+# 1186|           0: [AssignExpr] ... = ...
+# 1186|               Type = [IntType] int
+# 1186|               ValueCategory = lvalue
+# 1186|             0: [VariableAccess] y
+# 1186|                 Type = [IntType] int
+# 1186|                 ValueCategory = lvalue
+# 1186|             1: [Literal] 2
+# 1186|                 Type = [IntType] int
+# 1186|                 Value = [Literal] 2
+# 1186|                 ValueCategory = prvalue
+# 1187|         2: [SwitchCase] case ...:
+# 1187|           0: [Literal] 2
+# 1187|               Type = [IntType] int
+# 1187|               Value = [Literal] 2
+# 1187|               ValueCategory = prvalue
+# 1188|         3: [ExprStmt] ExprStmt
+# 1188|           0: [AssignExpr] ... = ...
+# 1188|               Type = [IntType] int
+# 1188|               ValueCategory = lvalue
+# 1188|             0: [VariableAccess] y
+# 1188|                 Type = [IntType] int
+# 1188|                 ValueCategory = lvalue
+# 1188|             1: [Literal] 3
+# 1188|                 Type = [IntType] int
+# 1188|                 Value = [Literal] 3
+# 1188|                 ValueCategory = prvalue
+# 1190|     2: [DeclStmt] declaration
+# 1190|       0: [VariableDeclarationEntry] definition of z
+# 1190|           Type = [IntType] int
+# 1190|         init: [Initializer] initializer for z
+# 1190|           expr: [VariableAccess] y
+# 1190|               Type = [IntType] int
+# 1190|               ValueCategory = prvalue(load)
+# 1191|     3: [ReturnStmt] return ...
+# 1193| [TopLevelFunction] void switch2Case(int)
+# 1193|   params: 
+# 1193|     0: [Parameter] x
+# 1193|         Type = [IntType] int
+# 1193|   body: [Block] { ... }
+# 1194|     0: [DeclStmt] declaration
+# 1194|       0: [VariableDeclarationEntry] definition of y
+# 1194|           Type = [IntType] int
+# 1194|         init: [Initializer] initializer for y
+# 1194|           expr: [Literal] 0
+# 1194|               Type = [IntType] int
+# 1194|               Value = [Literal] 0
+# 1194|               ValueCategory = prvalue
+# 1195|     1: [SwitchStmt] switch (...) ... 
+# 1195|       0: [VariableAccess] x
+# 1195|           Type = [IntType] int
+# 1195|           ValueCategory = prvalue(load)
+# 1195|       1: [Block] { ... }
+# 1196|         0: [SwitchCase] case ...:
+# 1196|           0: [Literal] 1
+# 1196|               Type = [IntType] int
+# 1196|               Value = [Literal] 1
+# 1196|               ValueCategory = prvalue
+# 1197|         1: [ExprStmt] ExprStmt
+# 1197|           0: [AssignExpr] ... = ...
+# 1197|               Type = [IntType] int
+# 1197|               ValueCategory = lvalue
+# 1197|             0: [VariableAccess] y
+# 1197|                 Type = [IntType] int
+# 1197|                 ValueCategory = lvalue
+# 1197|             1: [Literal] 2
+# 1197|                 Type = [IntType] int
+# 1197|                 Value = [Literal] 2
+# 1197|                 ValueCategory = prvalue
+# 1198|         2: [BreakStmt] break;
+# 1199|         3: [SwitchCase] case ...:
+# 1199|           0: [Literal] 2
+# 1199|               Type = [IntType] int
+# 1199|               Value = [Literal] 2
+# 1199|               ValueCategory = prvalue
+# 1200|         4: [ExprStmt] ExprStmt
+# 1200|           0: [AssignExpr] ... = ...
+# 1200|               Type = [IntType] int
+# 1200|               ValueCategory = lvalue
+# 1200|             0: [VariableAccess] y
+# 1200|                 Type = [IntType] int
+# 1200|                 ValueCategory = lvalue
+# 1200|             1: [Literal] 3
+# 1200|                 Type = [IntType] int
+# 1200|                 Value = [Literal] 3
+# 1200|                 ValueCategory = prvalue
+# 1201|     2: [LabelStmt] label ...:
+# 1202|     3: [DeclStmt] declaration
+# 1202|       0: [VariableDeclarationEntry] definition of z
+# 1202|           Type = [IntType] int
+# 1202|         init: [Initializer] initializer for z
+# 1202|           expr: [VariableAccess] y
+# 1202|               Type = [IntType] int
+# 1202|               ValueCategory = prvalue(load)
+# 1203|     4: [ReturnStmt] return ...
+# 1205| [TopLevelFunction] void switch2Case_default(int)
+# 1205|   params: 
+# 1205|     0: [Parameter] x
+# 1205|         Type = [IntType] int
+# 1205|   body: [Block] { ... }
+# 1206|     0: [DeclStmt] declaration
+# 1206|       0: [VariableDeclarationEntry] definition of y
+# 1206|           Type = [IntType] int
+# 1206|         init: [Initializer] initializer for y
+# 1206|           expr: [Literal] 0
+# 1206|               Type = [IntType] int
+# 1206|               Value = [Literal] 0
+# 1206|               ValueCategory = prvalue
+# 1207|     1: [SwitchStmt] switch (...) ... 
+# 1207|       0: [VariableAccess] x
+# 1207|           Type = [IntType] int
+# 1207|           ValueCategory = prvalue(load)
+# 1207|       1: [Block] { ... }
+# 1208|         0: [SwitchCase] case ...:
+# 1208|           0: [Literal] 1
+# 1208|               Type = [IntType] int
+# 1208|               Value = [Literal] 1
+# 1208|               ValueCategory = prvalue
+# 1209|         1: [ExprStmt] ExprStmt
+# 1209|           0: [AssignExpr] ... = ...
+# 1209|               Type = [IntType] int
+# 1209|               ValueCategory = lvalue
+# 1209|             0: [VariableAccess] y
+# 1209|                 Type = [IntType] int
+# 1209|                 ValueCategory = lvalue
+# 1209|             1: [Literal] 2
+# 1209|                 Type = [IntType] int
+# 1209|                 Value = [Literal] 2
+# 1209|                 ValueCategory = prvalue
+# 1210|         2: [BreakStmt] break;
+# 1212|         3: [SwitchCase] case ...:
+# 1212|           0: [Literal] 2
+# 1212|               Type = [IntType] int
+# 1212|               Value = [Literal] 2
+# 1212|               ValueCategory = prvalue
+# 1213|         4: [ExprStmt] ExprStmt
+# 1213|           0: [AssignExpr] ... = ...
+# 1213|               Type = [IntType] int
+# 1213|               ValueCategory = lvalue
+# 1213|             0: [VariableAccess] y
+# 1213|                 Type = [IntType] int
+# 1213|                 ValueCategory = lvalue
+# 1213|             1: [Literal] 3
+# 1213|                 Type = [IntType] int
+# 1213|                 Value = [Literal] 3
+# 1213|                 ValueCategory = prvalue
+# 1214|         5: [BreakStmt] break;
+# 1216|         6: [SwitchCase] default: 
+# 1217|         7: [ExprStmt] ExprStmt
+# 1217|           0: [AssignExpr] ... = ...
+# 1217|               Type = [IntType] int
+# 1217|               ValueCategory = lvalue
+# 1217|             0: [VariableAccess] y
+# 1217|                 Type = [IntType] int
+# 1217|                 ValueCategory = lvalue
+# 1217|             1: [Literal] 4
+# 1217|                 Type = [IntType] int
+# 1217|                 Value = [Literal] 4
+# 1217|                 ValueCategory = prvalue
+# 1218|     2: [LabelStmt] label ...:
+# 1219|     3: [DeclStmt] declaration
+# 1219|       0: [VariableDeclarationEntry] definition of z
+# 1219|           Type = [IntType] int
+# 1219|         init: [Initializer] initializer for z
+# 1219|           expr: [VariableAccess] y
+# 1219|               Type = [IntType] int
+# 1219|               ValueCategory = prvalue(load)
+# 1220|     4: [ReturnStmt] return ...
 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.expected b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.expected
index e5e666c020b1..289b7bcae86b 100644
--- a/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.expected
@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
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
index e5e666c020b1..289b7bcae86b 100644
--- 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
@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/ir/ir/ir.cpp b/cpp/ql/test/library-tests/ir/ir/ir.cpp
index 6989287d2224..c3a394f09857 100644
--- a/cpp/ql/test/library-tests/ir/ir/ir.cpp
+++ b/cpp/ql/test/library-tests/ir/ir/ir.cpp
@@ -1170,4 +1170,53 @@ String ReturnObjectImpl() {
   return String("foo");
 }
 
+void switch1Case(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+    }
+    int z = y;
+}
+
+void switch2Case_fallthrough(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+        case 2:
+        y = 3;
+    }
+    int z = y;
+}
+
+void switch2Case(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+        break;
+        case 2:
+        y = 3;
+    }
+    int z = y;
+}
+
+void switch2Case_default(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+            y = 2;
+            break;
+
+        case 2:
+            y = 3;
+            break;
+
+        default:
+            y = 4;
+    }
+    int z = y;
+}
+
 // 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 6420d52ee6d7..bc7289fd967a 100644
--- a/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
+++ b/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
@@ -6052,6 +6052,182 @@ ir.cpp:
 # 1169|     v1169_8(void)           = AliasedUse                      : ~mu1169_4
 # 1169|     v1169_9(void)           = ExitFunction                    : 
 
+# 1173| void switch1Case(int)
+# 1173|   Block 0
+# 1173|     v1173_1(void)       = EnterFunction          : 
+# 1173|     mu1173_2(unknown)   = AliasedDefinition      : 
+# 1173|     mu1173_3(unknown)   = InitializeNonLocal     : 
+# 1173|     mu1173_4(unknown)   = UnmodeledDefinition    : 
+# 1173|     r1173_5(glval<int>) = VariableAddress[x]     : 
+# 1173|     mu1173_6(int)       = InitializeParameter[x] : &:r1173_5
+# 1174|     r1174_1(glval<int>) = VariableAddress[y]     : 
+# 1174|     r1174_2(int)        = Constant[0]            : 
+# 1174|     mu1174_3(int)       = Store                  : &:r1174_1, r1174_2
+# 1175|     r1175_1(glval<int>) = VariableAddress[x]     : 
+# 1175|     r1175_2(int)        = Load                   : &:r1175_1, ~mu1173_4
+# 1175|     v1175_3(void)       = Switch                 : r1175_2
+#-----|   Case[1] -> Block 1
+#-----|   Default -> Block 2
+
+# 1176|   Block 1
+# 1176|     v1176_1(void)       = NoOp               : 
+# 1177|     r1177_1(int)        = Constant[2]        : 
+# 1177|     r1177_2(glval<int>) = VariableAddress[y] : 
+# 1177|     mu1177_3(int)       = Store              : &:r1177_2, r1177_1
+#-----|   Goto -> Block 2
+
+# 1179|   Block 2
+# 1179|     r1179_1(glval<int>) = VariableAddress[z] : 
+# 1179|     r1179_2(glval<int>) = VariableAddress[y] : 
+# 1179|     r1179_3(int)        = Load               : &:r1179_2, ~mu1173_4
+# 1179|     mu1179_4(int)       = Store              : &:r1179_1, r1179_3
+# 1180|     v1180_1(void)       = NoOp               : 
+# 1173|     v1173_7(void)       = ReturnVoid         : 
+# 1173|     v1173_8(void)       = UnmodeledUse       : mu*
+# 1173|     v1173_9(void)       = AliasedUse         : ~mu1173_4
+# 1173|     v1173_10(void)      = ExitFunction       : 
+
+# 1182| void switch2Case_fallthrough(int)
+# 1182|   Block 0
+# 1182|     v1182_1(void)       = EnterFunction          : 
+# 1182|     mu1182_2(unknown)   = AliasedDefinition      : 
+# 1182|     mu1182_3(unknown)   = InitializeNonLocal     : 
+# 1182|     mu1182_4(unknown)   = UnmodeledDefinition    : 
+# 1182|     r1182_5(glval<int>) = VariableAddress[x]     : 
+# 1182|     mu1182_6(int)       = InitializeParameter[x] : &:r1182_5
+# 1183|     r1183_1(glval<int>) = VariableAddress[y]     : 
+# 1183|     r1183_2(int)        = Constant[0]            : 
+# 1183|     mu1183_3(int)       = Store                  : &:r1183_1, r1183_2
+# 1184|     r1184_1(glval<int>) = VariableAddress[x]     : 
+# 1184|     r1184_2(int)        = Load                   : &:r1184_1, ~mu1182_4
+# 1184|     v1184_3(void)       = Switch                 : r1184_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1185|   Block 1
+# 1185|     v1185_1(void)       = NoOp               : 
+# 1186|     r1186_1(int)        = Constant[2]        : 
+# 1186|     r1186_2(glval<int>) = VariableAddress[y] : 
+# 1186|     mu1186_3(int)       = Store              : &:r1186_2, r1186_1
+#-----|   Goto -> Block 2
+
+# 1187|   Block 2
+# 1187|     v1187_1(void)       = NoOp               : 
+# 1188|     r1188_1(int)        = Constant[3]        : 
+# 1188|     r1188_2(glval<int>) = VariableAddress[y] : 
+# 1188|     mu1188_3(int)       = Store              : &:r1188_2, r1188_1
+#-----|   Goto -> Block 3
+
+# 1190|   Block 3
+# 1190|     r1190_1(glval<int>) = VariableAddress[z] : 
+# 1190|     r1190_2(glval<int>) = VariableAddress[y] : 
+# 1190|     r1190_3(int)        = Load               : &:r1190_2, ~mu1182_4
+# 1190|     mu1190_4(int)       = Store              : &:r1190_1, r1190_3
+# 1191|     v1191_1(void)       = NoOp               : 
+# 1182|     v1182_7(void)       = ReturnVoid         : 
+# 1182|     v1182_8(void)       = UnmodeledUse       : mu*
+# 1182|     v1182_9(void)       = AliasedUse         : ~mu1182_4
+# 1182|     v1182_10(void)      = ExitFunction       : 
+
+# 1193| void switch2Case(int)
+# 1193|   Block 0
+# 1193|     v1193_1(void)       = EnterFunction          : 
+# 1193|     mu1193_2(unknown)   = AliasedDefinition      : 
+# 1193|     mu1193_3(unknown)   = InitializeNonLocal     : 
+# 1193|     mu1193_4(unknown)   = UnmodeledDefinition    : 
+# 1193|     r1193_5(glval<int>) = VariableAddress[x]     : 
+# 1193|     mu1193_6(int)       = InitializeParameter[x] : &:r1193_5
+# 1194|     r1194_1(glval<int>) = VariableAddress[y]     : 
+# 1194|     r1194_2(int)        = Constant[0]            : 
+# 1194|     mu1194_3(int)       = Store                  : &:r1194_1, r1194_2
+# 1195|     r1195_1(glval<int>) = VariableAddress[x]     : 
+# 1195|     r1195_2(int)        = Load                   : &:r1195_1, ~mu1193_4
+# 1195|     v1195_3(void)       = Switch                 : r1195_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1196|   Block 1
+# 1196|     v1196_1(void)       = NoOp               : 
+# 1197|     r1197_1(int)        = Constant[2]        : 
+# 1197|     r1197_2(glval<int>) = VariableAddress[y] : 
+# 1197|     mu1197_3(int)       = Store              : &:r1197_2, r1197_1
+# 1198|     v1198_1(void)       = NoOp               : 
+#-----|   Goto -> Block 3
+
+# 1199|   Block 2
+# 1199|     v1199_1(void)       = NoOp               : 
+# 1200|     r1200_1(int)        = Constant[3]        : 
+# 1200|     r1200_2(glval<int>) = VariableAddress[y] : 
+# 1200|     mu1200_3(int)       = Store              : &:r1200_2, r1200_1
+#-----|   Goto -> Block 3
+
+# 1201|   Block 3
+# 1201|     v1201_1(void)       = NoOp               : 
+# 1202|     r1202_1(glval<int>) = VariableAddress[z] : 
+# 1202|     r1202_2(glval<int>) = VariableAddress[y] : 
+# 1202|     r1202_3(int)        = Load               : &:r1202_2, ~mu1193_4
+# 1202|     mu1202_4(int)       = Store              : &:r1202_1, r1202_3
+# 1203|     v1203_1(void)       = NoOp               : 
+# 1193|     v1193_7(void)       = ReturnVoid         : 
+# 1193|     v1193_8(void)       = UnmodeledUse       : mu*
+# 1193|     v1193_9(void)       = AliasedUse         : ~mu1193_4
+# 1193|     v1193_10(void)      = ExitFunction       : 
+
+# 1205| void switch2Case_default(int)
+# 1205|   Block 0
+# 1205|     v1205_1(void)       = EnterFunction          : 
+# 1205|     mu1205_2(unknown)   = AliasedDefinition      : 
+# 1205|     mu1205_3(unknown)   = InitializeNonLocal     : 
+# 1205|     mu1205_4(unknown)   = UnmodeledDefinition    : 
+# 1205|     r1205_5(glval<int>) = VariableAddress[x]     : 
+# 1205|     mu1205_6(int)       = InitializeParameter[x] : &:r1205_5
+# 1206|     r1206_1(glval<int>) = VariableAddress[y]     : 
+# 1206|     r1206_2(int)        = Constant[0]            : 
+# 1206|     mu1206_3(int)       = Store                  : &:r1206_1, r1206_2
+# 1207|     r1207_1(glval<int>) = VariableAddress[x]     : 
+# 1207|     r1207_2(int)        = Load                   : &:r1207_1, ~mu1205_4
+# 1207|     v1207_3(void)       = Switch                 : r1207_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1208|   Block 1
+# 1208|     v1208_1(void)       = NoOp               : 
+# 1209|     r1209_1(int)        = Constant[2]        : 
+# 1209|     r1209_2(glval<int>) = VariableAddress[y] : 
+# 1209|     mu1209_3(int)       = Store              : &:r1209_2, r1209_1
+# 1210|     v1210_1(void)       = NoOp               : 
+#-----|   Goto -> Block 4
+
+# 1212|   Block 2
+# 1212|     v1212_1(void)       = NoOp               : 
+# 1213|     r1213_1(int)        = Constant[3]        : 
+# 1213|     r1213_2(glval<int>) = VariableAddress[y] : 
+# 1213|     mu1213_3(int)       = Store              : &:r1213_2, r1213_1
+# 1214|     v1214_1(void)       = NoOp               : 
+#-----|   Goto -> Block 4
+
+# 1216|   Block 3
+# 1216|     v1216_1(void)       = NoOp               : 
+# 1217|     r1217_1(int)        = Constant[4]        : 
+# 1217|     r1217_2(glval<int>) = VariableAddress[y] : 
+# 1217|     mu1217_3(int)       = Store              : &:r1217_2, r1217_1
+#-----|   Goto -> Block 4
+
+# 1218|   Block 4
+# 1218|     v1218_1(void)       = NoOp               : 
+# 1219|     r1219_1(glval<int>) = VariableAddress[z] : 
+# 1219|     r1219_2(glval<int>) = VariableAddress[y] : 
+# 1219|     r1219_3(int)        = Load               : &:r1219_2, ~mu1205_4
+# 1219|     mu1219_4(int)       = Store              : &:r1219_1, r1219_3
+# 1220|     v1220_1(void)       = NoOp               : 
+# 1205|     v1205_7(void)       = ReturnVoid         : 
+# 1205|     v1205_8(void)       = UnmodeledUse       : mu*
+# 1205|     v1205_9(void)       = AliasedUse         : ~mu1205_4
+# 1205|     v1205_10(void)      = ExitFunction       : 
+
 perf-regression.cpp:
 #    6| void Big::Big()
 #    6|   Block 0
diff --git a/cpp/ql/test/library-tests/ir/ir/raw_sanity.expected b/cpp/ql/test/library-tests/ir/ir/raw_sanity.expected
index e5e666c020b1..289b7bcae86b 100644
--- a/cpp/ql/test/library-tests/ir/ir/raw_sanity.expected
+++ b/cpp/ql/test/library-tests/ir/ir/raw_sanity.expected
@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
index e5e666c020b1..289b7bcae86b 100644
--- a/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
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
index e5e666c020b1..289b7bcae86b 100644
--- 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
@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected
index 9769ee11f99f..962a5a4484bc 100644
--- a/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
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
index 9769ee11f99f..962a5a4484bc 100644
--- 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
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected
index 9769ee11f99f..962a5a4484bc 100644
--- a/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
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
index 9769ee11f99f..962a5a4484bc 100644
--- 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
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
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 c0671e967cc9..64a521865641 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
@@ -568,6 +568,7 @@ lostReachability
 | range_analysis.c:371:37:371:39 | Constant: 500 |
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected b/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected
index 80da8a79cedd..63e211635ea0 100644
--- a/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected
@@ -645,6 +645,7 @@ useNotDominatedByDefinition
 | pointer_to_member.cpp:36:22:36:28 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
 | try_catch.cpp:21:13:21:24 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | try_catch.cpp:19:6:19:23 | IR: throw_from_nonstmt | void throw_from_nonstmt(int) |
 | vla.c:3:27:3:30 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | vla.c:3:5:3:8 | IR: main | int main(int, char**) |
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected b/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected
index c7897f98817b..a7f2d82ac7e0 100644
--- a/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected
@@ -577,6 +577,7 @@ lostReachability
 | range_analysis.c:371:37:371:39 | Constant: 500 |
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/Instruction.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/Instruction.qll
index 4b993849046f..d058a6c5a3e8 100644
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/Instruction.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/Instruction.qll
@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedStmt.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedStmt.qll
index 5ead54f0a8a8..0ec51bd91908 100644
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -834,6 +834,11 @@ class TranslatedSwitchStmt extends TranslatedStmt {
       kind = this.getCaseEdge(caseStmt) and
       result = getTranslatedStmt(caseStmt).getFirstInstruction()
     )
+    or
+    not exists(stmt.getDefaultCase()) and
+    tag = SwitchBranchTag() and
+    kind instanceof DefaultEdge and
+    result = getParent().getChildSuccessor(this)
   }
 
   private EdgeKind getCaseEdge(CaseStmt caseStmt) {
diff --git a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll
index 4b993849046f..d058a6c5a3e8 100644
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll
@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**
diff --git a/csharp/ql/test/library-tests/ir/ir/raw_ir_sanity.expected b/csharp/ql/test/library-tests/ir/ir/raw_ir_sanity.expected
index 9f132fa6f280..4c0b8578a179 100644
--- a/csharp/ql/test/library-tests/ir/ir/raw_ir_sanity.expected
+++ b/csharp/ql/test/library-tests/ir/ir/raw_ir_sanity.expected
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType
diff --git a/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected b/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
index 9f132fa6f280..4c0b8578a179 100644
--- a/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
+++ b/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType