Hi Breno,
You can mix concrete and symbolic arguments (e.g., klee prog.bc -E
--sym-args 0 1 4), so part of what you want to achieve is easy. You can
constrain individual bytes with klee_assume() or similar constructs, but
there is no command-line functionality for this.
Best,
Cristian
On 25/11/14 23:18, Breno Miranda wrote:
Dear All,
I'm performing some tests on *grep* using KLEE and I have one question
regarding test case generation.
I'm aware of the arguments *grep* accepts (for example, let's assume
that this string contains all the command-line arguments accepted on a
given version of grep: *A:B:CEFGHVX:bce:f:hiLlnqsvwxyUu*) and If I run
KLEE via command line (for example: klee --libc=uclibc --posix-runtime
--only-output-states-covering-new ./grep.bc -sym-args 0 2 2) it will
generate test cases to the majority of(if not to all) the accepted
parameters (this is expected because KLEE will do the best to achieve
"full" path coverage).
However, let's assume that I'm interested in a *specific use case* of
grep. I want, for example, to explore extended regular expressions
(*-E*) and some tweaks on the output are allowed, which means that
I'm interested only in a subset of the accepted parameters (e.g.:
*EHce:f:hiLlnqsvwx*).
*Is there a way I can direct/guide KLEE exploration, and consequently,
test case generation to focus on the parameters I'm interested in via
command-line?* I believe that the answer is *no* but, because KLEE has
so many options available, I would like to hear from the experts in this
list.
I'm aware that *klee_assume* can be used to "limit"/guide KLEE and it
could be applied in the scenario above, but I am curious about what my
options would be using command-line.
I look forward to hearing from you.
--
Yours sincerely,
Breno Miranda
_______________________________________________
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
