Re: [klee-dev] (Re)implementing a randomized fork

2017-01-18 Thread Sean Heelan
register in /lib/Core/UserSearcher.cpp. >If you have any question about how to implement an own Searcher, you > can ask me. > > Cheers, > Chengyu > > 2017-01-18 5:30 GMT+08:00 Sean Heelan : > >> Hi, >> >> For various reasons a randomised fork would be ben

[klee-dev] (Re)implementing a randomized fork

2017-01-17 Thread Sean Heelan
Hi, For various reasons a randomised fork would be beneficial when using batched searching. In case it isn't apparent, what I mean by a 'randomised fork' is randomly selecting whether the conditions for the true side of a branch or the false side are applied to the current state. At present the cu

[klee-dev] Interpreting the output of --write-sym-paths and --write-paths

2017-01-09 Thread Sean Heelan
Hi, I was wondering if someone could enlighten me as to how the paths.ts, symPaths.ts, test*.path and test*.sym.path files generated by --write-sym-paths and --write-paths can be used? Some googling turned up [1] but, other than that, is there an intended application for processing this data? Ch

[klee-dev] Error using klee-replay

2016-12-12 Thread Sean Heelan
Hi all, When trying to use klee-replay to replay a test case I'm getting the following errors: $ ./Documents/git/klee/Release+Asserts/bin/klee-replay ./target klee-out-0/test44.ktest ./Documents/git/klee/Release+Asserts/bin/klee-replay: TEST CASE: klee-out-0/test44.ktest ./Documents/git/k

[klee-dev] Bugs found by KLEE (or symbolic execution in general)

2016-12-05 Thread Sean Heelan
Hi all, I'm investigating the impact of some modifications to KLEE and would like to tell whether or not those modifications negatively impact KLEEs bug finding ability on real world code. Is there a list somewhere of bugs that have either been found by KLEE, or that could have been found by KLEE?