[klee-dev] about klee inputs

[Paul Marinescu]

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 <douglaz88 at gmail.com> 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 <dan at su-root.co.uk>:
> On 11 March 2015 at 17:13, douglas schroeder <douglaz88 at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed