[klee-dev] Guided Search - Help

[Alberto Barbaro]

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
-------------- next part --------------
HTML attachment scrubbed and removed