Hi Alberto, Thank you for describing your problem. I had submitted this PR some while ago: https://github.com/klee/klee/pull/956 Basically I would use gen-bout implemented in the PR to create a ktest file using concrete inputs, then use the ktest file as a seed. In this way, all inputs will be symbolic, yet the path is the one that would have been executed using the concrete inputs. Best, Andrew On Sun, Oct 14, 2018 at 8:25 PM, Alberto Barbaro<[email protected]> wrote: Hi all,I have already asked this in the past and received few suggestions but I was not able to do it. I'm trying to test pngpixel[1] that takes as input an image file. My goal is to execute pngpixel with a real file and subsequently execute pngpixel with a symbolic file and follow the path followed by the first execution.I would like to describe my approach so before spending to much time on it and I can understand if I'm doing it right or not :) 1 - Execute pngpixel enabling -debug-print-instructions=src:file2 - Inside my searcher create a map from instruction.txt so I know which is the next instruction3 - Inside the update() function for my searcher, get the current instruction, get the next instruction,4 - Check for each state in addedStates if the next instruction would be execute at the next step in the state5 - If yes add the state using state.push_back(state) else remove the state ( adding the state to removedStates? ) I'm sure this flow is not optimized but at least is it correct? How would you approach this problem? Thanks for your timeAlberto [1] https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c _______________________________________________ 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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
