Its not every possible struct. Its a single symbolic representation of all values that might have been read by the symbolic offset read. STP can then reason about this representation.
Sent from my iPhone On Jul 18, 2011, at 5:29 PM, Manizzle <manizzle....@gmail.com> wrote: > On 07/18/2011 03:40 PM, David A. Ramos wrote: >> 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 >> > So basically KLEE is generating every possible struct through what, > bruteforce? _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
