[klee-dev] question about -max-time flag

[Tomasz Kuchta]

Hi Shiyu,

I'm not sure, whether that would be helpful, but I've noticed that
dumping states takes some time.
I personally use --dump-states-on-halt=false option. Maybe that would
make your execution time closer to --max-time?

Hope that helps,

Best regards,
Tomek

On 04/10/13 15:53, Shiyu Dong wrote:
> Hello,
> 
> I have a question about how the -max-time flag should be used. I ran the
> coreutil test using the following command and set the max time to 600
> seconds. However, when I tried to print out the result using klee-stats
> the time cost is 717.57 seconds. I'm wondering where does the extra time
> come from? Is that costed by generating the test cases, or simply by
> halting the program?
> 
> Here's the command that I used:
> 
> klee \                                                                  
>                                           
> --simplify-sym-indices \                                    
> --write-cvcs \                                              
> --write-cov \                                               
> --output-module \                                           
> --max-memory=1000 \                                         
> --disable-inlining \                                        
> --use-forked-solver \                                       
> --use-cache=false \                                         
> --use-cex-cache=false \                                     
> --libc=uclibc \                                             
> --posix-runtime \                                           
> --allow-external-sym-calls \                                
> --only-output-states-covering-new \                         
> --environ=../test.env \                                     
> --run-in=/tmp/sandbox \                                     
> --max-sym-array-size=4096 \                                 
> --max-instruction-time=30. \                                
> --watchdog \                                                
> --max-time=600. \                                           
> --max-memory-inhibit=false \                                
> --max-static-fork-pct=1 \                                   
> --max-static-solve-pct=1 \                                  
> --max-static-cpfork-pct=1 \                                 
> --switch-type=internal \                                    
> --randomize-fork \                                          
> --search=random-path \                                      
> --search=nurs:covnew \                                      
> --use-batching-search \                                     
> --batch-instructions=10000" \
> base64.bc \
> --sym-args 0 1 10 \
> --sym-args 0 2 2 \
> --sym-files 1 8 \
> --sym-stdout"
> 
> Thanks,
> Shiyu
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>