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

Thanks Dan and Christian! Adding klee_assume is a no-go because that would require either manual inspection/modification of the source code or heavy duty program analysis. I'm evaluating a change to executeMemoryOperation that appears to implement the behavior I need (succinctly drive

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