Hi Norlina,
Yes, generally it is possible for KLEE to generate string inputs, including a
program written in a particular language.For the space program that you are
testing, I guess that you would need to provide a symbolic file as an input
program.KLEE will then replace the content of the file with concrete contents
in the generated .ktest files.
Please have a look on how to use symbolic files in this tutorial: Symbolic
Environment · KLEE
Regards,Andrew
|
|
| |
Symbolic Environment · KLEE
|
|
|
On Tuesday, 13 February 2018, 6:19:06 pm GMT+8, Norlina Pasaribu
<[email protected]> wrote:
Hello,
I am so really thankful having chance to get KLEE contact. My name is Norlina
Pasaribu from Institut Teknologi Del, Indonesia. Now, I am in my last year of
my bachelor and getting a thesis abouttesting program. If you don't mind, let
me to tell you a little about my project.
We are really proud of you for buliding a KLEE tools for testing. I have Space
program being the object for the testing. Space is C program contains 9000 line
codes and I get from http://sir.unl.edu/.
I found on some paper, that concolic testing is possible to implemented using
KLEE.
My plan is I would like to generate test-case for Space program using concolic
testing method in KLEE. Space input is not numerical but Array Defenition
Language (ADL).
My question is, is that possible KLEE for generating test-case and for
non-numerical input ?
We really hope we be able to discuss more about it with you. If you dont mind,
let us to get your respond.
Thank you very much for attention.
Best regards,
Norlina Pasaribu_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
