[klee-dev] Limiting/Guiding KLEE exploration

[Breno Miranda]

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
-------------- next part --------------
HTML attachment scrubbed and removed