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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
