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
