Re: [klee-dev] Choosing the concrete values and getting the symbolic constraints

Hi, there is some documentation for ZESTI at https://srg.doc.ic.ac.uk/projects/zesti/. Unfortunately, the project is not maintained anymore. Best, Cristian On 14/12/2016 12:46, Papapanagiotakis-Bousy, Iason wrote: Hi Thuan, Thank you for pointing me to those two tools. Are you aware if

Re: [klee-dev] How to limit unrolling loops times

Hi Chengyu, KLEE is not aware of loops per se, so there's no easy way to achieve what you want. You might want to look instead at the search heuristics that KLEE provides, to see if they are good enough for your purposes. Best, Cristian On 04/01/2017 11:50, Chengyu Zhang wrote: Hi all,

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

Hi Sean, the .path files are recording the branches followed by the paths explored by KLEE -- one could also replay them later on if needed. But this feature needs more work to be usable, and we've started fixing it a few months ago, but haven't finished it yet. The other feature was added

Re: [klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array

Hi Richard, If adding klee_assume's is an option, that's indeed the easiest thing to do, as Dan suggests. You can also reduce the number of object resolutions as described by Dan, but you risk missing the case where the pointer is resolved to the buffer you're indexing. One possible

Re: [klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array

Hi Richard, On 10 January 2017 at 00:19, Richard Rutledge wrote: > Consider the following program: > > //- > #include > #include > > #define BUFFER_SIZE 16 > > int main(int argc, char *argv[]) { > > char