[klee-dev] Using Klee with Dynamic Libraries

[yukai zhao]

hi，
I am curious about the boundary situation of Klee. Will it constrain the generation of functions in the file specified by the parameter "-- link llvm lib"? Of course, this file is also a. bc file, in fact it is a dynamic library generated by the project. My executable file is dynamically linked to this library, and it will call some functions in this library.
I think the ideal scenario would be because this library is also from the project to be tested, but in a simple example, I found that it is not the case.
As shown below, I designed a main function: 


#include <stdio.h>
#include "math_operations.h"
#include <klee.h>
int main() {
    int a, b;
    klee_make_symbolic(&a, sizeof(a), "a");
    klee_make_symbolic(&b, sizeof(b), "b");
    printf("Max: %d\n", max(a, b));
    printf("Min: %d\n", min(a, b));
    return 0;
}


In this example, the max() and min() functions are both located in the library libmath_operations.so. However, KLEE only generated one test case in my testing scenario.
This is my execution statement:


 klee --link-llvm-lib=/home/directly_in/build/libmath_operations.so.bc  -libc=uclibc main.bc


Thank you for your time and help. I look forward to receiving your letter.
I'm not sure if I'm not using Klee correctly. If so, are there any recommended methods that can help me.
Thank you for your time and assistance. I look forward to your insights.


Best regards,
yukai zhao
-------------- next part --------------
HTML attachment scrubbed and removed