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();
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.
So the checker treats them as defined, but with an unknown variable. You could have written this instead:
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.