[klee-dev] Using Klee with Dynamic Libraries

[Nowack, Martin]

Hi Yukai Zhao,

Can you provide the output of your KLEE run?

My guess is that `max`, `min` are treated as external functions that forces a and b to be concretised, i.e. which leads to only one path being generated.
But let’s have a look at your output to confirm this.

Best,
Martin

> On 12. Dec 2023, at 01:55, yukai zhao <yukzhao at 163.com> wrote:
> 
> 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev