Tool CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon077; apollon078; apollon091] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 08:22:21 CET 2017-12-01 08:49:28 CET 2017-12-01 09:05:52 CET 2017-12-01 09:09:01 CET 2017-12-01 08:49:44 CET
Run set cpa-seq.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
basename_false-valid-deref.i error 0 wit inspect 3.5 270 30 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect
head_false-valid-deref.i error 0 wit inspect 4.4 270 36 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
sleep_false-valid-deref.i error 0 wit inspect 4.2 270 37 error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0034 .27 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error 0 wit inspect 4.3 290 39 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.0 290 30 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.4 270 40 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.7 270 39 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.1 270 44 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
dirname_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 3.9 290 33 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
du_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.1 300 46 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
echo_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.3 290 39 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.9 280 39 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
fold_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.8 270 37 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
hostid_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 3.9 290 30 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
logname_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.4 290 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.6 290 45 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
mkdir_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.9 270 41 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.1 300 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 6.4 310 53 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.7 270 37 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
readlink_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.5 270 40 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
realpath_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.1 270 32 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
rm_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.1 290 47 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
seq_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.4 280 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (parsing failed) 0 wit inspect 2.5 180 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
sync_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 3.9 270 33 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
tac_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.6 270 43 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
tee_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.5 270 34 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.9 290 46 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.9 270 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
uname_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.3 290 37 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
uniq_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.6 270 42 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
usleep_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.2 270 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
uudecode_true-no-overflow_true-valid-memsafety.i error (parsing failed) 0 wit inspect 2.7 180 27 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 5.1 290 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
who_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.8 290 45 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.2 270 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
yes_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 4.4 290 32 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 38 0 170 10000 1400 4 0 2.3 170 4 0 .077 20 4 0 .010 1.1 34 0 .67 170
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (38 tasks, max score: 72) 0 0 0 0 0
Run set cpa-seq.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety