[klee-dev] Concolic execution with Klee

[Sang Phan]

Thanks Andrew.

I just figured out that my question had been asked before.
https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2013-November/000489.html

I'm trying Chaoqiang's suggestion on using seed.

Best,
Sang

On Fri, May 11, 2018 at 6:33 PM, Andrew Santosa <asantosa1999 at gmail.com>
wrote:

> Hi Sang,
>
> I don't think that is possible in KLEE since firstly, given concrete inputs
> it will likely simplify the constraints into a constant (true/false).
> Secondly,
> it does not collect the constraints into the path condition whenever it can
> decide that a branch can only go one way, which is to always happen given
> concrete inputs.
>
> Best,
> Andrew
>
> On Friday, 11 May 2018, 4:52:50 am GMT+8, Sang Phan <
> phanquocsang at gmail.com> wrote:
>
>
> Hello,
>
> I'm interested in collecting the constraints for just one particular
> input, e.g. x = 3. Is it possible to do that with Klee?
>
> Thank you,
> Sang
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed