UTBotCpp
UTBotCpp copied to clipboard
Pass pointer value to function
Description Now UTBot create variable on stack and make this memory symbolic. But in this case, it doesn't generate tests that pass nullptr.
For function
int longptr_cmp(long *a, long *b) {
return (*a == *b);
}
KLEE file
int klee_entry__lib_pointers_pointer_parameters_longptr_cmp__wrapped(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
long a;
klee_make_symbolic(&a, sizeof(a), "a");
klee_prefer_cex(&a, a >= -10 & a <= 10);
////////////////////////////////////////////
long b;
klee_make_symbolic(&b, sizeof(b), "b");
klee_prefer_cex(&b, b >= -10 & b <= 10);
////////////////////////////////////////////
long a_post;
klee_make_symbolic(&a_post, sizeof(a_post), "a_post");
long b_post;
klee_make_symbolic(&b_post, sizeof(b_post), "b_post");
int utbot_result;
klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
int utbot_tmp = longptr_cmp(&a, &b);
klee_assume(utbot_tmp == utbot_result);
klee_assume(a == a_post);
klee_assume(b == b_post);
return 0;
}
For solve this problem UTBot should generate symbolic pointer in KLEE and pass it to function.
KLEE file
int klee_entry__lib_pointers_pointer_parameters_longptr_cmp__wrapped(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
long* a;
klee_make_symbolic(&a, sizeof(a), "a");
long* b;
klee_make_symbolic(&b, sizeof(b), "b");
int utbot_result;
klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
int utbot_tmp = longptr_cmp(&a, &b);
klee_assume(utbot_tmp == utbot_result);
return 0;
}
In first implementation some problem can be ignored like
- Array
- Post value
- Parameter is reference to
utbotInnerVar