[klee-dev] How to get （or capture ） the value of replaying a test case and the usage of KLEE

[乔磊]

Dear all,I am a new user of KLEE, I am learning some knoeledge about symbolic execution.

I saw the usage of KLEE from the website http://klee.github.io/. 


I have some questions as follows:


1. Does KLEE just only generate testcases for C program？




2. How to get （or capture  ） the value after replaying a test case and how to store the value of replaying a test case  into a file.


I saw one method from the website：http://klee.github.io/tutorials/testing-function/


$ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-last/test000001.ktest ./a.out 
$ echo$?
1
After I input and execute  the command of KTEST_FILE=klee-last/test000001.ktest ./a.out, the result of running the testcase on C program will print a value on the screen. It looks like the function of the Linux command "echo" . I just see it on the screen. I can't get （or capture ）the value after executing  the command of KTEST_FILE=klee-last/test000001.ktest ./a.out.
Is there any mistakes on my usage on KLEE.




When I use the command as follows：
    KTEST_FILE=klee-last/test000001.ktest ./a.out   >> a.txt
There is no result. How can I store the value of running the testcase on a program.






When I write the command：KTEST_FILE=klee-last/$testcase ./a.out into a bash file named replayingtestcaseesstorageinputoutput.sh


Then I execute  this bash script as follows. Some errors information will print on the screen? I don't know the reason of occuring error. Can you give
me a help?








3.How to run the test cases generated by KLEE on our c program  ?


    just one method as follows? 
$ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-last/test000001.ktest ./a.out 
$ echo$?
1
Do you have other method or other usage？




4. There are only simple example on the KLEE website http://klee.github.io/， the tutorial one and two just give two examples.  when my C program has two or three , even more than three input arguments，How to use klee ？


When I use klee. I just replace the input variable of the statement  “scanf("%d%d%d,&a，&b，&c);” to the function of klee_make_symbolic(&a,sizeof(a),"a")just like the following ; Do I need replace other variable or statement？


When the c program has no the statement of “scanf("%d%d%d,&a，&b，&c);” How to make symbolic use klee to generate the testcase？


Is the following usage right？
intmain(){inta;klee_make_symbolic(&a,sizeof(a),"a");returnget_sign(a);}
when there is one input variable ：  scanf("%d",&a);    I replaceed the Statement scanf("%d",&n)  to  klee_make_symbolic(&a,sizeof(a),"a");
when there are two input variables ： scanf("%d%d‘’,&a，&b);   I replaceed this statement  to two statements  klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b");
when there are three input variables ：  scanf("%d%d%d,&a，&b，&c);   I replaceed this statement  to three statements  klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b");  klee_make_symbolic(&c,sizeof(c),"c");
Is all right？


5.How can I get the learning materials and Instructions of using KLEE, If you have, please send to me by Email. which website or internet forum can I search some usages materials of KLEE？






Thank you very much. 


Best wishes.


 Beijing Institute of Technology
                                                                    
School of Computer Science and Technology


                                                                                              Beijing Institute of Technology : 5 South Zhongguancun Street, Haidian District, Beijing Postcode: 100081, CHINA
                                                                                                                                                                             
                                                                                                                                                               Lei  Qiao
E-mail: qiaoleioffice at 163.com




















 
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 11.png
Type: image/png
Size: 69439 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20161124/36ce855c/attachment.png>