uninitialized check

[kroening]

Uninitialized local or dynamically allocated variables have an indeterminate initial value.

Reading an indeterminate value may be undefined behavior, or may yield an unspecific value.

This adds a check for uninitialized local variables. The check is not added as a standard check.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 38.70968% with 19 lines in your changes missing coverage. Please review.

Project coverage is 78.27%. Comparing base (f9a7807) to head (a8069ba).

Files with missing lines	Patch %	Lines
src/ansi-c/goto-conversion/goto_check_c.cpp	38.70%	19 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8545      +/-   ##
===========================================
- Coverage    78.38%   78.27%   -0.12%     
===========================================
  Files         1729     1729              
  Lines       200151   200453     +302     
  Branches     18244    18316      +72     
===========================================
+ Hits        156883   156895      +12     
- Misses       43268    43558     +290     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[rod-chapman]

Good to see this PR coming. What is your soundness argument? Does this check always detect all cases of uninitialized variables? Are there cases where it is known to miss? What are they?