Re: [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
 *gave me a solution. However, this
solution can’t solve this problem perfectly. I make a little change to
the testcase:



#include 

#include 



unsigned long test_func(int x)

{

unsigned long ret;

if ( x == 'p' )

{

printf("addr_flag=%lx\n", (unsigned long)&_flag);

ret = (unsigned long)&_flag;

return ret;

}



ret = x;

addr_flag:

return ret;

}

int main()

{

int a;

klee_make_symbolic(, 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@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

[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 gave me 
a solution. However, this solution can't solve this problem perfectly. I make a 
little change to the testcase:

#include 
#include 

unsigned long test_func(int x)
{
unsigned long ret;
if ( x == 'p' )
{
printf("addr_flag=%lx\n", (unsigned long)&_flag);
ret = (unsigned long)&_flag;
return ret;
}

ret = x;
addr_flag:
return ret;
}
int main()
{
int a;
klee_make_symbolic(, 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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev