Should `undef` be treated as zero?

[delcypher]

In Executor::evalConstant(const Constant *c) undef is treated as zero. We might want to provide an option to introduce symbolic data instead if this happens.

[MartinNowack]

@delcypher This is very good point. Do we have other code locations where a similar behavior would be appropriate as well?

[delcypher]

@MartinNowack I'm not sure. This is just one I stumbled across recently which I thought seemed a little odd.

[MartinNowack]

@delcypher We can also have this option for Executor::Alloc the call of the initializeToRandom() after allocating memory (Same for globals.). This would allow us to find uninitialized memory bugs.

[ccadar]

Indeed, I think this would be a nice extension to KLEE. I would guard all these calls with the same option.