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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to