[klee-dev] execute function with symbolic argument

Dingbao Xie xiedingbao at gmail.com
Mon Dec 22 04:22:30 GMT 2014


Thanks for your reply.
Could you please tell me how to implement it?
Instrument a call to klee_make_symbolic at the start of function?

Regards
Dingbao

On Sun, Dec 21, 2014 at 7:28 PM, xiaoqixue_1 <xiaoqixue_1 at 163.com> wrote:

>
> Hi,
>
> I think it could be done well with klee if you only want run a function
> without complex memory accessing.
> and we have done some experiments.
>
> the challenges are :
> 1. how to handle the pointer argument , when it pointing to a structure.
> further more, if there are pointers in the structure.
> 2. how to address the global
> <http://cn.bing.com/dict/search?q=global&FORM=BDVSP6> variables
> <http://cn.bing.com/dict/search?q=variables&FORM=BDVSP6>.
> may be more..
>
>
> best regards
>
> xqx
>
>
>
>
>
> At 2014-12-20 23:33:28, "Hongxu Chen" <leftcopy.chx at gmail.com> wrote:
>
> Hi Dingbao,
>
> AFAIK, If you wanna make a memory location M symbolic, the only public API
> is klee_make_symbolic(FIRST_ADDR(M), SIZE(M), "specified_name").
>
> If you simply make pointer P symbolic, that's exactly the same as a normal
> variable, i.e., klee_make_symbolic(&P, sizeof(P), "p"), which means that
> P's value is uncertain.
> However if you also need to deference it(in most of the cases you do),
> you've to make the pointed area symbolic rather than P itself; also notice
> that KLEE cannot make symbolic if the length of the pointed area is
> uncertain.
>
> Thanks and Regards,
> Hongxu
>
> On Sat, Dec 20, 2014 at 9:58 AM, Dingbao Xie <xiedingbao at gmail.com> wrote:
>
>> Hi, everyone.
>> I want to test functions of a program one by one with klee.
>> It's easy to change the entry function of a program when using klee
>> to execute it.
>> But I don't know how to make the arguments of the function to be
>> symbolic and the type of an argument may be pointer, struct etc.
>>
>> What's the easiest way to achieve that?
>> Thanks in advance.
>>
>>
>>
>>
>>
>> --
>> Dingbao Xie
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
>
>


-- 
Dingbao Xie
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list