Hi Andrew, Thanks for your email and PR. So I tested gen-bout on a simple project called first that prints a different message depending on the first byte of file passed as a parameter. I think I did it properly because at the end I had the file.bout file. At this point I was able to use klee-replay with it and have the same stdout. Now I don't know how to use file.bout as a seed. Are you happy to show me a simple example please? I would like to able to use it in conjunction with a new searcher in order to 'execute,' queries at runtime on the code.
Thanks a lot! Alberto On Mon, Oct 15, 2018, 01:19 Andrew Santosa <[email protected]> wrote: > 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:file > 2 - Inside my searcher create a map from instruction.txt so I know which > is the next instruction > 3 - 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 state > 5 - 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 time > Alberto > > [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
