constval/createUndefValue: replacing LLVM undef value by all zeros is not accurate
tomsik68 opened this issue · 1 comments
tomsik68 commented
We need this for scalar as well as aggregate type of undef value.
It would be nice to have a choice:
- The default behavior could be to crash with an error message that undef value doesn't translate to C.
- For sv-comp compatible verifiers, we need an option to replace undef values by
__VERIFIER_nondet_*
(depending on type). - We can still have the option to replace undef value by zero, but user has to ask for it explicitly.
tomsik68 commented
Actually, undef value can easily be created in C by allocating a variable without assigning any value to it. This is a better candidate for the default behavior than crashing.
int main() {
int a;
return a;
}