[klee-dev] Limiting/Guiding KLEE exploration

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>