[klee-dev] OSDI2008 experiment

[Cristian Cadar]

Hi Zhiyi,

On 31/07/2014 10:31, Zhiyi Zhang wrote:
> Hi all,
>
> In the section3.2 of your OSDI2008's paper, there is a experiment about
> independence and cex.cache optimizations. You run klee for 5 minutes
> with both optimization turned off and then run same number
> *instructions(not query) *with independence and cex,cache separately.
>
> However, I am confused about the meaning of query. I have two questions.
>
> First, I used the command
> in http://klee.github.io/klee/TestingCoreutils.html, and result contains
> the number of *instruction.* But*how can I get the execution number of
> the queries*?
Look at http://klee.github.io/klee/klee-tools.html#klee-stats

> I didn't find the related options in klee‘s help.  And
> *what is the different between the instruction and the query*?
The latter refers to constraint solver queries.

> Second, In the experiment of  OSDI2008's paper, you run klee for 5
> minutes. If one program was small and executed less than 5 minutes, such
> as echo,*how to deal with the remaining time*?　Do nothing, run this
> program again until 5 minutes or run other program until 5 minutes?
We ignored those utilities for which KLEE takes less than 5 minutes to 
execute.

Best,
Cristian

>
>
> Thank you very much.
> Zhiyi Zhang
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>