[klee-dev] Reproduce the OSDI'08 coreutils result on the latest version of KLEE

[Shiyu Dong]

Hi Cristian,

Thanks for your information. That's really helpful.

One more question: does KLEE has any way to limit to the number of paths to
explore? From the --help command the only possible option I see is
"-stop-after-n-tests=<uint>" because I assume each test case corresponds to
one path by observing the test results that I already have. Is that a good
assumption? Are there better flags to use?

Best,
Shiyu


On Tue, Sep 24, 2013 at 3:48 PM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:

> Hi Shiyu,
>
>
> On 24/09/2013 19:56, Shiyu Dong wrote:
>
>> http://klee.llvm.org/**CoreutilsExperiments.html<http://klee.llvm.org/CoreutilsExperiments.html>
>>
>> I used the command specified in question #7. However it takes forever to
>> run on my machine.
>>
> I'm not sure what you mean: as specified by the --max-time option, that
> should take approximately one hour :) (modulo some extra test generation at
> the end, and benchmarks that complete in less than one hour).  Don't you
> see the message "HaltTimer invoked" after 1h?
>
> This being said, it is unlikely that you'll obtain the same results as in
> the original paper, for reasons that are discussed on the webpage above and
> in prior messages (changes in KLEE, different LLVM and STP versions, 64 vs
> 32bit, etc.)
>
> Best,
> Cristian
>
> ______________________________**_________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
-------------- next part --------------
HTML attachment scrubbed and removed