diff --git a/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md b/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md
new file mode 100644
index 000000000000..c68fdb91c717
--- /dev/null
+++ b/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* Added support for structured exception handling (SEH). As a result, dataflow queries may have more results in code bases that use SEH.
\ No newline at end of file
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
index 81db183fa63e..0dd16c6dd6b9 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
@@ -3,12 +3,13 @@
  */
 
 private import internal.EdgeKindInternal
+private import codeql.util.Boolean
 
 private newtype TEdgeKind =
   TGotoEdge() or // Single successor (including fall-through)
   TTrueEdge() or // 'true' edge of conditional branch
   TFalseEdge() or // 'false' edge of conditional branch
-  TExceptionEdge() or // Thrown exception
+  TExceptionEdge(Boolean isSeh) or // Thrown exception, true for SEH exceptions, false otherwise
   TDefaultEdge() or // 'default' label of switch
   TCaseEdge(string minValue, string maxValue) {
     // Case label of switch
@@ -54,7 +55,18 @@ class FalseEdge extends EdgeKind, TFalseEdge {
  * instruction's evaluation throws an exception.
  */
 class ExceptionEdge extends EdgeKind, TExceptionEdge {
-  final override string toString() { result = "Exception" }
+  boolean isSeh; //true for Structured Exception Handling, false for C++ exceptions
+
+  ExceptionEdge() { this = TExceptionEdge(isSeh) }
+
+  /**
+   * Holds if the exception is a Structured Exception Handling (SEH) exception.
+   */
+  final predicate isSeh() { isSeh = true }
+
+  final override string toString() {
+    if isSeh = true then result = "SEH Exception" else result = "C++ Exception"
+  }
 }
 
 /**
@@ -121,9 +133,10 @@ module EdgeKind {
   FalseEdge falseEdge() { result = TFalseEdge() }
 
   /**
-   * Gets the single instance of the `ExceptionEdge` class.
+   * Gets the instance of the `ExceptionEdge` class.
+   * `isSeh` is true if the exception is an SEH exception, and false for a C++ edge.
    */
-  ExceptionEdge exceptionEdge() { result = TExceptionEdge() }
+  ExceptionEdge exceptionEdge(boolean isSeh) { result = TExceptionEdge(isSeh) }
 
   /**
    * Gets the single instance of the `DefaultEdge` class.
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index daa6bdaafcf6..4aebcad423fc 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -10,6 +10,7 @@ private import TranslatedElement
 private import TranslatedExpr
 private import TranslatedFunction
 private import DefaultOptions as DefaultOptions
+private import EdgeKind
 
 /**
  * Gets the `CallInstruction` from the `TranslatedCallExpr` for the specified expression.
@@ -83,14 +84,36 @@ abstract class TranslatedCall extends TranslatedExpr {
         any(UnreachedInstruction instr |
           this.getEnclosingFunction().getFunction() = instr.getEnclosingFunction()
         )
-    else (
-      not this.mustThrowException() and
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      this.mayThrowException() and
-      kind instanceof ExceptionEdge and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
-    )
+    else
+      exists(boolean isSeh | kind = exceptionEdge(isSeh) |
+        // Call throw behavior is resolved from most restricted to least restricted in order
+        // if there are conflicting throwing specificaitons for a function.
+        // Enumerating all scenarios to be explicit.
+        (
+          // If the call is known to never throw, regardless of other defined throwing behavior,
+          // do not generate any exception edges, only an ordinary successor
+          if this.(TranslatedCallExpr).neverRaiseException(isSeh)
+          then result = this.getParent().getChildSuccessor(this, any(GotoEdge edge))
+          else
+            // If the call is known to always throw, regardless of other defined throwing behavior,
+            // only generate an exception edge.
+            if this.(TranslatedCallExpr).alwaysRaiseException(isSeh)
+            then
+              result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSeh)
+            else
+              if this.(TranslatedCallExpr).mayRaiseException(isSeh)
+              then (
+                // if the call is known to conditionally throw, generate both an exception edge and an
+                // ordinary successor
+                result =
+                  this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSeh)
+                or
+                result = this.getParent().getChildSuccessor(this, kind)
+              ) else
+                // fallthrough case, no exceptions, just get the ordinary successor
+                result = this.getParent().getChildSuccessor(this, kind)
+        )
+      )
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
@@ -117,14 +140,28 @@ abstract class TranslatedCall extends TranslatedExpr {
   final override Instruction getResult() { result = this.getInstruction(CallTag()) }
 
   /**
-   * Holds if the evaluation of this call may throw an exception.
+   * The call target is known to always raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
    */
-  abstract predicate mayThrowException();
+  abstract predicate alwaysRaiseException(boolean isSeh);
 
   /**
-   * Holds if the evaluation of this call always throws an exception.
+   * Holds when call target is known to conditionally raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
    */
-  abstract predicate mustThrowException();
+  abstract predicate mayRaiseException(boolean isSeh);
+
+  /**
+   * Holds when the call target is known to never raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
+   */
+  abstract predicate neverRaiseException(boolean isSeh);
 
   /**
    * Gets the result type of the call.
@@ -320,6 +357,34 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   final override int getNumberOfArguments() { result = expr.getNumberOfArguments() }
 
   final override predicate isNoReturn() { any(Options opt).exits(expr.getTarget()) }
+
+  override Function getInstructionFunction(InstructionTag tag) {
+    tag = CallTargetTag() and result = expr.getTarget()
+  }
+
+  override predicate alwaysRaiseException(boolean isSeh) {
+    exists(ThrowingFunction f | f = expr.getTarget() |
+      f.alwaysRaisesException() and f.isSeh() and isSeh = true
+      or
+      f.alwaysRaisesException() and f.isCxx() and isSeh = false
+    )
+  }
+
+  override predicate mayRaiseException(boolean isSeh) {
+    exists(ThrowingFunction f | f = expr.getTarget() |
+      f.mayRaiseException() and f.isSeh() and isSeh = true
+      or
+      f.mayRaiseException() and f.isCxx() and isSeh = false
+    )
+  }
+
+  override predicate neverRaiseException(boolean isSeh) {
+    exists(NonThrowingFunction f | f = expr.getTarget() |
+      f.isSeh() and isSeh = true
+      or
+      f.isCxx() and isSeh = false
+    )
+  }
 }
 
 /**
@@ -332,14 +397,42 @@ class TranslatedExprCall extends TranslatedCallExpr {
     result = getTranslatedExpr(expr.getExpr().getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
-    // We assume that a call to a function pointer will not throw an exception.
+  override predicate alwaysRaiseException(boolean isSeh) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
-    none()
+    // For SEH exceptions, use the defined ThrowingFunction behavior and
+    // if no throwing function is found, assume a conditional SEH exception
+    // see `mayRaiseException`
+    exists(ThrowingFunction f | f = expr.getTarget() |
+      f.alwaysRaisesException() and f.isSeh() and isSeh = true
+    )
+  }
+
+  override predicate mayRaiseException(boolean isSeh) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
+    // This is not sound in general, but this will greatly reduce the number of
+    // exceptional edges.
+    // For SEH exceptions, use the defined ThrowingFunction behavior.
+    // ASSUMPTION: if no ThrowingFunction is found for the given call, assume a conditional SEH exception
+    // on the call.
+    exists(ThrowingFunction f | f = expr.getTarget() |
+      f.mayRaiseException() and f.isSeh() and isSeh = true
+    )
+    or
+    not exists(ThrowingFunction f | f = expr.getTarget() and f.isSeh()) and
+    isSeh = true
   }
 
-  final override predicate mustThrowException() { none() }
+  override predicate neverRaiseException(boolean isSeh) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
+    // This is not sound in general, but this will greatly reduce the number of
+    // exceptional edges.
+    // For SEH exceptions, use the defined ThrowingFunction behavior and
+    // if no throwing function is found, assume a conditional SEH exception
+    // see `mayRaiseException`
+    exists(NonThrowingFunction f | f = expr.getTarget() | f.isSeh() and isSeh = true)
+  }
 }
 
 /**
@@ -348,10 +441,6 @@ class TranslatedExprCall extends TranslatedCallExpr {
 class TranslatedFunctionCall extends TranslatedCallExpr, TranslatedDirectCall {
   override FunctionCall expr;
 
-  override Function getInstructionFunction(InstructionTag tag) {
-    tag = CallTargetTag() and result = expr.getTarget()
-  }
-
   override Instruction getQualifierResult() {
     this.hasQualifier() and
     result = this.getQualifier().getResult()
@@ -361,14 +450,6 @@ class TranslatedFunctionCall extends TranslatedCallExpr, TranslatedDirectCall {
     exists(this.getQualifier()) and
     not exists(MemberFunction func | expr.getTarget() = func and func.isStatic())
   }
-
-  final override predicate mayThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(_)
-  }
-
-  final override predicate mustThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(true)
-  }
 }
 
 /**
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
index 0f9bc370f7a5..0dd6ec99a192 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
@@ -1104,9 +1104,13 @@ abstract class TranslatedElement extends TTranslatedElement {
    * within this element. This will generally return first `catch` block of the
    * nearest enclosing `try`, or the `Unwind` instruction for the function if
    * there is no enclosing `try`. The successor edge kind is specified by `kind`.
+   *
+   * `isSeh` is true if the exception is a structured exception, false if otherwise.
+   * The boolean value can be extracted from `ExceptionEdge` from the exception
+   * edge triggering the call to this function.
    */
-  Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
-    result = this.getParent().getExceptionSuccessorInstruction(kind)
+  Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
+    result = this.getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 
   /**
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index e7ccac24eb92..d9c2dede732f 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -15,6 +15,7 @@ private import TranslatedInitialization
 private import TranslatedStmt
 private import TranslatedGlobalVar
 private import IRConstruction
+private import EdgeKind
 import TranslatedCall
 
 /**
@@ -391,7 +392,13 @@ class TranslatedLoad extends TranslatedValueCategoryAdjustment, TTranslatedLoad
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = LoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -1083,7 +1090,13 @@ class TranslatedStructuredBindingVariableAccess extends TranslatedNonConstantExp
     result = this.getInstruction(LoadTag())
     or
     tag = LoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
@@ -1898,8 +1911,13 @@ class TranslatedBlockAssignExpr extends TranslatedNonConstantExpr {
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = LoadTag() and
-    result = this.getInstruction(AssignmentStoreTag()) and
-    kind instanceof GotoEdge
+    (
+      result = this.getInstruction(AssignmentStoreTag()) and kind instanceof GotoEdge
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
     or
     tag = AssignmentStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
@@ -2375,14 +2393,16 @@ class TranslatedAllocatorCall extends TTranslatedAllocatorCall, TranslatedDirect
         result = getTranslatedExpr(expr.getAllocatorCall().getArgument(index).getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
+  final override predicate mayRaiseException(boolean isSeh) {
     // We assume that a call to `new` or `new[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate mustThrowException() { none() }
+  final override predicate alwaysRaiseException(boolean isSeh) { none() }
+
+  final override predicate neverRaiseException(boolean isSeh) { none() }
 }
 
 TranslatedAllocatorCall getTranslatedAllocatorCall(NewOrNewArrayExpr newExpr) {
@@ -2448,14 +2468,16 @@ class TranslatedDeleteOrDeleteArrayExpr extends TranslatedNonConstantExpr, Trans
     result = getTranslatedExpr(expr.getExprWithReuse().getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
+  final override predicate mayRaiseException(boolean isSeh) {
     // We assume that a call to `delete` or `delete[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate mustThrowException() { none() }
+  final override predicate alwaysRaiseException(boolean isSeh) { none() }
+
+  final override predicate neverRaiseException(boolean isSeh) { none() }
 }
 
 TranslatedDeleteOrDeleteArrayExpr getTranslatedDeleteOrDeleteArray(DeleteOrDeleteArrayExpr newExpr) {
@@ -3039,8 +3061,8 @@ class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDest
       or
       // And otherwise, exit this element with an exceptional edge
       not exists(this.getChild(id + 1)) and
-      kind instanceof ExceptionEdge and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+      kind = exceptionEdge(false) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), false)
     )
   }
 
@@ -3079,7 +3101,8 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
       or
       not exists(this.getDestructors()) and
       kind instanceof ExceptionEdge and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+      kind = exceptionEdge(false) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), false)
     )
   }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index 57f718bcb6ab..beccc7f3a839 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -214,7 +214,8 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
         exists(ThrowExpr throw | throw.getEnclosingFunction() = func)
         or
         exists(FunctionCall call | call.getEnclosingFunction() = func |
-          getTranslatedExpr(call).(TranslatedCallExpr).mayThrowException()
+          getTranslatedExpr(call).(TranslatedCallExpr).mayRaiseException(_) or
+          getTranslatedExpr(call).(TranslatedCallExpr).alwaysRaiseException(_)
         )
       )
       or
@@ -228,7 +229,10 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
     )
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
+    // only unwind for C++ exceptions since SEH exceptions are too verbose
+    // and would generate unwind for all functions.
+    isSeh = false and
     result = this.getInstruction(UnwindTag()) and
     kind instanceof GotoEdge
   }
@@ -401,9 +405,9 @@ abstract class TranslatedParameter extends TranslatedElement {
     then kind instanceof GotoEdge and result = this.getInstruction(InitializerIndirectAddressTag())
     else result = this.getParent().getChildSuccessor(this, kind)
     or
-    kind instanceof GotoEdge and
     tag = InitializerIndirectAddressTag() and
-    result = this.getInstruction(InitializerIndirectStoreTag())
+    result = this.getInstruction(InitializerIndirectStoreTag()) and
+    kind instanceof GotoEdge
     or
     tag = InitializerIndirectStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 06ce91932051..46b43571e3c3 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -281,7 +281,13 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = InitializerStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -357,9 +363,14 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
-    kind instanceof GotoEdge and
     tag = InitializerLoadStringTag() and
-    result = this.getInstruction(InitializerStoreTag())
+    (
+      result = this.getInstruction(InitializerStoreTag()) and kind instanceof GotoEdge
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
     or
     if this.zeroInitRange(_, _)
     then (
@@ -650,7 +661,13 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
     )
     or
     tag = this.getFieldDefaultValueStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
   }
 
   override string getInstructionConstantValue(InstructionTag tag) {
@@ -850,7 +867,13 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
     )
     or
     tag = this.getElementDefaultValueStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSeh()
+    )
   }
 
   override string getInstructionConstantValue(InstructionTag tag) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index e37df72abbd0..1603e9e8ca7b 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -151,7 +151,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
       // TODO: This is not really correct. The semantics of `EXCEPTION_CONTINUE_EXECUTION` is that
       // we should continue execution at the point where the exception occurred. But we don't have
       // any instruction to model this behavior.
-      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge), true)
       or
       kind instanceof FalseEdge and
       result = this.getInstruction(TryExceptGenerateZero())
@@ -171,7 +171,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
     tag = TryExceptCompareZeroBranch() and
     (
       kind instanceof TrueEdge and
-      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge), true)
       or
       kind instanceof FalseEdge and
       result = this.getInstruction(TryExceptGenerateOne())
@@ -226,10 +226,10 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
 
   final override Function getFunction() { result = tryExcept.getEnclosingFunction() }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `__except` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 }
 
@@ -282,10 +282,10 @@ class TranslatedMicrosoftTryFinallyHandler extends TranslatedElement,
     result = getTranslatedStmt(tryFinally.getFinally())
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `__finally` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 }
 
@@ -734,14 +734,32 @@ class TranslatedTryStmt extends TranslatedStmt {
     // of the `try`, because the exception successor of the `try` itself is
     // the first catch clause.
     handler = this.getHandler(stmt.getNumberOfCatchClauses() - 1) and
-    result = this.getParent().getExceptionSuccessorInstruction(kind)
+    exists(boolean isSeh |
+      stmt instanceof MicrosoftTryStmt and isSeh = true
+      or
+      stmt instanceof TryStmt and isSeh = false
+    |
+      result = this.getParent().getExceptionSuccessorInstruction(kind, isSeh)
+    )
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
-    result = this.getHandler(0).getFirstInstruction(kind)
-    or
-    not exists(this.getHandler(_)) and
-    result = this.getFinally().getFirstInstruction(kind)
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
+    // SEH exceptions are only handled for SEH try statements and
+    // C++ exceptions for C++ try statements.
+    // I.e., we are assuming there isn't a mix and match between SEH and C++ exceptions.
+    // They are either all SEH or all C++ within a single try block depending on the
+    // try type (TryStmt vs MicrosoftTryStmt).
+    (
+      stmt instanceof TryStmt and isSeh = false
+      or
+      stmt instanceof MicrosoftTryStmt and isSeh = true
+    ) and
+    (
+      result = this.getHandler(0).getFirstInstruction(kind)
+      or
+      not exists(this.getHandler(_)) and
+      result = this.getFinally().getFirstInstruction(kind)
+    )
   }
 
   private TranslatedElement getHandler(int index) { result = stmt.getTranslatedHandler(index) }
@@ -821,10 +839,10 @@ abstract class TranslatedHandler extends TranslatedStmt {
     child = this.getBlock() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `catch` block flows to the handler for the parent of
     // the `try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 
   TranslatedStmt getBlock() { result = getTranslatedStmt(stmt.getBlock()) }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
index 0bf2dd31fe40..8c3ae368da9d 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
@@ -9,7 +9,7 @@ import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
 import semmle.code.cpp.models.interfaces.Taint
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard functions `memcpy`, `memmove` and `bcopy`; and the gcc variant
@@ -106,6 +106,8 @@ private class MemcpyFunction extends ArrayFunction, DataFlowFunction, SideEffect
     not this.hasGlobalName(["bcopy", mempcpy(), "memccpy"]) and
     index = this.getParamDest()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 private string mempcpy() { result = ["mempcpy", "wmempcpy"] }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
index ab2e0af99f38..6a4ab8a133f2 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
@@ -8,7 +8,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 private class MemsetFunctionModel extends ArrayFunction, DataFlowFunction, AliasFunction,
   SideEffectFunction, NonThrowingFunction
@@ -74,6 +74,8 @@ private class MemsetFunctionModel extends ArrayFunction, DataFlowFunction, Alias
     i = 0 and
     if this.hasGlobalName(bzero()) then result = 1 else result = 2
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 private string bzero() { result = ["bzero", "explicit_bzero"] }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
index b0f76ee6538a..ee05b2a68a0b 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
@@ -1,4 +1,4 @@
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * A function that is annotated with a `noexcept` specifier (or the equivalent
@@ -8,4 +8,6 @@ import semmle.code.cpp.models.interfaces.NonThrowing
  */
 class NoexceptFunction extends NonThrowingFunction {
   NoexceptFunction() { this.isNoExcept() or this.isNoThrow() }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
index 7286552e3ee0..8e94dba0ddbb 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
@@ -8,7 +8,7 @@
 import semmle.code.cpp.models.interfaces.FormattingFunction
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard functions `printf`, `wprintf` and their glib variants.
@@ -32,6 +32,8 @@ private class Printf extends FormattingFunction, AliasFunction, NonThrowingFunct
   override predicate parameterEscapesOnlyViaReturn(int n) { none() }
 
   override predicate parameterIsAlwaysReturned(int n) { none() }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -50,6 +52,8 @@ private class Fprintf extends FormattingFunction, NonThrowingFunction {
   override int getFormatParameterIndex() { result = 1 }
 
   override int getOutputParameterIndex(boolean isStream) { result = 0 and isStream = true }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -93,6 +97,8 @@ private class Sprintf extends FormattingFunction, NonThrowingFunction {
     then result = 4
     else result = this.getNumberOfParameters()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -165,6 +171,8 @@ private class SnprintfImpl extends Snprintf, AliasFunction, SideEffectFunction,
     // We don't know how many parameters are passed to the function since it's varargs, but they also have read side effects.
     i = this.getFormatParameterIndex() and buffer = true
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -215,4 +223,6 @@ private class Syslog extends FormattingFunction, NonThrowingFunction {
   override int getFormatParameterIndex() { result = 1 }
 
   override predicate isOutputGlobal() { any() }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
index 9b11ed0af153..df85c56148a8 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
@@ -7,7 +7,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard function `strcat` and its wide, sized, and Microsoft variants.
@@ -94,6 +94,8 @@ class StrcatFunction extends TaintFunction, DataFlowFunction, ArrayFunction, Sid
     (i = 0 or i = 1) and
     buffer = true
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
index b7f06f0cebf4..b09cbeb8dc60 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
@@ -7,7 +7,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard function `strcpy` and its wide, sized, and Microsoft variants.
@@ -145,4 +145,6 @@ class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, Sid
     i = this.getParamDest() and
     result = this.getParamSize()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index af8f3088f255..d5941488d0d7 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -1,9 +1,26 @@
 import semmle.code.cpp.models.interfaces.Throwing
 
-class WindowsDriverFunction extends ThrowingFunction {
-  WindowsDriverFunction() {
+/**
+ * The default behavior for Structured Exception Handling (SEH) is
+ * any function may (conditionally) raise an exception.
+ * NOTE: this can be overridden by for any specific function to make in
+ * unconditional or non-throwing. IR generation will enforce
+ * the most strict interpretation.
+ */
+class DefaultSehExceptionBehavior extends ThrowingFunction {
+  DefaultSehExceptionBehavior() { any() }
+
+  override predicate raisesException(boolean unconditional) { unconditional = false }
+
+  override TSehException getExceptionType() { any() }
+}
+
+class WindowsDriverExceptionAnnotation extends ThrowingFunction {
+  WindowsDriverExceptionAnnotation() {
     this.hasGlobalName(["RaiseException", "ExRaiseAccessViolation", "ExRaiseDatatypeMisalignment"])
   }
 
-  final override predicate mayThrowException(boolean unconditional) { unconditional = true }
+  override predicate raisesException(boolean unconditional) { unconditional = true }
+
+  override TSehException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll
deleted file mode 100644
index 64901d39ad30..000000000000
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll
+++ /dev/null
@@ -1,11 +0,0 @@
-/**
- * Provides an abstract class for modeling functions that never throw.
- */
-
-import semmle.code.cpp.Function
-import semmle.code.cpp.models.Models
-
-/**
- * A function that is guaranteed to never throw.
- */
-abstract class NonThrowingFunction extends Function { }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 79b7523f1d9f..72db8c9e96c7 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -11,12 +11,71 @@ import semmle.code.cpp.models.Models
 import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
 
 /**
- * A class that models the exceptional behavior of a function.
+ * Represents a type of exception,
+ * either Structured Exception Handling (SEH) or C++ exceptions.
  */
-abstract class ThrowingFunction extends Function {
+newtype TException =
+  /** Structured Exception Handling (SEH) exception */
+  TSehException() or
+  /** C++ exception */
+  TCxxException()
+
+/**
+ * Functions with information about how an exception is thrown or if one is thrown at all.
+ * If throwing details conflict for the same function, IR is assumed
+ * to use the most restricted interpretation, meaning taking options
+ * that stipulate no exception is raised, before the exception is always raised,
+ * before conditional exceptions.
+ *
+ * Annotations must specify if the exception is from SEH (structured exception handling)
+ * or ordinary c++ exceptions.
+ */
+abstract private class ExceptionAnnotation extends Function {
+  /**
+   * Returns the type of exception this annotation is for,
+   * either a CPP exception or a STructured Exception Handling (SEH) exception.
+   */
+  abstract TException getExceptionType();
+
+  /**
+   * Holds if the exception type of this annotation is for a Structured Exception Handling (SEH) exception.
+   */
+  final predicate isSeh() { this.getExceptionType() = TSehException() }
+
+  /**
+   * Holds if the exception type of this annotation is for a CPP exception.
+   */
+  final predicate isCxx() { this.getExceptionType() = TCxxException() }
+}
+
+/**
+ * A Function that is known to not throw an exception.
+ */
+abstract class NonThrowingFunction extends ExceptionAnnotation { }
+
+/**
+ * A function this is known to raise an exception.
+ */
+abstract class ThrowingFunction extends ExceptionAnnotation {
+  ThrowingFunction() { any() }
+
+  /**
+   * Holds if this function may raise an exception during evaluation.
+   * If `unconditional` is `false` the function may raise, and if `true` the function
+   * will always raise an exception.
+   * Do not specify `none()` if no exception is raised, instead use the
+   * `NonThrowingFunction` class instead.
+   */
+  abstract predicate raisesException(boolean unconditional);
+
+  /**
+   * Holds if this function will always raise an exception if called
+   */
+  final predicate alwaysRaisesException() { this.raisesException(true) }
+
   /**
-   * Holds if this function may throw an exception during evaluation.
-   * If `unconditional` is `true` the function always throws an exception.
+   * Holds if this function may raise an exception if called but
+   * it is not guaranteed to do so. I.e., the function does not always raise an exception.
    */
-  abstract predicate mayThrowException(boolean unconditional);
+  final predicate mayRaiseException() { this.raisesException(false) }
 }