Merge branch 'main' into no-dtt-in-unbounded-write

2026-04-19 05:54:00 +02:00 · 2023-11-08 15:06:59 +00:00
parent e90803a81c 512c6a59c5
commit 38bd893c81
81 changed files with 861 additions and 523 deletions
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/MustFlow.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/MustFlow.qll
@@ -31,6 +31,11 @@ abstract class MustFlowConfiguration extends string {
   */
  abstract predicate isSink(Operand sink);

+  /**
+   * Holds if data flow through `instr` is prohibited.
+   */
+  predicate isBarrier(Instruction instr) { none() }
+
  /**
   * Holds if the additional flow step from `node1` to `node2` must be taken
   * into account in the analysis.
@@ -48,18 +53,21 @@ abstract class MustFlowConfiguration extends string {
   */
  final predicate hasFlowPath(MustFlowPathNode source, MustFlowPathSink sink) {
    this.isSource(source.getInstruction()) and
-    source.getASuccessor+() = sink
+    source.getASuccessor*() = sink
  }
 }

 /** Holds if `node` flows from a source. */
 pragma[nomagic]
 private predicate flowsFromSource(Instruction node, MustFlowConfiguration config) {
-  config.isSource(node)
-  or
-  exists(Instruction mid |
-    step(mid, node, config) and
-    flowsFromSource(mid, pragma[only_bind_into](config))
+  not config.isBarrier(node) and
+  (
+    config.isSource(node)
+    or
+    exists(Instruction mid |
+      step(mid, node, config) and
+      flowsFromSource(mid, pragma[only_bind_into](config))
+    )
  )
 }

--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticCFG.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticCFG.qll
@@ -12,9 +12,6 @@ class SemBasicBlock extends Specific::BasicBlock {
  /** Holds if this block (transitively) dominates `otherblock`. */
  final predicate bbDominates(SemBasicBlock otherBlock) { Specific::bbDominates(this, otherBlock) }

-  /** Holds if this block has dominance information. */
-  final predicate hasDominanceInformation() { Specific::hasDominanceInformation(this) }
-
  /** Gets an expression that is evaluated in this basic block. */
  final SemExpr getAnExpr() { result.getBasicBlock() = this }

--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
@@ -122,8 +122,6 @@ module SemanticExprConfig {
    dominator.dominates(dominated)
  }

-  predicate hasDominanceInformation(BasicBlock block) { any() }
-
  private predicate id(Cpp::Locatable x, Cpp::Locatable y) { x = y }

  private predicate idOf(Cpp::Locatable x, int y) = equivalenceRelation(id/2)(x, y)
@@ -132,17 +130,7 @@ module SemanticExprConfig {

  newtype TSsaVariable =
    TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
-    TSsaOperand(IR::Operand op) { op.isDefinitionInexact() } or
-    TSsaPointerArithmeticGuard(ValueNumber instr) {
-      exists(Guard g, IR::Operand use |
-        use = instr.getAUse() and use.getIRType() instanceof IR::IRAddressType
-      |
-        g.comparesLt(use, _, _, _, _) or
-        g.comparesLt(_, use, _, _, _) or
-        g.comparesEq(use, _, _, _, _) or
-        g.comparesEq(_, use, _, _, _)
-      )
-    }
+    TSsaOperand(IR::Operand op) { op.isDefinitionInexact() }

  class SsaVariable extends TSsaVariable {
    string toString() { none() }
@@ -151,8 +139,6 @@ module SemanticExprConfig {

    IR::Instruction asInstruction() { none() }

-    ValueNumber asPointerArithGuard() { none() }
-
    IR::Operand asOperand() { none() }
  }

@@ -168,18 +154,6 @@ module SemanticExprConfig {
    final override IR::Instruction asInstruction() { result = instr }
  }

-  class SsaPointerArithmeticGuard extends SsaVariable, TSsaPointerArithmeticGuard {
-    ValueNumber vn;
-
-    SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(vn) }
-
-    final override string toString() { result = vn.toString() }
-
-    final override Location getLocation() { result = vn.getLocation() }
-
-    final override ValueNumber asPointerArithGuard() { result = vn }
-  }
-
  class SsaOperand extends SsaVariable, TSsaOperand {
    IR::Operand op;

@@ -212,11 +186,7 @@ module SemanticExprConfig {
    )
  }

-  Expr getAUse(SsaVariable v) {
-    result.(IR::LoadInstruction).getSourceValue() = v.asInstruction()
-    or
-    result = v.asPointerArithGuard().getAnInstruction()
-  }
+  Expr getAUse(SsaVariable v) { result.(IR::LoadInstruction).getSourceValue() = v.asInstruction() }

  SemType getSsaVariableType(SsaVariable v) {
    result = getSemanticType(v.asInstruction().getResultIRType())
@@ -255,10 +225,7 @@ module SemanticExprConfig {
    final override Location getLocation() { result = block.getLocation() }

    final override predicate hasRead(SsaVariable v) {
-      exists(IR::Operand operand |
-        operand.getDef() = v.asInstruction() or
-        operand.getDef() = v.asPointerArithGuard().getAnInstruction()
-      |
+      exists(IR::Operand operand | operand.getDef() = v.asInstruction() |
        not operand instanceof IR::PhiInputOperand and
        operand.getUse().getBlock() = block
      )
@@ -276,10 +243,7 @@ module SemanticExprConfig {
    final override Location getLocation() { result = succ.getLocation() }

    final override predicate hasRead(SsaVariable v) {
-      exists(IR::PhiInputOperand operand |
-        operand.getDef() = v.asInstruction() or
-        operand.getDef() = v.asPointerArithGuard().getAnInstruction()
-      |
+      exists(IR::PhiInputOperand operand | operand.getDef() = v.asInstruction() |
        operand.getPredecessorBlock() = pred and
        operand.getUse().getBlock() = succ
      )
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll
@@ -35,32 +35,4 @@ predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
  Specific::implies_v2(g1, b1, g2, b2)
 }

-/**
- * Holds if `guard` directly controls the position `controlled` with the
- * value `testIsTrue`.
- */
-pragma[nomagic]
-predicate semGuardDirectlyControlsSsaRead(
-  SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue
-) {
-  guard.directlyControls(controlled.(SemSsaReadPositionBlock).getBlock(), testIsTrue)
-  or
-  exists(SemSsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
-    guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
-    guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
-  )
-}
-
-/**
- * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
- */
-predicate semGuardControlsSsaRead(SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue) {
-  semGuardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
-  or
-  exists(SemGuard guard0, boolean testIsTrue0 |
-    semImplies_v2(guard0, testIsTrue0, guard, testIsTrue) and
-    semGuardControlsSsaRead(guard0, controlled, testIsTrue0)
-  )
-}
-
 SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
@@ -63,36 +63,3 @@ class SemSsaReadPositionBlock extends SemSsaReadPosition {

  SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
 }
-
-/**
- * Holds if `inp` is an input to `phi` along a back edge.
- */
-predicate semBackEdge(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge) {
-  edge.phiInput(phi, inp) and
-  // Conservatively assume that every edge is a back edge if we don't have dominance information.
-  (
-    phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
-    irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock()) or
-    not edge.getOrigBlock().hasDominanceInformation()
-  )
-}
-
-/**
- * Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
- * graph.
- *
- * An ireducible control flow graph is one where the usual dominance-based back edge detection does
- * not work, because there is a cycle with multiple entry points, meaning there are
- * mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
- * remove all detectable back-edges using the normal condition that the predecessor block is
- * dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
- * edges.
- */
-private predicate irreducibleSccEdge(SemBasicBlock b1, SemBasicBlock b2) {
-  trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
-}
-
-private predicate trimmedEdge(SemBasicBlock pred, SemBasicBlock succ) {
-  pred.getASuccessor() = succ and
-  not succ.bbDominates(pred)
-}
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
@@ -72,14 +72,12 @@ module Sem implements Semantic {

  class BasicBlock = SemBasicBlock;

+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
  class Guard = SemGuard;

  predicate implies_v2 = semImplies_v2/4;

-  predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
-
-  predicate guardControlsSsaRead = semGuardControlsSsaRead/3;
-
  class Type = SemType;

  class IntegerType = SemIntegerType;
@@ -100,8 +98,6 @@ module Sem implements Semantic {

  class SsaReadPositionBlock = SemSsaReadPositionBlock;

-  predicate backEdge = semBackEdge/3;
-
  predicate conversionCannotOverflow(Type fromType, Type toType) {
    SemanticType::conversionCannotOverflow(fromType, toType)
  }
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
@@ -294,7 +294,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
  ) {
    exists(boolean testIsTrue, SemRelationalExpr comp |
      pos.hasReadOfVar(v) and
-      semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
+      guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
      not unknownSign(lowerbound)
    |
      testIsTrue = true and
@@ -318,7 +318,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
  ) {
    exists(boolean testIsTrue, SemRelationalExpr comp |
      pos.hasReadOfVar(v) and
-      semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
+      guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
      not unknownSign(upperbound)
    |
      testIsTrue = true and
@@ -343,7 +343,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
  private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
    exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
      pos.hasReadOfVar(pragma[only_bind_into](v)) and
-      semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
+      guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
      e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
      guard.isEquality(eqbound, e, polarity) and
      isEq = polarity.booleanXor(testIsTrue).booleanNot() and
--- a/Management/UninitializedLocal.ql
+++ b/Management/UninitializedLocal.ql
@@ -13,7 +13,8 @@
 */

 import cpp
-import semmle.code.cpp.controlflow.StackVariableReachability
+import semmle.code.cpp.ir.IR
+import semmle.code.cpp.ir.dataflow.MustFlow

 /**
 * Auxiliary predicate: Types that don't require initialization
@@ -33,31 +34,6 @@ predicate allocatedType(Type t) {
  allocatedType(t.getUnspecifiedType())
 }

-/**
- * A declaration of a local variable that leaves the
- * variable uninitialized.
- */
-DeclStmt declWithNoInit(LocalVariable v) {
-  result.getADeclaration() = v and
-  not exists(v.getInitializer()) and
-  /* The type of the variable is not stack-allocated. */
-  exists(Type t | t = v.getType() | not allocatedType(t))
-}
-
-class UninitialisedLocalReachability extends StackVariableReachability {
-  UninitialisedLocalReachability() { this = "UninitialisedLocal" }
-
-  override predicate isSource(ControlFlowNode node, StackVariable v) { node = declWithNoInit(v) }
-
-  override predicate isSink(ControlFlowNode node, StackVariable v) { useOfVarActual(v, node) }
-
-  override predicate isBarrier(ControlFlowNode node, StackVariable v) {
-    // only report the _first_ possibly uninitialized use
-    useOfVarActual(v, node) or
-    definitionBarrier(v, node)
-  }
-}
-
 pragma[noinline]
 predicate containsInlineAssembly(Function f) { exists(AsmStmt s | s.getEnclosingFunction() = f) }

@@ -82,8 +58,33 @@ VariableAccess commonException() {
  containsInlineAssembly(result.getEnclosingFunction())
 }

-from UninitialisedLocalReachability r, LocalVariable v, VariableAccess va
+predicate isSinkImpl(Instruction sink, VariableAccess va) {
+  exists(LoadInstruction load |
+    va = load.getUnconvertedResultExpression() and
+    not va = commonException() and
+    sink = load.getSourceValue()
+  )
+}
+
+class MustFlow extends MustFlowConfiguration {
+  MustFlow() { this = "MustFlow" }
+
+  override predicate isSource(Instruction source) {
+    source instanceof UninitializedInstruction and
+    exists(Type t | t = source.getResultType() | not allocatedType(t))
+  }
+
+  override predicate isSink(Operand sink) { isSinkImpl(sink.getDef(), _) }
+
+  override predicate allowInterproceduralFlow() { none() }
+
+  override predicate isBarrier(Instruction instr) { instr instanceof ChiInstruction }
+}
+
+from
+  VariableAccess va, LocalVariable v, MustFlow conf, MustFlowPathNode source, MustFlowPathNode sink
 where
-  r.reaches(_, v, va) and
-  not va = commonException()
+  conf.hasFlowPath(source, sink) and
+  isSinkImpl(sink.getInstruction(), va) and
+  v = va.getTarget()
 select va, "The variable $@ may not be initialized at this access.", v, v.getName()
--- a/cpp/ql/src/change-notes/2023-11-07-uninitialized-local.md
+++ b/cpp/ql/src/change-notes/2023-11-07-uninitialized-local.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The `cpp/uninitialized-local` query has been improved to produce fewer false positives.
--- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
+++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
@@ -134,6 +134,12 @@ void test_div(int x) {
 struct X { int n; };
 void read_argument(const X *);

+// This test exists purely to ensure that modulus analysis terminates in the
+// presence of inexact phi operands. The LoadInstruction on `while(x->n) { ... }`
+// reads from a PhiInstruction with two input operands: an exact operand defined
+// by the StoreInstruction generated by `x->n--` and an inexact operand coming
+// from the WriteSideEffect generated by `read_argument(x)`. If we don't consider
+// the inexact operand modulus analysis fails to terminate.
 void nonterminating_without_operands_as_ssa(X *x) {
  read_argument(x);
  while (x->n) {
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
@@ -22,10 +22,6 @@ edges
 | test.cpp:52:19:52:37 | call to malloc | test.cpp:53:12:53:23 | ... + ... |
 | test.cpp:53:12:53:23 | ... + ... | test.cpp:51:33:51:35 | end |
 | test.cpp:60:34:60:37 | mk_array output argument | test.cpp:67:9:67:14 | ... = ... |
-| test.cpp:194:15:194:33 | call to malloc | test.cpp:195:17:195:23 | ... + ... |
-| test.cpp:195:17:195:23 | ... + ... | test.cpp:195:17:195:23 | ... + ... |
-| test.cpp:195:17:195:23 | ... + ... | test.cpp:201:5:201:19 | ... = ... |
-| test.cpp:195:17:195:23 | ... + ... | test.cpp:201:5:201:19 | ... = ... |
 | test.cpp:205:15:205:33 | call to malloc | test.cpp:206:17:206:23 | ... + ... |
 | test.cpp:206:17:206:23 | ... + ... | test.cpp:206:17:206:23 | ... + ... |
 | test.cpp:206:17:206:23 | ... + ... | test.cpp:213:5:213:13 | ... = ... |
@@ -125,10 +121,6 @@ nodes
 | test.cpp:53:12:53:23 | ... + ... | semmle.label | ... + ... |
 | test.cpp:60:34:60:37 | mk_array output argument | semmle.label | mk_array output argument |
 | test.cpp:67:9:67:14 | ... = ... | semmle.label | ... = ... |
-| test.cpp:194:15:194:33 | call to malloc | semmle.label | call to malloc |
-| test.cpp:195:17:195:23 | ... + ... | semmle.label | ... + ... |
-| test.cpp:195:17:195:23 | ... + ... | semmle.label | ... + ... |
-| test.cpp:201:5:201:19 | ... = ... | semmle.label | ... = ... |
 | test.cpp:205:15:205:33 | call to malloc | semmle.label | call to malloc |
 | test.cpp:206:17:206:23 | ... + ... | semmle.label | ... + ... |
 | test.cpp:206:17:206:23 | ... + ... | semmle.label | ... + ... |
@@ -214,7 +206,6 @@ subpaths
 | test.cpp:30:14:30:15 | * ... | test.cpp:28:15:28:37 | call to malloc | test.cpp:30:14:30:15 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:28:15:28:37 | call to malloc | call to malloc | test.cpp:29:20:29:27 | ... + ... | ... + ... |
 | test.cpp:32:14:32:21 | * ... | test.cpp:28:15:28:37 | call to malloc | test.cpp:32:14:32:21 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:28:15:28:37 | call to malloc | call to malloc | test.cpp:29:20:29:27 | ... + ... | ... + ... |
 | test.cpp:67:9:67:14 | ... = ... | test.cpp:52:19:52:37 | call to malloc | test.cpp:67:9:67:14 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:52:19:52:37 | call to malloc | call to malloc | test.cpp:53:20:53:23 | size | size |
-| test.cpp:201:5:201:19 | ... = ... | test.cpp:194:15:194:33 | call to malloc | test.cpp:201:5:201:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:194:15:194:33 | call to malloc | call to malloc | test.cpp:195:21:195:23 | len | len |
 | test.cpp:213:5:213:13 | ... = ... | test.cpp:205:15:205:33 | call to malloc | test.cpp:213:5:213:13 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:205:15:205:33 | call to malloc | call to malloc | test.cpp:206:21:206:23 | len | len |
 | test.cpp:264:13:264:14 | * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
 | test.cpp:274:5:274:10 | ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len |
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-193/test.cpp
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-193/test.cpp
@@ -198,7 +198,7 @@ void test12(unsigned len, unsigned index) {
        return;
    }
    
-    p[index] = '\0'; // $ deref=L195->L201 // BAD
+    p[index] = '\0'; // $ MISSING: deref=L195->L201 // BAD [NOT DETECTED]
 }

 void test13(unsigned len, unsigned index) {
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-457/semmle/tests/UninitializedLocal.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-457/semmle/tests/UninitializedLocal.expected
@@ -1,14 +1,7 @@
 | test.cpp:12:6:12:8 | foo | The variable $@ may not be initialized at this access. | test.cpp:11:6:11:8 | foo | foo |
-| test.cpp:30:6:30:8 | foo | The variable $@ may not be initialized at this access. | test.cpp:26:6:26:8 | foo | foo |
-| test.cpp:46:6:46:8 | foo | The variable $@ may not be initialized at this access. | test.cpp:42:6:42:8 | foo | foo |
-| test.cpp:55:7:55:9 | foo | The variable $@ may not be initialized at this access. | test.cpp:50:6:50:8 | foo | foo |
-| test.cpp:67:7:67:9 | foo | The variable $@ may not be initialized at this access. | test.cpp:61:6:61:8 | foo | foo |
-| test.cpp:92:6:92:8 | foo | The variable $@ may not be initialized at this access. | test.cpp:82:6:82:8 | foo | foo |
 | test.cpp:113:6:113:8 | foo | The variable $@ may not be initialized at this access. | test.cpp:111:6:111:8 | foo | foo |
-| test.cpp:132:9:132:9 | j | The variable $@ may not be initialized at this access. | test.cpp:126:6:126:6 | j | j |
 | test.cpp:219:3:219:3 | x | The variable $@ may not be initialized at this access. | test.cpp:218:7:218:7 | x | x |
 | test.cpp:243:13:243:13 | i | The variable $@ may not be initialized at this access. | test.cpp:241:6:241:6 | i | i |
-| test.cpp:329:9:329:11 | val | The variable $@ may not be initialized at this access. | test.cpp:321:6:321:8 | val | val |
 | test.cpp:336:10:336:10 | a | The variable $@ may not be initialized at this access. | test.cpp:333:7:333:7 | a | a |
 | test.cpp:369:10:369:10 | a | The variable $@ may not be initialized at this access. | test.cpp:358:7:358:7 | a | a |
 | test.cpp:378:9:378:11 | val | The variable $@ may not be initialized at this access. | test.cpp:359:6:359:8 | val | val |
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-457/semmle/tests/test.cpp
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-457/semmle/tests/test.cpp
@@ -27,7 +27,7 @@ void test4(bool b) {
 	if (b) {
 		foo = 1;
 	}
-	use(foo); // BAD
+	use(foo); // BAD [NOT DETECTED]
 }

 void test5() {
@@ -43,7 +43,7 @@ void test5(int count) {
 	for (int i = 0; i < count; i++) {
 		foo = i;
 	}
-	use(foo); // BAD
+	use(foo); // BAD [NOT DETECTED]
 }

 void test6(bool b) {
@@ -52,7 +52,7 @@ void test6(bool b) {
 		foo = 42;
 	}
 	if (b) {
-		use(foo); // GOOD (REPORTED, FP)
+		use(foo); // GOOD
 	}
 }

@@ -64,7 +64,7 @@ void test7(bool b) {
 		set = true;
 	}
 	if (set) {
-		use(foo); // GOOD (REPORTED, FP)
+		use(foo); // GOOD
 	}
 }

@@ -89,7 +89,7 @@ void test9(int count) {
 	if (!set) {
 		foo = 42;
 	}
-	use(foo); // GOOD (REPORTED, FP)
+	use(foo); // GOOD
 }

 void test10() {
@@ -129,7 +129,7 @@ int absWrong(int i) {
 	} else if (i < 0) {
 		j = -i;
 	}
-	return j; // wrong: j may not be initialized before use
+	return j; // wrong: j may not be initialized before use [NOT DETECTED]
 }

 // Example from qhelp
@@ -326,7 +326,7 @@ int test28() {
 		a = false;
 		c = false;
 	}
-	return val; // GOOD [FALSE POSITIVE]
+	return val; // GOOD
 }

 int test29() {
@@ -472,4 +472,64 @@ void test44() {
 	int y = 1;

 	void(x + y); // BAD
+}
+
+enum class State { StateA, StateB, StateC };
+
+int exhaustive_switch(State s) {
+	int y;
+	switch(s) {
+		case State::StateA:
+			y = 1;
+			break;
+		case State::StateB:
+			y = 2;
+			break;
+		case State::StateC:
+			y = 3;
+			break;
+	}
+	return y; // GOOD (y is always initialized)
+}
+
+int exhaustive_switch_2(State s) {
+	int y;
+	switch(s) {
+		case State::StateA:
+			y = 1;
+			break;
+		default:
+			y = 2;
+			break;
+	}
+	return y; // GOOD (y is always initialized)
+}
+
+int non_exhaustive_switch(State s) {
+	int y;
+	switch(s) {
+		case State::StateA:
+			y = 1;
+			break;
+		case State::StateB:
+			y = 2;
+			break;
+	}
+	return y; // BAD [NOT DETECTED] (y is not initialized when s = StateC)
+}
+
+int non_exhaustive_switch_2(State s) {
+	int y;
+	switch(s) {
+		case State::StateA:
+			y = 1;
+			break;
+		case State::StateB:
+			y = 2;
+			break;
+	}
+	if(s != State::StateC) {
+		return y; // GOOD (y is not initialized when s = StateC, but if s = StateC we won't reach this point)
+	}
+	return 0;
 }