Hi Wei-Fan, yes, you can use the --load option to do this.

Cristian

On 10/01/2011 12:36 AM, Wei-Fan wrote:
> Hello Sir,
>
> My name is Wei-Fan Chiang.
> I am now a graduated student of U. of Utah.
> I have a question about call external function in KLEE.
>
> Suppose I have a simple program:
>
> int main (int argc,  char *argv[]) {
>       int i = 2, j = 3, k;
>       k = foo(2, 3);
>       return 0;
> }
>
> "foo" is an external function made by us.
> However, we can guarantee that in all our test cases, the arguments of
> foo will ALWAYS be concrete! Therefore, ideally, we just need to
> natively execute foo and pass the result back to KLEE (in our example,
> we need the result for 'k').
>
> Is it possible?
>
> Thanks.
>
> Regards,
> Wei-Fan
> _______________________________________________
> 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

Reply via email to