Hi Stefan, The invariant you mention should indeed hold. I've never seen a violation on a 32-bit machine. But I encountered a similar issue on 64-bit, where I think the next address should have been "none". I don't have time to debug this any further, but let me know if you do.
Best, Cristian On 11/04/10 01:11, Stefan Bucur wrote: > 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 > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
