You need to pass -allow-seed-extension (or -allow-seed-truncation) when the seed is shorter (or longer) than the symbolic file
On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro <barbaro.albe...@gmail.com> wrote: > Hi Andrew and Sang, > Thanks a lot for your explanation. I tried and I think we are getting > there. > > @Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc > -only-seed A -sym-files 1 10. Now klee is complaining about the different > file size. When I generated the file.bout of course the file was just 1 > byte, now I would like to use a symbolic file. Can you suggest me how to > solve my problem please? > > @Sang: I'll have a look and try to use it and get back to you. > > Once I solved this problem I'll try to create a PR so next time should be > easier for all of us. > > Thanks again > > > On Tue, Oct 16, 2018, 00:50 Sang Phan <phanquocs...@gmail.com> wrote: > >> Hi Alberto, >> >> What you described is called concolic execution ( >> https://en.wikipedia.org/wiki/Concolic_testing) >> So the easiest way is to use an existing concolic execution engine, and >> you will have what you want out-of-the-box. >> >> KLEE had a concolic execution engine, called ZESTI, but it is no longer >> supported. You may want to try Crete, it is based on KLEE, but maintained >> by a different group. >> https://github.com/SVL-PSU/crete-dev >> I have not checked it. >> >> KLEE can be run with (concrete) seeds, and when there is only one seed, >> it is somewhat similar to concolic execution. But you need to: >> + tell KLEE that you only want to run seed (-only-seed) and you only want >> to replay seeds (-only-replay-seeds), and >> + re-start KLEE for each run of each seed. >> >> Cheers, >> Sang >> >> On Sun, Oct 14, 2018 at 5:25 AM Alberto Barbaro < >> barbaro.albe...@gmail.com> 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 >>> klee-dev@imperial.ac.uk >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>> >>
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
