[klee-dev] Klee See Mode Concretization

[Cadar, Cristian]

Hi, take a look at https://srg.doc.ic.ac.uk/projects/zesti/.  It's based 
on a very old version of KLEE, but the code might still be helpful.

Cristian

On 12/12/2018 08:55, Ridwan Shariffdeen wrote:
> Hi,
> 
> I am running Klee in seed mode using a generated ktest file, in order to 
> capture the symbolic expression for the path given by the ktest file. 
> However in trying to execute klee, when it comes to external calls it 
> needs to pass concretized values instead of the symbolic value. From my 
> understanding, currently, Klee tries to compute a concrete value for the 
> symbolic variable from the path constraints and pass to the external 
> function.
> 
> Since I am using seed mode with pre-defined values, I need to change the 
> way Klee concretize the symbolic value by using the current value given 
> in the ktest file, instead of resolving through path constraints. But, I 
> have no idea how to achieve this.
> 
> Is there a reference I can look into or is this achievable?
> Any help in this regard would be much appreciated.
> 
> Thanks
> Regards
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>