MartinNowack

@paulmar I guess you know, but if somebody wants to implement a bug fix, `AddressSpace::copyInConcretes()` in lib/Core/AddressSpace.cpp should be extended to mark changes as concrete in the `ObjectState`. According to...

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

@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.

As far as I know, this is indeed currently a limitation. Can you try to workaround that issue, by first, initializing the whole structure as symbolic and then setting the...

@jirislaby Woooow good to know. So, yes - there are also LLVM builds with assertions enabled as well. I think there is a bug in KLEE for debug information. It...

@jirislaby By the way, to build this locally you now have two options: * build a docker image * build it in a local directory Just provide the options you...

@jirislaby I debugged the case a bit. First, it wasn't me. Yeah. And as I suspected, using LLVM with assertions makes this problem explicit, which is a good thing. The...

@jirislaby #945, #946, #949 are a concerted effort to fix this issue. As a sidenote, we currently have that problem already with LLVM 3.8, as soon as `--optimize` is used...

@jirislaby #945, #946, #949 is merged now. We can close this.

@andrewvaughanj Can you run KLEE with the following option: `--disable-verify` this should workaround your problem without recompiling anything. Please let me know if this works.