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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
