OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole?

[Ronald F. Guilmette]

In message <CAG5KPzw_cOfFLX_kn=5DWAX+z+9VeXuzo3Q8YekDJG37tDQ_wQ at mail.gmail.com>
Ben Laurie <benl at freebsd.org> wrote:

>But that would then hide the error condition of it being not set to a
>new value after initialisation.

The (modified/quieted) code example under discussion is as follows:

	variable = value0;  /* initialization */
	if (condition) variable = value1;
	if (!condition) variable = value2;
	use (variable);

Please note that variable *is* *always* set to some value (either value1
or value2) after initialization.  The "error condition" that you seem
concerned about having explicitly flagged does not in fact exist in the
example code snippet under discussion.

>One better answer would be to have a way to annotate that after the
>two conditionals you assert that |variable| is initialised. Then a
>future, smarter static analyzer can attempt to prove you wrong.

Sir, is there any sense in which the final line of the above example
_does not_ already and standing all by itself constitute an implicit
assertion that "variable" has been initialized by that point in the
code?


Regards,
rfg