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

[Xuzhijian]

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
-------------- next part --------------
HTML attachment scrubbed and removed