Open
Description
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
Metadata
Metadata
Assignees
Labels
Type
Projects
Status
Todo