diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index f829ebeda7e..8d52fd3942c 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -53,6 +53,8 @@ class goto_check_ct
   {
     enable_bounds_check = _options.get_bool_option("bounds-check");
     enable_pointer_check = _options.get_bool_option("pointer-check");
+    enable_uninitialized_check =
+      _options.get_bool_option("uninitialized-check");
     enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
     enable_memory_cleanup_check =
       _options.get_bool_option("memory-cleanup-check");
@@ -157,11 +159,13 @@ class goto_check_ct
   ///   guard.
   /// \param expr: the expression to be checked
   /// \param guard: the condition for when the check should be made
-  void check_rec(const exprt &expr, const guardt &guard);
+  /// \param is_lhs: the expression is the LHS of an assignment
+  void check_rec(const exprt &, const guardt &, bool is_lhs);
 
   /// Initiate the recursively analysis of \p expr with its `guard' set to TRUE.
   /// \param expr: the expression to be checked
-  void check(const exprt &expr);
+  /// \param is_lhs: the expression is the LHS of an assignment
+  void check(const exprt &expr, bool is_lhs);
 
   struct conditiont
   {
@@ -187,6 +191,7 @@ class goto_check_ct
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const binary_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
+  void uninitialized_check(const symbol_exprt &, const guardt &);
   void memory_leak_check(const irep_idt &function_id);
 
   /// Generates VCCs for the validity of the given dereferencing operation.
@@ -263,6 +268,7 @@ class goto_check_ct
 
   bool enable_bounds_check;
   bool enable_pointer_check;
+  bool enable_uninitialized_check;
   bool enable_memory_leak_check;
   bool enable_memory_cleanup_check;
   bool enable_div_by_zero_check;
@@ -284,6 +290,7 @@ class goto_check_ct
   std::map<irep_idt, bool *> name_to_flag{
     {"bounds-check", &enable_bounds_check},
     {"pointer-check", &enable_pointer_check},
+    {"uninitialized-check", &enable_uninitialized_check},
     {"memory-leak-check", &enable_memory_leak_check},
     {"memory-cleanup-check", &enable_memory_cleanup_check},
     {"div-by-zero-check", &enable_div_by_zero_check},
@@ -1331,6 +1338,23 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
     guard);
 }
 
+void goto_check_ct::uninitialized_check(
+  const symbol_exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_uninitialized_check)
+    return;
+
+  add_guarded_property(
+    false_exprt{},
+    "reading uninitialized local",
+    "uninitialized",
+    true, // not fatal
+    expr.find_source_location(),
+    expr,
+    guard);
+}
+
 void goto_check_ct::pointer_rel_check(
   const binary_exprt &expr,
   const guardt &guard)
@@ -1807,13 +1831,13 @@ void goto_check_ct::check_rec_address(const exprt &expr, const guardt &guard)
 
   if(expr.id() == ID_dereference)
   {
-    check_rec(to_dereference_expr(expr).pointer(), guard);
+    check_rec(to_dereference_expr(expr).pointer(), guard, false);
   }
   else if(expr.id() == ID_index)
   {
     const index_exprt &index_expr = to_index_expr(expr);
     check_rec_address(index_expr.array(), guard);
-    check_rec(index_expr.index(), guard);
+    check_rec(index_expr.index(), guard, false);
   }
   else
   {
@@ -1843,7 +1867,7 @@ void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
       return guard(implication(conjunction(constraints), expr));
     };
 
-    check_rec(op, new_guard);
+    check_rec(op, new_guard, false);
 
     constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
   }
@@ -1855,20 +1879,20 @@ void goto_check_ct::check_rec_if(const if_exprt &if_expr, const guardt &guard)
     if_expr.cond().is_boolean(),
     "first argument of if must be boolean, but got " + if_expr.cond().pretty());
 
-  check_rec(if_expr.cond(), guard);
+  check_rec(if_expr.cond(), guard, false);
 
   {
     auto new_guard = [&guard, &if_expr](exprt expr) {
       return guard(implication(if_expr.cond(), std::move(expr)));
     };
-    check_rec(if_expr.true_case(), new_guard);
+    check_rec(if_expr.true_case(), new_guard, false);
   }
 
   {
     auto new_guard = [&guard, &if_expr](exprt expr) {
       return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
     };
-    check_rec(if_expr.false_case(), new_guard);
+    check_rec(if_expr.false_case(), new_guard, false);
   }
 }
 
@@ -1878,7 +1902,7 @@ bool goto_check_ct::check_rec_member(
 {
   const dereference_exprt &deref = to_dereference_expr(member.struct_op());
 
-  check_rec(deref.pointer(), guard);
+  check_rec(deref.pointer(), guard, false);
 
   // avoid building the following expressions when pointer_validity_check
   // would return immediately anyway
@@ -1969,7 +1993,7 @@ void goto_check_ct::check_rec_arithmetic_op(
   }
 }
 
-void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
+void goto_check_ct::check_rec(const exprt &expr, const guardt &guard, bool is_lhs)
 {
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
@@ -1980,7 +2004,7 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
       return guard(forall_exprt(quantifier_expr.symbol(), expr));
     };
 
-    check_rec(quantifier_expr.where(), new_guard);
+    check_rec(quantifier_expr.where(), new_guard, false);
     return;
   }
   else if(expr.id() == ID_address_of)
