[klee-dev] How to get （or capture ） the value of replaying a test case and the usage of KLEE
Chengyu Zhang
dale.chengyu.zhang at gmail.com
Fri Nov 25 05:49:28 GMT 2016
Hi Lei,
Here is my advice:
1. KLEE has support for C and limited support for C++. If you want to
test C++ program, you could take a look at KLOVER project.
you can find more information in the paper of KLOVER :
http://www.cs.utah.edu/~ligd/publications/KLOVER-CAV11.pdf
2. You could make a little script to solve the problem. I need the full
text of your replayingtestcaseesstorageinputoutput.sh script to find what's
wrong with the script.
But I think the command like : "KTEST_FILE=klee-last/test000001.ktest
./a.out >> a.txt" in your email is not reasonable, you may need the
return code of your tested program, you should redirect the result of "echo
$?" to a.txt rather than "KTEST_FILE=klee-last/test000001.ktest ./a.out".
3. You could use klee-reply tool. "To use the klee-replay tool, we
just tell it the executable to run and the .ktest file to use"
there is a example of how to use klee-reply on
http://klee.github.io/tutorials/testing-coreutils/
4. You should read the tutorial of how to test coreutils, then you
could find the way to deal with multiple arguments.
Here is the link: http://klee.github.io/tutorials/testing-coreutils/,
the answer is in Step4.
Cheers,
Chengyu
2016-11-24 11:26 GMT+08:00 乔磊 <qiaoleioffice at 163.com>:
> 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 e
> xecuting 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？
>
> int main() {
> int a;
> klee_make_symbolic(&a, sizeof(a), "a");
> return get_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
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
--
张枨宇 Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.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/20161125/1950c9aa/attachment.png>
More information about the klee-dev
mailing list