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