Hi Manizzle, On 18.07.11 22:18, 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
in KLEE, it's not possible to declare parts of an object to be symbolic directly. Simply declare a temporary byte buffer, make it symbolic, and use memcpy to write the symbolic data into the object. - Raimondas _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
