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.
We need this for scalar as well as aggregate type of undef value.
It would be nice to have a choice:
__VERIFIER_nondet_*(depending on type).