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

2017-05-11 Thread 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

[klee-dev] ?????? One phenomenon after the execution using klee

2017-05-11 Thread ????
Thanks a lot! -- -- ??: "Dan Liew"; : 2017??5??11??(??) 7:53 ??: ""; : "klee-dev"; : Re: [klee-dev] One phenomenon after the execution using klee

Re: [klee-dev] One phenomenon after the execution using klee

2017-05-11 Thread Dan Liew
Hi, On 10 May 2017 at 03:55, 曾杰 wrote: > Hi, all, > If you write test.c with an error out of bound and test2.c with an > error assertion failed. > You first symbolically execution test.bc(using clang to generate), and > then the test2.c. you will find the contents