Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon024; apollon065; apollon077; apollon078] [apollon077; apollon078; apollon093] [apollon077; apollon078] [apollon073; apollon077; apollon078; apollon091; apollon099; apollon124]
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: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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-02 00:00:31 CET 2017-12-02 01:15:07 CET 2017-12-02 01:40:08 CET 2017-12-02 01:42:26 CET 2017-12-02 01:17:53 CET
Run set esbmc-incr.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0000.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/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.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 false(valid-deref) 1 wit inspect 780    1300 8200   true -32 wit inspect 3.2  260 error (7) 0 wit inspect 5.4   210   false(valid-deref) 1 wit inspect .82   28    - wit inspect
head_false-valid-deref.i unknown 0 wit inspect 5.0  210 78   error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
sleep_false-valid-deref.i unknown 0 wit inspect 5.6  230 76   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 wit inspect 4.8  190 58   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900    1100 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 57   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .037 4.9
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 69   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  210 74   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
dirname_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900    4400 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
du_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  210 78   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
echo_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 7.0  330 99   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.7  250 67   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
fold_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.6  250 75   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
hostid_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900    1600 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
logname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 57   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect .20 50 2.3 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
mkdir_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  200 77   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 56   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.0  220 56   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  200 58   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
readlink_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 74   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 63   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
rm_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  200 61   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
seq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect .13 35 1.2 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.7  250 71   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
sync_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 71   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
tac_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 63   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
tee_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 64   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.6  310 70   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  210 55   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
uname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 64   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
uniq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 74   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.2  230 65   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
uudecode_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.9  210 71   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.6  250 77   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
who_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  200 74   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 4.8  190 62   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
yes_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 5.3  210 69   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 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 1 3600 15000 42000 4 -32 4.6 390 4 0 5.4 220 4 1 .82 28 34 0 .70 170
    correct results 1 1 780 1300 8200 0 0 1 1 .82 28 0
        correct true 0 0 0 0 0
        correct false 1 1 780 1300 8200 0 0 1 1 .82 28 0
    incorrect results 0 1 -32 3.2 260 0 0 0
        incorrect true 0 1 -32 3.2 260 0 0 0
        incorrect false 0 0 0 0 0
score (38 tasks, max score: 72) 1 -32 0 1 0
Run set esbmc-incr.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety