./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] function virtblk_probe uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __raw_spin_lock_init
[Info]     add_disk
[Info]     set_disk_ro
[Info]     alloc_disk
[Info]     ldv_malloc
[Info]     ldv_is_err
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     put_disk
[Info]     mempool_destroy
[Info]     blk_init_queue
[Info]     ldv_malloc
[Info]     ldv_is_err
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     blk_queue_bounce_limit
[Info]     blk_queue_max_hw_sectors
[Info]     blk_queue_max_segments
[Info]     blk_queue_max_segment_size
[Info]     blk_queue_logical_block_size
[Info]     blk_queue_physical_block_size
[Info]     blk_queue_alignment_offset
[Info]     blk_queue_io_min
[Info]     blk_queue_io_opt
[Info]     blk_queue_ordered
[Info]     __VERIFIER_nondet_int
[Info]     kfree
[Info]     sg_init_table
[Info]     PTR_ERR
[Info]     ldv_ptr_err
[Info]     IS_ERR
[Info]     ldv_is_err
[Info]     INIT_LIST_HEAD
[Info]     spinlock_check
[Info]     set_capacity
[Info]     mempool_create_kmalloc_pool
[Info]     mempool_create
[Info]     ldv_malloc
[Info]     ldv_is_err
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     queue_logical_block_size
[Info]     kmalloc
[Info]     __kmalloc
[Info]     ldv_malloc
[Info]     ldv_is_err
[Info]     __VERIFIER_nondet_int
[Info]     assume_abort_if_not
[Info]     trace_kmalloc
[Info]     ldv__builtin_expect
[Info]     lockdep_rcu_dereference
[Info]     debug_lockdep_rcu_enabled
[Info]     __VERIFIER_nondet_int
[Info]     rcu_read_lock_sched_held
[Info]     rcu_read_lock_sched_notrace
[Info]     kmalloc_slab
[Info]     kmalloc_index
[Info]     kmalloc_large
[Info]     __get_free_pages
[Info]     __VERIFIER_nondet_ulong
[Info]     get_order
[Info]     trace_kmalloc
[Info]     ldv__builtin_expect
[Info]     lockdep_rcu_dereference
[Info]     debug_lockdep_rcu_enabled
[Info]     __VERIFIER_nondet_int
[Info]     rcu_read_lock_sched_held
[Info]     rcu_read_lock_sched_notrace
[Info]     kmemleak_alloc
[Info]     virtio_has_feature
[Info]     virtio_check_driver_offered_feature
[Info]     variable_test_bit
[Info]     virtio_config_buf
[Info]     virtio_has_feature
[Info]     virtio_check_driver_offered_feature
[Info]     variable_test_bit
[Info]     virtio_find_single_vq
[Info]     ERR_PTR
[Info]     ldv_err_ptr
[Info]     index_to_minor
[Info]   "up":
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Imprecise][Unsound] Function definition missing for kmem_cache_alloc_notrace
[Info][Witness] cannot unassume entry of type violation_sequence
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4190:3-4190:45)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4190:3-4190:45)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4190:3-4190:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4237:3-4237:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3959:3-3959:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3960:3-3960:69)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3960:3-3960:69)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3611:3-3611:69)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3598:5-3598:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3601:3-3601:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3601:3-3601:90)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3096:3-3097:34)
[Warning][Unknown] lval (& vdev)->features points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3098:11-3098:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3621:4-3621:51)
[Warning][Imprecise][Call] Function pointer *((vdev->config)->get) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3621:4-3621:51)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3621:4-3621:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3962:5-3962:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3963:5-3963:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3964:5-3964:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3966:5-3966:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3967:5-3967:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3968:5-3968:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3968:5-3968:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3186:11-3186:32)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3969:5-3969:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3969:5-3969:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3969:5-3969:50)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4233:3-4233:100)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3922:3-3922:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3923:3-3923:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3926:5-3926:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3888:3-3888:49)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3889:3-3889:69)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3889:3-3889:69)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4319:11-4319:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4319:11-4319:49)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3893:13-3893:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3896:3-3896:63)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3896:3-3896:63)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4286:3-4286:70)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3901:13-3901:27)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3904:3-3904:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3905:3-3905:68)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3905:3-3905:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3205:11-3205:21)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3938:3-3938:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3938:3-3938:77)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3948:3-3948:71)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3948:3-3948:71)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4197:3-4197:53)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4198:3-4198:41)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4198:3-4198:41)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4198:3-4198:41)
[Warning][Deadcode] Function 'get_order' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3104:1-3119:1)
[Warning][Deadcode] Function 'INIT_LIST_HEAD' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3123:1-3130:1)
[Warning][Deadcode] Function 'list_add_tail' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3132:1-3138:1)
[Warning][Deadcode] Function 'list_empty' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3140:1-3145:1)
[Warning][Deadcode] Function 'spinlock_check' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3150:1-3155:1)
[Warning][Deadcode] Function 'spin_unlock_irqrestore' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3156:1-3162:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_held' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3164:1-3169:1)
[Warning][Deadcode] Function 'rcu_read_lock_sched_notrace' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3170:1-3175:1)
[Warning][Deadcode] Function 'set_capacity' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3189:1-3195:1)
[Warning][Deadcode] Function 'mempool_create_kmalloc_pool' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3214:1-3221:1)
[Warning][Deadcode] Function 'req_get_ioprio' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3225:1-3230:1)
[Warning][Deadcode] Function 'blk_rq_pos' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3240:1-3245:1)
[Warning][Deadcode] Function 'queue_logical_block_size' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3262:1-3273:1)
[Warning][Deadcode] Function 'trace_kmalloc' is uncalled: 20 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3280:1-3326:1)
[Warning][Deadcode] Function 'kmemleak_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3327:1-3333:1)
[Warning][Deadcode] Function 'kmalloc_index' is uncalled: 47 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3335:1-3432:1)
[Warning][Deadcode] Function 'kmalloc_slab' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3433:1-3446:1)
[Warning][Deadcode] Function '__kmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3464:1-3467:1)
[Warning][Deadcode] Function 'kmalloc_large' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3469:1-3485:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3487:1-3519:1)
[Warning][Deadcode] Function 'sg_assign_page' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3520:1-3555:1)
[Warning][Deadcode] Function 'sg_set_page' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3556:1-3565:1)
[Warning][Deadcode] Function 'sg_set_buf' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3566:1-3574:1)
[Warning][Deadcode] Function 'virtqueue_add_buf' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3578:1-3587:1)
[Warning][Deadcode] Function 'virtio_find_single_vq' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3625:1-3647:1)
[Warning][Deadcode] Function 'blk_done' is uncalled: 29 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3650:1-3701:1)
[Warning][Deadcode] Function 'do_req' is uncalled: 69 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3702:1-3819:1)
[Warning][Deadcode] Function 'do_virtblk_request' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3820:1-3868:1)
[Warning][Deadcode] Function 'virtblk_prepare_flush' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3869:1-3876:1)
[Warning][Deadcode] Function 'index_to_minor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3976:1-3981:1)
[Warning][Deadcode] Function 'virtblk_probe' is uncalled: 96 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3982:1-4146:1)
[Warning][Deadcode] Function 'virtblk_remove' is uncalled: 14 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4147:1-4172:1)
[Warning][Deadcode] Function 'ERR_PTR' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4256:1-4263:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4298:1-4303:1)
[Warning][Deadcode] Function 'ldv_err_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4310:1-4315:1)
[Warning][Deadcode] Function 'ldv_is_err_or_null' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4322:1-4339:1)
[Warning][Deadcode] Function 'IS_ERR___0' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4340:1-4347:1)
[Warning][Deadcode] Function 'ldv_put_blk_rq' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4371:1-4381:1)
[Warning][Deadcode] Function '__blk_end_request_all' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4392:1-4394:1)
[Warning][Deadcode] Function '__get_free_pages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4396:1-4398:1)
[Warning][Deadcode] Function '__list_add' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4399:1-4401:1)
[Warning][Deadcode] Function '__phys_addr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4403:1-4405:1)
[Warning][Deadcode] Function '__raw_spin_lock_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4406:1-4408:1)
[Warning][Deadcode] Function '_raw_spin_lock_irqsave' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4414:1-4416:1)
[Warning][Deadcode] Function '_raw_spin_unlock_irqrestore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4417:1-4419:1)
[Warning][Deadcode] Function 'add_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4420:1-4422:1)
[Warning][Deadcode] Function 'alloc_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4423:1-4425:1)
[Warning][Deadcode] Function 'blk_cleanup_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4432:1-4434:1)
[Warning][Deadcode] Function 'blk_init_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4439:1-4441:1)
[Warning][Deadcode] Function 'blk_peek_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4445:1-4447:1)
[Warning][Deadcode] Function 'blk_queue_alignment_offset' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4448:1-4450:1)
[Warning][Deadcode] Function 'blk_queue_bounce_limit' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4451:1-4453:1)
[Warning][Deadcode] Function 'blk_queue_io_min' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4454:1-4456:1)
[Warning][Deadcode] Function 'blk_queue_io_opt' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4457:1-4459:1)
[Warning][Deadcode] Function 'blk_queue_logical_block_size' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4460:1-4462:1)
[Warning][Deadcode] Function 'blk_queue_max_hw_sectors' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4463:1-4465:1)
[Warning][Deadcode] Function 'blk_queue_max_segment_size' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4466:1-4468:1)
[Warning][Deadcode] Function 'blk_queue_max_segments' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4469:1-4471:1)
[Warning][Deadcode] Function 'blk_queue_ordered' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4473:1-4475:1)
[Warning][Deadcode] Function 'blk_queue_physical_block_size' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4476:1-4478:1)
[Warning][Deadcode] Function 'blk_rq_map_sg' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4480:1-4482:1)
[Warning][Deadcode] Function 'blk_start_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4483:1-4485:1)
[Warning][Deadcode] Function 'blk_start_request' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4486:1-4488:1)
[Warning][Deadcode] Function 'blk_stop_queue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4489:1-4491:1)
[Warning][Deadcode] Function 'debug_lockdep_rcu_enabled' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4493:1-4495:1)
[Warning][Deadcode] Function 'del_gendisk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4496:1-4498:1)
[Warning][Deadcode] Function 'list_del' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4505:1-4507:1)
[Warning][Deadcode] Function 'lockdep_rcu_dereference' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4508:1-4510:1)
[Warning][Deadcode] Function 'mempool_alloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4511:1-4513:1)
[Warning][Deadcode] Function 'mempool_create' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4514:1-4516:1)
[Warning][Deadcode] Function 'mempool_destroy' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4517:1-4519:1)
[Warning][Deadcode] Function 'mempool_free' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4520:1-4522:1)
[Warning][Deadcode] Function 'put_disk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4526:1-4528:1)
[Warning][Deadcode] Function 'set_disk_ro' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4541:1-4543:1)
[Warning][Deadcode] Function 'sg_init_table' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4544:1-4546:1)
[Warning][Deadcode] Function 'virtqueue_add_buf_gfp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4557:1-4559:1)
[Warning][Deadcode] Function 'virtqueue_get_buf' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4560:1-4562:1)
[Warning][Deadcode] Function 'virtqueue_kick' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4563:1-4565:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4567:1-4569:1)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 4297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4297-4297)
[Warning][Deadcode] Function 'ldv_get_blk_rq' has dead code:
  on lines 4360..4362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4360-4362)
  on line 4364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4364-4364)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 166
  dead: 453 (448 in uncalled functions)
  total lines: 619
[Warning][Deadcode][CWE-571] condition 'fbit <= 27U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:3597:7-3597:18)
[Warning][Deadcode][CWE-570] condition 'mask == 16U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4357:8-4357:51)
[Warning][Deadcode][CWE-571] condition 'mask == 208U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:4357:8-4357:51)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.i:12:73-12:74)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
[Info][Unsound] ASM ignored
[Warning][Unsound][Call] No suitable function to call
[Error][Imprecise][Unsound] Function definition missing
