[klee-dev] a question about external function and klee_assert API?

[Yi Zhou]

 Hi everyone:
             Now I want to use klee to test a programm.But I can not deal
with some external functions.For example,I have a file main.c:
           #include<stdio.h>
           #include<klee/klee.h>
           int main(){
                   int test();
                   int my=test(8,9);
                   printf("---%d\n",my);
                   klee_assert(my<17);
                   return 0;
          }
and a file test.c :
         #include<stdio.h>
         int test(int a,int b){
                  printf("%d\n",a+b);
                  return a+b;
        }
Then I use llvm-gcc -I ../../include -emit-llvm -c -g main.c to get a
object file--main.o.
But  klee  will  report "failed external call" when  klee just test the
main.o.So how can I make the two object files to be linked and the klee can
deal with the external function?Or I need to make the two c files to be one
c file manually？But the programm have many files ,I do not think it is a
good ideal to deal with the files manually.

Thank you very much~~

Yi Zhou
Institute Of Software
Chinese Academy of Sciences
-------------- next part --------------
HTML attachment scrubbed and removed