On 07/18/2011 02:10 PM, Milen Dzhumerov wrote:
> 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
Yup Milen. Thats pretty much what I ended up doing. Thanks though.
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
