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
