Taking your example, when you have a constraint like "if(x < 0)", setting the value of x to -2147483648 or to -1 produces the same coverage. At a high level, klee generates one input per path explored. While there may be multiple inputs that follow the same path, klee does not differentiate between them in any way (and certainly they all produce the same coverage).
As an aside, if you’re interested in a weaker type of coverage (say line or branch) you might want to omit inputs that don't contribute to it. There is the -only-output-states-covering-new option for omitting inputs that don’t improve line coverage. For something more specific you will need to make changes to the code. No, there is no option do disable the verifications that klee does. You would have to modify the code (Executor::executeMemoryOperation is a good starting point). Paul On 12 Mar 2015, at 16:01, douglas schroeder <[email protected]> wrote: > Hello > By improve I meant to use values that actually makes the program reach more > coverage, or more branches. > Another question: Is there a option to disable the verifications that Klee > does? I just need the inputs that results in > the best coverage. I don't want to actualy verify the code with Klee. Is is > possible? > Thank you. > > 2015-03-11 14:16 GMT-03:00 Dan Liew <[email protected]>: > On 11 March 2015 at 17:13, douglas schroeder <[email protected]> wrote: > > Hello, thanks for the reply. > > another question. > > in my tests, almost all generated inputs are zeros. > > > > 0: name: 'string' > > object 0: size: 8 > > object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00' > > object 1: name: 'data' > > object 1: size: 1 > > object 1: data: '\x00' > > > > is there a way to improve the generation of inputs? > > > > I don't know, but what is your definition of improve? > > Also please make sure you keep klee-dev CC'ed so that the discussion > remains public. > > > > -- > DOUGLAS SCHROEDER > FLORIANÓPOLIS-SC > _______________________________________________ > 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
