You can implement it yourself quite easily. Here's an example implementation of
a function that can mark a particular range of bytes as symbolic. Hope that
helps.
M
void klee_make_symbolic_range(void* addr, size_t offset, size_t nbytes, const
char* name) {
assert(addr != NULL && "Must pass a valid addr");
assert(name != NULL && "Must pass a valid name");
if(nbytes == 0)
return;
// this function can be made a primitive but it will require changes to
the ktest file format
void* start = addr + offset;
klee_check_memory_access(start, nbytes);
void* symbolic_data = malloc(nbytes);
klee_make_symbolic(symbolic_data, nbytes, name);
memcpy(start, symbolic_data, nbytes);
free(symbolic_data);
}
On 18 Jul 2011, at 21: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
>
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
