How to avoid detecting uninitialized variables when using the impact analysis of Frama-C

Question

I find that if there is an uninitialized left-value (variable X for example) in the program, Frama-C asserts that X has been initialized, but then the assertion gets the final status invalid. It seems that Frama-C stops the analysis after detecting the invalid final status, so that the actual result of the impact analysis (the impacted statements) is just a part of the ideal result. I want Frama-C to proceed the impact analysis regardless of those uninitialized variables, but I haven't found any related options yet. How to deal with this problem?

Answer 1

You're invoking an undefined behavior as indicated in annex J.2 of ISO C standard "The value of an object with automatic storage duration is used while it is indeterminate" (Note to language lawyers: said annex is informative, and I've been unable to trace that claim back to the normative sections of the standard, at least for C11). The EVA plug-in, which is used internally by Impact analysis, restricts itself to execution paths that have a well-defined meaning according to the standard (the proverbial nasal demons are not part of the abstract domains of EVA). If there are no such paths, abstract execution will indeed stop. The appropriate way to deal with this problem is to ensure the local variables of the program under analysis are properly initialized before being accessed.

Update

I forgot to mention that in the next version (16 - Sulfur), whose beta version is available at https://github.com/Frama-C/Frama-C-snapshot/wiki/downloads/frama-c-Sulfur-20171101-beta.tar.gz, EVA has an option -val-initialized-locals, whose help specifies:

Local variables enter in scope fully initialized. Only useful for the analysis of programs buggy w.r.t. initialization.