Hi, I've just run into a Klee "out of bound pointer" error which I believe it is actually not a bug in the program I'm testing, but some error in Klee.
I tried to analyze the associated test.ptr.err file generated, but I don't quite understand the meaning of "next" and "prev" addresses in the information given. In my case, address: 18446744073709366704 next: object at 140550159429952 of size 768 prev: object at 254899360 of size 72 As far as I deduced from the code that generates this output, next and prev correspond to the upper_bound() and lower_bound() values of the offending address in the sorted map that keeps all the allocated memory objects. Because of this, I expected that next > address > prev, which clearly is not the case here. Another observation which might be relevant is that the address value in 64-bit hexa is 0xFFFFFFFFFFFD2DB0, which looks like a small negative value or an address from the end of the memory space (maybe on the stack?). Do you have any insights about this issue? Thanks, Stefan
