Re: [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 
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 <
> phanquocs...@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@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Concolic execution with Klee

[Andrew Santosa]

 Hi Sang,
I don't think that is possible in KLEE since firstly, given concrete inputsit 
will likely simplify the constraints into a constant (true/false). Secondly,it 
does not collect the constraints into the path condition whenever it candecide 
that a branch can only go one way, which is to always happen givenconcrete 
inputs.
Best,
Andrew

   On Friday, 11 May 2018, 4:52:50 am GMT+8, Sang Phan  
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  ___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev