The easiest solution is probably to make the entire object symbolic, and then to store the concrete values from the binary header into the fields you want to concretize. -David
On Jul 18, 2011, at 2:18 PM, Manizzle wrote: > Hey guys. So I am working on a problem where I am testing the binary > parsing capabilities of some code. Example, some binary has a header > field, and then the payload of the file. To test the effectiveness of > the parsing, one would like to make the header fields symbolic. This is, > however, not possible as the header field is not the whole object of the > byte buffer, and thus resulting in an error of > wrong size given to klee_make_symbolic[_name] > > Is this a feature that needs to be added to KLEE or is there something I > am missing? Thanks > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
