[fweimer]

Uninitialized local variables are documented as a source of a certain type of nondeterminism: http://www.cprover.org/cprover-manual/modeling/nondeterminis...

So the checker treats them as defined, but with an unknown variable. You could have written this instead:

    extern int unknown_int_value(void);
    int x = unknown_int_value();

And leaving unknown_int_value undefined (so it's not visible to the analyzer). Or write a function and use x as a parameter.

I suspect CBMC does this to have a convenient syntax for this frequent scenario. Apparently, it's used quite often, as in these examples: https://model-checking.github.io/cbmc-training/cbmc/overview...

It seems that CBMC is not intended to check production sources directly against C semantics, but to prove things about programs written in a C-like syntax.