Tool Forester 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* [apollon029; apollon040; apollon054; apollon077; apollon078; apollon114] 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]
Date of execution 2017-12-01 19:12:21 CET 2017-12-01 20:00:01 CET 2017-12-01 20:21:22 CET 2017-12-01 20:22:56 CET 2017-12-01 20:02:08 CET
Run set forester.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-forester.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --trace error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/forester.2017-12-01_1912.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/forester.2017-12-01_1912.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/forester.2017-12-01_1912.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/forester.2017-12-01_1912.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ 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
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .058 11 .56 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .055 11 .66 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .072 11 .46 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .14  14 2.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   290  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .055 11 .51 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .073 11 .63 timeout 0 wit inspect 92    2400 true -32 wit inspect 7.0   290   false(valid-deref) 1 wit inspect .66   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .10  15 .94 error (1) 0 wit inspect .46 48 timeout 0 wit inspect 97     960   error (1) 0 wit inspect .067  9.0  - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .40  19 5.5  timeout 0 wit inspect 91    3100 true -32 wit inspect 56     880   true -32 wit inspect .74   19    - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.6   38 21    error (1) 0 wit inspect .62 46 timeout 0 wit inspect 96     680   error (1) 0 wit inspect .066  9.2  - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .71  24 10    error (1) 0 wit inspect .67 46 timeout 0 wit inspect 96     650   error (1) 0 wit inspect .067  9.1  - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19  16 2.0  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 240     760  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .051 10 .59 error (invalid witness file) 0 wit inspect .40 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 2.6   30 850    error (invalid witness file) 0 wit inspect .63 48 error (invalid witness file) 0 wit inspect 3.3   200   error (invalid witness file) 0 wit inspect .066  9.0  - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) 0 wit inspect .080 11 .52 error (invalid witness file) 0 wit inspect .62 45 error (invalid witness file) 0 wit inspect 3.1   200   error (invalid witness file) 0 wit inspect .066  9.1  - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .052 11 .61 error (1) 0 wit inspect .61 45 unknown 0 wit inspect 23     470   error (1) 0 wit inspect .065  9.1  - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 5.5   73 930    error (invalid witness file) 0 wit inspect .43 47 error (invalid witness file) 0 wit inspect 3.2   200   error (invalid witness file) 0 wit inspect .069  9.1  - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15  18 1.3  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .14  17 1.6  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.9
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  17 1.3  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  17 1.4  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .14  17 1.6  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  17 1.4  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .14  17 1.6  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .14  17 1.5  error (invalid witness file) 0 wit inspect .41 42 error (2) 0 wit inspect .032 4.9 error (invalid witness file) 0 wit inspect .0014 .33 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  17 1.7  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  17 1.4  error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  17 1.4  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .14  17 1.5  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .13  17 1.6  error (invalid witness file) 0 wit inspect .39 42 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .54  29 6.4  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1600  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 31     120 410    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     780  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.3   42 15    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     980  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.5   30 19    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     800  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.4   37 18    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     940  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.3   37 20    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     790  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 240     710 3300    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1400  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 120     450 1700    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1000  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .12  14 1.4  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 300     1100  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .90  39 14    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1400  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 660     1600 7300    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1200  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1   47 28    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     840  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .94  35 15    - wit inspect - wit inspect - wit inspect true 2 wit inspect 860     1000  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 17     91 240    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     810  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.1   51 73    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .48  22 6.0  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     820  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3   66 55    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 190     390 2900    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1000  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .10  14 1.3  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 330     790  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .070 11 .55 timeout 0 wit inspect 91    2500 true -32 wit inspect 10     340   true -32 wit inspect .66   18    - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .071 12 .76 timeout 0 wit inspect 92    2400 true -32 wit inspect 19     580   false(valid-deref) 1 wit inspect .68   19    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .071 11 .54 timeout 0 wit inspect 92    2600 true -32 wit inspect 77     970   true -32 wit inspect .66   18    - wit inspect
sv-benchmarks/c/ 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 51 42 1300    4400 18000   24 0 470 14000 24 -160 490 6500 24 -94 3.9 160 27 4 17000 22000
    correct results 22 42 1300    3900 16000   0 0 2 2 1.3 37 2 4 870 1300
        correct true 20 40 1300    3900 16000   0 0 0 2 4 870 1300
        correct false 2 2 .14 22 1.4 0 0 2 2 1.3 37 0
    correct-unconfimed results 4 0 2.5  88 33   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 4 0 2.5  88 33   0 0 0 0
    incorrect results 0 0 5 -160 170 3100 3 -96 2.1 55 0
        incorrect true 0 0 5 -160 170 3100 3 -96 2.1 55 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 42 0 -160 -94 4
Run set forester.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-forester.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-forester.sv-comp18-correctness-witness.MemSafety-LinkedLists