Thanks I'll try that one later :) On Tue, Oct 16, 2018, 14:08 Sang Phan <[email protected]> wrote:
> 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 < > [email protected]> 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 <[email protected]> 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 < >>> [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
