Manizzle, Whenever you read from an object at a symbolic offset, KLEE internally returns a symbolic expression with an update list that contains each byte that might be accessed by the read. It seems like you're doing this on a very large object, so KLEE is blowing up.
-David On Jul 18, 2011, at 3:06 PM, Manizzle wrote: > So i have this behaviour in my code. where header fields are added > together to produce a offset. this offset is used to create a struct* by > struct* casting the main data buffer at that particular offset. eg. > offset = somedata; offset += someotherdata; dataptr = (struct* > datstruct)&maindatabuffer[offset]. this goes fine. but now, as soon as > this dataptr is derefenced in anyway, i get a klee crash of KLEE: > WARNING: flushing 165888 bytes on read, may be slow and/or > crash:MO53[165888] allocated at global:load_buf. > > This crash only occurs when i have somdata and/or someotherdata set to > be symbolic. > > I run klee in gdb and run a bt, http://paste.org/pastebin/view/36263 > Just cant seem to pin down what is happening. > Has anyone had this problem or hints where to go from here? > _______________________________________________ > klee-dev mailing list > klee-dev@keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
