Uninitialized variables should have possibly-distinct values. about smack HOT 7 OPEN

Note: it is the --mem2reg flag, which we pass to llvm, that ultimately introduces these "undefined" values.

from smack.

At the moment, the only way I see to resolve this issue is to disable LLVM's mem2reg pass, which I advise against, due to the mess of additional memory operations in the code we would generate if we did.

from smack.

According to the LLVM reference manual, each "undef" should correspond to a unique uninitialized value, so actually the previous comment is irrelevant.

from smack.

I was wondering if it's still valid to assume that undefined values should hold the same value. I couldn't find any references now and intuitively they should be distinct.

from smack.

How do we translate this now?

from smack.

We create a global variable for undefined values of a type.

from smack.

If I remember this correctly, undef is between our current implementation and using verifier_nondet to model it. In particular, I think that undef in a loop for example should always evaluate to the same nondeterministic value. If that makes sense.
I can't find this discussion anywhere now.

from smack.