Modeling LLVM's poison values

[keram88]

Smack does not currently model LLVM's poison values. These arise as the result of invalid computations. It's not clear what this actually means for verification, however these can arise, for example, from generating out-of-bounds addresses with a getelementpointer instruction marked inbounds. Memory safety checking will detect this specific case, but a poison value pointer could be brought back in range and will be fine according to SMACK, however it should still be a poison value. Again, it is not clear what if anything SMACK should do here. Some related reading about the semantics of this can be found here: https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf