./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/ddv_machzwd_pthread_mutex_unlock.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/ddv_machzwd_pthread_mutex_unlock.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.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
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-free) ) -> enabling soundness analyses "base, useAfterFree"[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-deref) ) -> enabling soundness analyses "base, memOutOfBounds"[0;0;00m
[0;34m[Info] Setting "ana.arrayoob" to true[0;0;00m
[0;34m[Info] Setting "cil.addNestedScopeAttr" to true[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-memtrack) ) -> enabling soundness analyses "memLeak"[0;0;00m
[0;34m[Info] Setting "ana.malloc.unique_address_count" to 5[0;0;00m
/usr/include/pthread.h:202: Warning: Incompatible declaration for pthread_create (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:604 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:219: Warning: Incompatible declaration for pthread_join (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:615 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:269: Warning: Incompatible declaration for pthread_detach (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:616 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:273: Warning: Incompatible declaration for pthread_self (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:612 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:276: Warning: Incompatible declaration for pthread_equal (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:613 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:285: Warning: Incompatible declaration for pthread_attr_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:617 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:288: Warning: Incompatible declaration for pthread_attr_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:618 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:292: Warning: Incompatible declaration for pthread_attr_getdetachstate (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:620 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:297: Warning: Incompatible declaration for pthread_attr_setdetachstate (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:619 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:303: Warning: Incompatible declaration for pthread_attr_getguardsize (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:630 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:308: Warning: Incompatible declaration for pthread_attr_setguardsize (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:629 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:314: Warning: Incompatible declaration for pthread_attr_getschedparam (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:622 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:319: Warning: Incompatible declaration for pthread_attr_setschedparam (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:621 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:324: Warning: Incompatible declaration for pthread_attr_getschedpolicy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:624 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:329: Warning: Incompatible declaration for pthread_attr_setschedpolicy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:623 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:333: Warning: Incompatible declaration for pthread_attr_getinheritsched (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:626 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:338: Warning: Incompatible declaration for pthread_attr_setinheritsched (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:625 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:344: Warning: Incompatible declaration for pthread_attr_getscope (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:628 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:349: Warning: Incompatible declaration for pthread_attr_setscope (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:627 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:353: Warning: Incompatible declaration for pthread_attr_getstackaddr (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:632 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:361: Warning: Incompatible declaration for pthread_attr_setstackaddr (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:631 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:366: Warning: Incompatible declaration for pthread_attr_getstacksize (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:638 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:373: Warning: Incompatible declaration for pthread_attr_setstacksize (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:637 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:379: Warning: Incompatible declaration for pthread_attr_getstack (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:634 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:387: Warning: Incompatible declaration for pthread_attr_setstack (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:633 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:441: Warning: Incompatible declaration for pthread_setschedparam (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:642 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:446: Warning: Incompatible declaration for pthread_getschedparam (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:645 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:528: Warning: Incompatible declaration for pthread_cancel (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:707 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_t and pthread_t are isomorphic (different type constructors: struct __pthread_t_struct  vs. unsigned long ) 
/usr/include/pthread.h:781: Warning: Incompatible declaration for pthread_mutex_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:653 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:786: Warning: Incompatible declaration for pthread_mutex_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:661 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:790: Warning: Incompatible declaration for pthread_mutex_trylock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:665 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:794: Warning: Incompatible declaration for pthread_mutex_lock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:670 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:835: Warning: Incompatible declaration for pthread_mutex_unlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:680 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1230: Warning: Incompatible declaration for pthread_spin_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:688 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_spinlock_t and pthread_spinlock_t are isomorphic (different type qualifiers  and  volatile  ) 
/usr/include/pthread.h:1234: Warning: Incompatible declaration for pthread_spin_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:689 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_spinlock_t and pthread_spinlock_t are isomorphic (different type qualifiers  and  volatile  ) 
/usr/include/pthread.h:1238: Warning: Incompatible declaration for pthread_spin_lock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:690 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_spinlock_t and pthread_spinlock_t are isomorphic (different type qualifiers  and  volatile  ) 
/usr/include/pthread.h:1242: Warning: Incompatible declaration for pthread_spin_trylock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:691 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_spinlock_t and pthread_spinlock_t are isomorphic (different type qualifiers  and  volatile  ) 
/usr/include/pthread.h:1246: Warning: Incompatible declaration for pthread_spin_unlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:692 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_spinlock_t and pthread_spinlock_t are isomorphic (different type qualifiers  and  volatile  ) 
/usr/include/pthread.h:1254: Warning: Incompatible declaration for pthread_barrier_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:693 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrier_t and pthread_barrier_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1260: Warning: Incompatible declaration for pthread_barrier_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:696 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrier_t and pthread_barrier_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1264: Warning: Incompatible declaration for pthread_barrier_wait (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:703 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrier_t and pthread_barrier_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1269: Warning: Incompatible declaration for pthread_barrierattr_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:697 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrierattr_t and pthread_barrierattr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1273: Warning: Incompatible declaration for pthread_barrierattr_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:698 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrierattr_t and pthread_barrierattr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1277: Warning: Incompatible declaration for pthread_barrierattr_getpshared (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:699 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrierattr_t and pthread_barrierattr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:1283: Warning: Incompatible declaration for pthread_barrierattr_setpshared (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:702 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i (0)) 
	Failed assumption that pthread_barrierattr_t and pthread_barrierattr_t are isomorphic (different struct/union types) 
/usr/include/pthread.h:781: Warning: The name pthread_mutex_init is used for two distinct globals
/usr/include/pthread.h:786: Warning: The name pthread_mutex_destroy is used for two distinct globals
/usr/include/pthread.h:794: Warning: The name pthread_mutex_lock is used for two distinct globals
/usr/include/pthread.h:835: Warning: The name pthread_mutex_unlock is used for two distinct globals
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1644:4-1652:4 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:5-2672:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2674:5-2677:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2684:5-2721:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3132:5-3136:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3211:5-3212:29 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3219:5-3222:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3225:5-3226:29 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3333:3-3337:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3876:5-3882:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4121:5-4129:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4342:5-4352:5 with factor 12
[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] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
[Error][Imprecise][Unsound] Function definition missing for __VERIFIER_nondet_sector_t
[Info][Witness] couldn't parse entry: find uuid
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4153:5-4153:19)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4154:5-4154:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 7 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4154:5-4154:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 23 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3502:5-3502:35)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 23 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3849:5-3849:17)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 23 (in bytes). It is offset by 160 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3850:5-3850:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 31 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4246:2-4246:25)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 31 (in bytes). It is offset by 208 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4247:2-4247:23)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:1878(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:10:14-10:21)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:10:14-10:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3035:5-3035:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3117:7-3117:46)
[Warning][Unknown] Size of lval dereference expression timer_registered[i].timer is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3117:7-3117:46)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer timer_registered[i].timer is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3117:7-3117:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3118:6-3118:77)
[Warning][Unknown] Size of lval dereference expression timer_registered[i].timer is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3118:6-3118:77)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer timer_registered[i].timer is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3118:6-3118:77)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4177:5-4177:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 7 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4177:5-4177:21)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1610:3-1610:27)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1614:3-1614:27)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4220:5-4220:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 7 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4220:5-4220:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 31 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4260:5-4260:28)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2769:10-2769:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2769:10-2769:53)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2769:10-2769:53)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2769:10-2769:53)
[Info][Imprecise] Invalidating expressions: & loff_t_value (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2770:3-2770:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2773:4-2775:19)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2773:4-2775:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2779:10-2779:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2779:10-2779:51)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2779:10-2779:51)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2779:10-2779:51)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2793:10-2793:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2793:10-2793:52)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2793:10-2793:52)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2793:10-2793:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2797:4-2800:29)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2797:4-2800:29)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[1]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[2]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[4]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[5]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1644:8-1644:37)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (⊤) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Info][Unsound] Unknown value in {&char_value[def_exc:Unknown int([0,32]); intervals:[0,4294967295]; enums:not {} ([0,32])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1646:9-1646:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1664:9-1664:14)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 199 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2817:4-2820:27)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2817:4-2820:27)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1674:8-1674:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1679:11-1679:25)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 199 (in bytes). It is offset by 640 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2836:3-2837:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2836:3-2837:47)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4165:5-4165:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 7 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4165:5-4165:21)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4211:5-4211:21)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 7 (in bytes). It is offset by 32 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4211:5-4211:21)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1584:2-1584:26)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1707:9-1707:38)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2840:7-2840:40)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 199 (in bytes). It is offset by 768 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Unknown] Size of lval dereference expression cdev_registered[cdev_no].cdevp is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer cdev_registered[cdev_no].cdevp is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2850:3-2851:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2850:3-2851:43)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 31 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4271:5-4271:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1552:2-1552:26)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2854:7-2854:40)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:1878(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1856:11-1856:12)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1856:11-1856:12)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3:1-3:98)
[Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:12:1-12:112)
[Warning][Deadcode] Function 'jiffies_to_msecs' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:233:1-242:1)
[Warning][Deadcode] Function 'jiffies_to_usecs' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:244:1-253:1)
[Warning][Deadcode] Function 'msecs_to_jiffies' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:255:1-266:1)
[Warning][Deadcode] Function 'usecs_to_jiffies' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:268:1-279:1)
[Warning][Deadcode] Function 'INIT_LIST_HEAD' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:374:1-378:1)
[Warning][Deadcode] Function '__list_add' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:379:1-387:1)
[Warning][Deadcode] Function 'list_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:388:1-391:1)
[Warning][Deadcode] Function '__list_del' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:392:1-396:1)
[Warning][Deadcode] Function 'list_del_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:402:1-406:1)
[Warning][Deadcode] Function 'list_empty' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:412:1-415:1)
[Warning][Deadcode] Function 'pthread_mutex_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:653:1-659:1)
[Warning][Deadcode] Function 'pthread_mutex_destroy' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:661:1-663:1)
[Warning][Deadcode] Function 'pthread_mutex_lock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:670:1-678:1)
[Warning][Deadcode] Function 'pthread_mutex_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:680:1-686:1)
[Warning][Deadcode] Function 'atomic_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:752:1-755:1)
[Warning][Deadcode] Function 'atomic_sub' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:756:1-759:1)
[Warning][Deadcode] Function 'atomic_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:767:1-770:1)
[Warning][Deadcode] Function 'atomic_dec' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:778:1-781:1)
[Warning][Deadcode] Function 'atomic_dec_and_test' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:782:1-797:1)
[Warning][Deadcode] Function 'atomic_inc_and_test' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:798:1-813:1)
[Warning][Deadcode] Function 'atomic_add_negative' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:814:1-829:1)
[Warning][Deadcode] Function 'atomic_add_return' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:830:1-833:1)
[Warning][Deadcode] Function 'atomic_sub_return' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:835:1-838:1)
[Warning][Deadcode] Function 'sigfillset' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:951:1-961:1)
[Warning][Deadcode] Function 'sigaddsetmask' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:965:1-968:1)
[Warning][Deadcode] Function 'sigdelsetmask' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:970:1-973:1)
[Warning][Deadcode] Function 'sigtestsetmask' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:975:1-978:1)
[Warning][Deadcode] Function 'ERR_PTR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1157:1-1160:1)
[Warning][Deadcode] Function 'PTR_ERR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1162:1-1165:1)
[Warning][Deadcode] Function 'IS_ERR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1167:1-1170:1)
[Warning][Deadcode] Function 'iminor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1294:1-1297:1)
[Warning][Deadcode] Function 'imajor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1299:1-1302:1)
[Warning][Deadcode] Function 'zf_notify_sys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1732:1-1740:1)
[Warning][Deadcode] Function 'dev_get_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2023:1-2026:1)
[Warning][Deadcode] Function 'dev_set_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2028:1-2031:1)
[Warning][Deadcode] Function 'tasklet_disable' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2138:1-2141:1)
[Warning][Deadcode] Function 'create_request' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2915:1-2928:1)
[Warning][Deadcode] Function 'call_rq_function' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2930:1-2951:1)
[Warning][Deadcode] Function 'call_genhd_functions' is uncalled: 40 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2953:1-3029:1)
[Warning][Deadcode] Function 'create_pci_dev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3043:1-3045:1)
[Warning][Deadcode] Function 'pci_probe_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3047:1-3065:1)
[Warning][Deadcode] Function 'pci_remove_device' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3067:1-3072:1)
[Warning][Deadcode] Function 'call_pci_functions' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3074:1-3092:1)
[Warning][Deadcode] Function 'pci_enable_device' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3128:1-3137:1)
[Warning][Deadcode] Function 'pci_get_class' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3139:1-3155:1)
[Warning][Deadcode] Function 'pci_register_driver' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3157:1-3168:1)
[Warning][Deadcode] Function 'pci_unregister_driver' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3170:1-3174:1)
[Warning][Deadcode] Function 'pci_release_region' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3176:1-3186:1)
[Warning][Deadcode] Function 'pci_request_region' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3188:1-3205:1)
[Warning][Deadcode] Function 'pci_release_regions' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3207:1-3213:1)
[Warning][Deadcode] Function 'pci_request_regions' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3215:1-3229:1)
[Warning][Deadcode] Function 'copy_from_user' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3274:1-3280:1)
[Warning][Deadcode] Function 'register_blkdev' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3286:1-3295:1)
[Warning][Deadcode] Function 'unregister_blkdev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3297:1-3300:1)
[Warning][Deadcode] Function 'alloc_disk' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3302:1-3316:1)
[Warning][Deadcode] Function 'add_disk' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3318:1-3327:1)
[Warning][Deadcode] Function 'del_gendisk' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3329:1-3338:1)
[Warning][Deadcode] Function 'get_fixed_request_queue' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3352:1-3359:1)
[Warning][Deadcode] Function 'blk_init_queue' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3361:1-3377:1)
[Warning][Deadcode] Function 'blk_alloc_queue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3379:1-3394:1)
[Warning][Deadcode] Function 'blk_queue_make_request' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3396:1-3399:1)
[Warning][Deadcode] Function 'end_request' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3401:1-3406:1)
[Warning][Deadcode] Function 'blk_queue_hardsect_size' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3409:1-3412:1)
[Warning][Deadcode] Function 'blk_cleanup_queue' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3414:1-3417:1)
[Warning][Deadcode] Function 'alloc_tty_driver' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3746:1-3754:1)
[Warning][Deadcode] Function 'tty_set_operations' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3756:1-3782:1)
[Warning][Deadcode] Function 'alloc_chrdev_region' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3783:1-3795:1)
[Warning][Deadcode] Function 'register_chrdev_region' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3797:1-3803:1)
[Warning][Deadcode] Function 'register_chrdev' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3807:1-3828:1)
[Warning][Deadcode] Function 'unregister_chrdev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3830:1-3833:1)
[Warning][Deadcode] Function 'cdev_alloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3835:1-3840:1)
[Warning][Deadcode] Function 'cdev_init' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3842:1-3845:1)
[Warning][Deadcode] Function 'cdev_del' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3872:1-3883:1)
[Warning][Deadcode] Function 'mutex_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3887:1-3895:1)
[Warning][Deadcode] Function 'mutex_lock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3897:1-3908:1)
[Warning][Deadcode] Function 'mutex_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3910:1-3918:1)
[Warning][Deadcode] Function 'inb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3952:1-3955:1)
[Warning][Deadcode] Function 'inl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3970:1-3973:1)
[Warning][Deadcode] Function 'outl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3975:1-3977:1)
[Warning][Deadcode] Function 'schedule' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4012:1-4015:1)
[Warning][Deadcode] Function 'schedule_timeout' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4017:1-4022:1)
[Warning][Deadcode] Function 'sema_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4028:1-4032:1)
[Warning][Deadcode] Function 'init_MUTEX' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4034:1-4038:1)
[Warning][Deadcode] Function 'init_MUTEX_LOCKED' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4040:1-4044:1)
[Warning][Deadcode] Function 'down' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4046:1-4057:1)
[Warning][Deadcode] Function 'down_interruptible' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4059:1-4076:1)
[Warning][Deadcode] Function 'down_trylock' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4078:1-4098:1)
[Warning][Deadcode] Function 'up' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4100:1-4108:1)
[Warning][Deadcode] Function 'tasklet_schedule' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4112:1-4137:1)
[Warning][Deadcode] Function 'tasklet_init' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4139:1-4147:1)
[Warning][Deadcode] Function 'add_timer_on' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4263:1-4267:1)
[Warning][Deadcode] Function 'mod_timer' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4274:1-4282:1)
[Warning][Deadcode] Function 'init_waitqueue_head' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4285:1-4288:1)
[Warning][Deadcode] Function 'wake_up' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4290:1-4296:1)
[Warning][Deadcode] Function 'schedule_work' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4333:1-4356:1)
[Warning][Deadcode] Function 'request_irq' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4371:1-4382:1)
[Warning][Deadcode] Function 'free_irq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4384:1-4388:1)
[Warning][Deadcode] Function '__get_free_pages' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4393:1-4399:1)
[Warning][Deadcode] Function '__get_free_page' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4401:1-4407:1)
[Warning][Deadcode] Function 'alloc_pages_node' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4417:1-4424:1)
[Warning][Deadcode] Function 'alloc_pages' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4426:1-4432:1)
[Warning][Deadcode] Function 'alloc_page' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4434:1-4440:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4446:1-4453:1)
[Warning][Deadcode] Function 'kzalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4455:1-4462:1)
[Warning][Deadcode] Function 'vmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4474:1-4477:1)
[Warning][Deadcode] Function '__module_get' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4503:1-4503:44)
[Warning][Deadcode] Function 'release_mem_region' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4524:1-4524:67)
[Warning][Deadcode] Function 'kfree' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4525:1-4525:32)
[Warning][Deadcode] Function 'request_mem_region' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4527:1-4530:1)
[Warning][Deadcode] Function 'call_cdev_functions' has dead code:
  on lines 2780..2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2780-2781)
  on line 2783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2783-2783)
[Warning][Deadcode] Function 'call_interrupt_handler' has dead code:
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3039-3039)
[Warning][Deadcode] Function 'call_shared_workqueue_functions' has dead code:
  on lines 4364..4365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4364-4365)
[Warning][Deadcode] Function 'call_tasklet_functions' has dead code:
  on lines 3102..3105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3102-3105)
[Warning][Deadcode] Function 'cdev_add' has dead code:
  on line 3865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3865-3865)
[Warning][Deadcode] Function 'misc_register' has dead code:
  on line 3508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3508-3508)
[Warning][Deadcode] Function 'zf_init' has dead code:
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1791-1791)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1806-1806)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1808-1808)
[Warning][Deadcode] Function 'zf_open' has dead code:
  on line 1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1701-1701)
[Warning][Deadcode] Function 'zf_set_timer' has dead code:
  on line 1529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1529-1529)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 363
  dead: 462 (445 in uncalled functions)
  total lines: 825
[Warning][Deadcode][CWE-571] condition '((cdev_registered[cdev_no].cdevp)->ops)->open' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2834:11-2835:35)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'fixed_cdev_used < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3497:7-3497:26)
[Warning][Deadcode][CWE-571] condition '((cdev_registered[cdev_no].cdevp)->ops)->release' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2848:11-2849:41)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition '! result' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2853:7-2853:14)
[Warning][Deadcode][CWE-570] condition 'nowayout' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1700:6-1700:14)
[Warning][Deadcode][CWE-571] condition '! nowayout' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1634:7-1634:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'ofs != count' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1644:8-1644:37)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition '0 <= cdev_no' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2765:5-2765:75)
[Warning][Deadcode][CWE-570] condition '(unsigned long )tasklet_registered[i].tasklet != (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3100:8-3101:50)
[Warning][Deadcode][CWE-571] condition '(int )number_timer_registered < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4245:9-4245:36)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Warning][Deadcode][CWE-571] condition 'action <= 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1788:6-1788:35)
[Warning][Deadcode][CWE-571] condition 'action >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1788:6-1788:35)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1805:5-1805:47)
[Warning][Deadcode][CWE-571] condition '(int )n == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1527:3-1527:9)
[Warning][Deadcode][CWE-571] condition 'i < 1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2674:9-2674:27)
[Warning][Deadcode][CWE-570] condition 'i < 1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2674:9-2674:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )shared_workqueue[i] != (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:4363:9-4363:43)
[Warning][Deadcode][CWE-571] condition '(int )new > 0xff' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:1530:25-1530:61)
[Warning][Deadcode][CWE-571] condition '((cdev_registered[cdev_no].cdevp)->ops)->llseek' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2769:10-2769:53)
[Warning][Deadcode][CWE-570] condition '((cdev_registered[cdev_no].cdevp)->ops)->read' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2779:10-2779:51)
[Warning][Deadcode][CWE-571] condition '((cdev_registered[cdev_no].cdevp)->ops)->write' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2793:10-2793:52)
[Warning][Deadcode][CWE-571] condition '(int )number_cdev_registered < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3856:6-3856:32)
[Warning][Deadcode][CWE-571] condition '((cdev_registered[cdev_no].cdevp)->ops)->ioctl' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2813:10-2813:52)
[Warning][Deadcode][CWE-570] condition 'registered_irq[i].handler' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:3038:9-3038:34)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i:2670:9-2670:28)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
[Error][Imprecise][Unsound] Function definition missing