@@ -2007,7 +2031,7 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
   }
 
   for(const auto &op : expr.operands())
-    check_rec(op, guard);
+    check_rec(op, guard, false);
 
   if(expr.type().id() == ID_c_enum_tag)
     enum_range_check(expr, guard);
@@ -2048,6 +2072,10 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
   {
     pointer_validity_check(to_dereference_expr(expr), expr, guard);
   }
+  else if(expr.id() == ID_symbol)
+  {
+    uninitialized_check(to_symbol_expr(expr), guard);
+  }
   else if(requires_pointer_primitive_check(expr))
   {
     pointer_primitive_check(expr, guard);
@@ -2059,9 +2087,9 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
   }
 }
 
-void goto_check_ct::check(const exprt &expr)
+void goto_check_ct::check(const exprt &expr, bool is_lhs)
 {
-  check_rec(expr, identity);
+  check_rec(expr, identity, is_lhs);
 }
 
 void goto_check_ct::memory_leak_check(const irep_idt &function_id)
@@ -2151,7 +2179,7 @@ void goto_check_ct::goto_check(
 
     if(i.has_condition())
     {
-      check(i.condition());
+      check(i.condition(), false);
     }
 
     // magic ERROR label?
@@ -2184,12 +2212,12 @@ void goto_check_ct::goto_check(
 
       if(statement == ID_expression)
       {
-        check(code);
+        check(code, false);
       }
       else if(statement == ID_printf)
       {
         for(const auto &op : code.operands())
-          check(op);
+          check(op, false);
       }
     }
     else if(i.is_assign())
@@ -2202,10 +2230,10 @@ void goto_check_ct::goto_check(
       {
         flag_overridet resetter(i.source_location());
         resetter.disable_flag(enable_enum_range_check, "enum_range_check");
-        check(assign_lhs);
+        check(assign_lhs, true);
       }
 
-      check(assign_rhs);
+      check(assign_rhs, false);
 
       // the LHS might invalidate any assertion
       invalidate(assign_lhs);
@@ -2217,12 +2245,13 @@ void goto_check_ct::goto_check(
       {
         flag_overridet resetter(i.source_location());
         resetter.disable_flag(enable_enum_range_check, "enum_range_check");
-        check(i.call_lhs());
+        check(i.call_lhs(), true);
       }
-      check(i.call_function());
+
+      check(i.call_function(), false);
 
       for(const auto &arg : i.call_arguments())
-        check(arg);
+        check(arg, false);
 
       check_shadow_memory_api_calls(i);
 
@@ -2231,7 +2260,7 @@ void goto_check_ct::goto_check(
     }
     else if(i.is_set_return_value())
     {
-      check(i.return_value());
+      check(i.return_value(), false);
       // the return value invalidate any assertion
       invalidate(i.return_value());
     }
@@ -2342,7 +2371,7 @@ void goto_check_ct::check_shadow_memory_api_calls(
   {
     const exprt &expr = i.call_arguments()[0];
     PRECONDITION(expr.type().id() == ID_pointer);
-    check(dereference_exprt(expr));
+    check(dereference_exprt(expr), false);
   }
 }
 
diff --git a/src/ansi-c/goto-conversion/goto_check_c.h b/src/ansi-c/goto-conversion/goto_check_c.h
index e560634cf16..0f1a86d342e 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.h
+++ b/src/ansi-c/goto-conversion/goto_check_c.h
@@ -39,6 +39,7 @@ void goto_check_c(
 
 #define OPT_GOTO_CHECK                                                         \
   "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
+  "(uninitialized-check)"                                                      \
   "(div-by-zero-check)(float-div-by-zero-check)"                               \
   "(enum-range-check)"                                                         \
   "(signed-overflow-check)(unsigned-overflow-check)"                           \
@@ -51,6 +52,7 @@ void goto_check_c(
   "(assert-to-assume)"                                                         \
   "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
   "(no-pointer-primitive-check)(no-undefined-shift-check)"                     \
+  "(no-uninitialized-check)"                                                   \
   "(no-div-by-zero-check)"
 
 // clang-format off
@@ -59,6 +61,8 @@ void goto_check_c(
   " {y--bounds-check} \t enable array bounds checks (default on)\n"            \
   " {y--no-bounds-check} \t disable array bounds checks\n"                     \
   " {y--pointer-check} \t enable pointer checks (default on)\n"                \
+  " {y--uninitialized-check} \t enable checks for uninitialized data (default off)\n" \
+  " {y--no-uninitialized-check} \t disable checks for uninitialized data\n"    \
   " {y--no-pointer-check} \t disable pointer checks\n"                         \
   " {y--memory-leak-check} \t enable memory leak checks\n"                     \
   " {y--memory-cleanup-check} \t enable memory cleanup checks\n"               \
@@ -126,6 +130,7 @@ void goto_check_c(
     options.set_option("error-label", cmdline.get_values("error-label"));      \
   PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "uninitialized-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \