[klee-dev] klee can't handle when the constant is a statement label, how to solve this problem?

[Cristian Cadar]

Hi, this is due to KLEE lacking support for the indirectbr instruction 
and blockaddress constants.  I added them to 
https://github.com/klee/klee/issues/678, which keeps track of unhandled 
parts of the LLVM language.

Best,
Cristian

On 11/05/17 04:13, Xuzhijian wrote:
> Hi,all,I’m sorry to disturb you.
>
> I had open an issue on GitHub(https://github.com/klee/klee/issues/615),
> Klee can’t handle the constant when it is a statement label. I gave a
> test example before and thanks *andreamattavelli
> <https://github.com/andreamattavelli> *gave me a solution. However, this
> solution can’t solve this problem perfectly. I make a little change to
> the testcase:
>
>
>
> #include <klee/klee.h>
>
> #include <stdio.h>
>
>
>
> unsigned long test_func(int x)
>
> {
>
>     unsigned long ret;
>
>     if ( x == 'p' )
>
>     {
>
>         printf("addr_flag=%lx\n", (unsigned long)&&addr_flag);
>
>         ret = (unsigned long)&&addr_flag;
>
>         return ret;
>
>     }
>
>
>
>     ret = x;
>
> addr_flag:
>
>     return ret;
>
> }
>
> int main()
>
> {
>
>     int a;
>
>     klee_make_symbolic(&a, sizeof(a), "a");
>
>     return !!test_func(a);
>
> }
>
>
>
> Klee gives the same error again.
>
>
>
> # klee -optimize test.bc
>
> KLEE: output directory is "/home/odysseus/tmp/klee-out-2"
>
> Using STP solver backend
>
> KLEE: WARNING: undefined reference to function: printf
>
> LLVM ERROR: invalid argument to evalConstant()
>
>
>
> How to solve this problem? Hope for your help! Thank you very much.
>
>
>
> Zhijian Xu
>
> 5/11/2017
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>