./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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:604 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:615 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:616 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:612 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:613 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:617 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:618 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:620 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:619 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:630 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:629 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:622 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:621 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:624 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:623 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:626 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:625 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:628 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:627 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:632 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:631 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:638 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:637 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:634 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:633 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:642 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:645 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:705 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:653 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:661 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:665 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:670 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:680 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:686 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:687 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:688 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:689 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:690 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:691 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:694 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:701 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:695 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:696 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:697 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:700 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:1642:4-1650:4 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2668:5-2670:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2672:5-2675:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2682:5-2719:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3130:5-3134:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3209:5-3210:29 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3217:5-3220:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3223:5-3224:29 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3331:3-3335:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3874:5-3880:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:4121:5-4129:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:3500:5-3500: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_outl_p.i:3847:5-3847: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_outl_p.i:3848:5-3848: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_outl_p.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_outl_p.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:1877(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.i:3033:5-3033:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3115:7-3115: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_outl_p.i:3115:7-3115: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_outl_p.i:3115:7-3115:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3116:6-3116: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_outl_p.i:3116:6-3116: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_outl_p.i:3116:6-3116: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_outl_p.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_outl_p.i:4177:5-4177:21)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1608:3-1608:27)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1612:3-1612: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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:2767:10-2767:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2767:10-2767: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_outl_p.i:2767:10-2767: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_outl_p.i:2767:10-2767:53)
[Info][Imprecise] Invalidating expressions: & loff_t_value (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2768:3-2768:44)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2771:4-2773:19)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2771:4-2773:19)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2777:10-2777:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2777:10-2777: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_outl_p.i:2777:10-2777: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_outl_p.i:2777:10-2777:51)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2791:10-2791:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2791:10-2791: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_outl_p.i:2791:10-2791: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_outl_p.i:2791:10-2791:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2795:4-2798:29)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2795:4-2798: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1642:8-1642: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_outl_p.i:1644:9-1644: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_outl_p.i:1644:9-1644:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1662:9-1662:14)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2811:10-2811:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2811:10-2811: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_outl_p.i:2811:10-2811: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_outl_p.i:2811:10-2811: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_outl_p.i:2811:10-2811:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2815:4-2818:27)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2815:4-2818:27)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1672:8-1672:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1677:11-1677:25)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2832:11-2833:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2832:11-2833: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_outl_p.i:2832:11-2833: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_outl_p.i:2832:11-2833: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_outl_p.i:2832:11-2833:35)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2832:11-2833:35)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2834:3-2835:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2834:3-2835: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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:4211:5-4211:21)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1582:2-1582:26)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1705:9-1705:38)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2838:7-2838:40)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2846:11-2847:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2846:11-2847: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_outl_p.i:2846:11-2847: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_outl_p.i:2846:11-2847: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_outl_p.i:2846:11-2847:41)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2846:11-2847:41)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2848:3-2849:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2848:3-2849: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_outl_p.i:4271:5-4271:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1550:2-1550:26)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2852:7-2852: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:1877(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1854:11-1854:12)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1854:11-1854:12)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3:1-3:84)
[Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:670:1-678:1)
[Warning][Deadcode] Function 'pthread_mutex_unlock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:680:1-684:1)
[Warning][Deadcode] Function 'atomic_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:750:1-753:1)
[Warning][Deadcode] Function 'atomic_sub' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:754:1-757:1)
[Warning][Deadcode] Function 'atomic_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:765:1-768:1)
[Warning][Deadcode] Function 'atomic_dec' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:776:1-779:1)
[Warning][Deadcode] Function 'atomic_dec_and_test' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:780:1-795:1)
[Warning][Deadcode] Function 'atomic_inc_and_test' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:796:1-811:1)
[Warning][Deadcode] Function 'atomic_add_negative' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:812:1-827:1)
[Warning][Deadcode] Function 'atomic_add_return' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:828:1-831:1)
[Warning][Deadcode] Function 'atomic_sub_return' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:833:1-836:1)
[Warning][Deadcode] Function 'sigfillset' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:949:1-959:1)
[Warning][Deadcode] Function 'sigaddsetmask' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:963:1-966:1)
[Warning][Deadcode] Function 'sigdelsetmask' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:968:1-971:1)
[Warning][Deadcode] Function 'sigtestsetmask' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:973:1-976:1)
[Warning][Deadcode] Function 'ERR_PTR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1155:1-1158:1)
[Warning][Deadcode] Function 'PTR_ERR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1160:1-1163:1)
[Warning][Deadcode] Function 'IS_ERR' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1165:1-1168:1)
[Warning][Deadcode] Function 'iminor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1292:1-1295:1)
[Warning][Deadcode] Function 'imajor' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1297:1-1300:1)
[Warning][Deadcode] Function 'zf_notify_sys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1730:1-1738:1)
[Warning][Deadcode] Function 'dev_get_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2021:1-2024:1)
[Warning][Deadcode] Function 'dev_set_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2026:1-2029:1)
[Warning][Deadcode] Function 'tasklet_disable' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2136:1-2139:1)
[Warning][Deadcode] Function 'create_request' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2913:1-2926:1)
[Warning][Deadcode] Function 'call_rq_function' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2928:1-2949:1)
[Warning][Deadcode] Function 'call_genhd_functions' is uncalled: 40 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2951:1-3027:1)
[Warning][Deadcode] Function 'create_pci_dev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3041:1-3043:1)
[Warning][Deadcode] Function 'pci_probe_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3045:1-3063:1)
[Warning][Deadcode] Function 'pci_remove_device' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3065:1-3070:1)
[Warning][Deadcode] Function 'call_pci_functions' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3072:1-3090:1)
[Warning][Deadcode] Function 'pci_enable_device' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3126:1-3135:1)
[Warning][Deadcode] Function 'pci_get_class' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3137:1-3153:1)
[Warning][Deadcode] Function 'pci_register_driver' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3155:1-3166:1)
[Warning][Deadcode] Function 'pci_unregister_driver' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3168:1-3172:1)
[Warning][Deadcode] Function 'pci_release_region' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3174:1-3184:1)
[Warning][Deadcode] Function 'pci_request_region' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3186:1-3203:1)
[Warning][Deadcode] Function 'pci_release_regions' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3205:1-3211:1)
[Warning][Deadcode] Function 'pci_request_regions' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3213:1-3227:1)
[Warning][Deadcode] Function 'copy_from_user' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3272:1-3278:1)
[Warning][Deadcode] Function 'register_blkdev' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3284:1-3293:1)
[Warning][Deadcode] Function 'unregister_blkdev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3295:1-3298:1)
[Warning][Deadcode] Function 'alloc_disk' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3300:1-3314:1)
[Warning][Deadcode] Function 'add_disk' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3316:1-3325:1)
[Warning][Deadcode] Function 'del_gendisk' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3327:1-3336:1)
[Warning][Deadcode] Function 'get_fixed_request_queue' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3350:1-3357:1)
[Warning][Deadcode] Function 'blk_init_queue' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3359:1-3375:1)
[Warning][Deadcode] Function 'blk_alloc_queue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3377:1-3392:1)
[Warning][Deadcode] Function 'blk_queue_make_request' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3394:1-3397:1)
[Warning][Deadcode] Function 'end_request' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3399:1-3404:1)
[Warning][Deadcode] Function 'blk_queue_hardsect_size' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3407:1-3410:1)
[Warning][Deadcode] Function 'blk_cleanup_queue' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3412:1-3415:1)
[Warning][Deadcode] Function 'alloc_tty_driver' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3744:1-3752:1)
[Warning][Deadcode] Function 'tty_set_operations' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3754:1-3780:1)
[Warning][Deadcode] Function 'alloc_chrdev_region' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3781:1-3793:1)
[Warning][Deadcode] Function 'register_chrdev_region' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3795:1-3801:1)
[Warning][Deadcode] Function 'register_chrdev' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3805:1-3826:1)
[Warning][Deadcode] Function 'unregister_chrdev' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3828:1-3831:1)
[Warning][Deadcode] Function 'cdev_alloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3833:1-3838:1)
[Warning][Deadcode] Function 'cdev_init' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3840:1-3843:1)
[Warning][Deadcode] Function 'cdev_del' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3870:1-3881:1)
[Warning][Deadcode] Function 'mutex_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3885:1-3893:1)
[Warning][Deadcode] Function 'mutex_lock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3895:1-3906:1)
[Warning][Deadcode] Function 'mutex_unlock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3908:1-3916:1)
[Warning][Deadcode] Function 'inb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3950:1-3953:1)
[Warning][Deadcode] Function 'inl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3968:1-3971:1)
[Warning][Deadcode] Function 'outl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3973:1-3975:1)
[Warning][Deadcode] Function 'outl_p' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:4000:1-4004:1)
[Warning][Deadcode] Function 'schedule' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:4040:1-4044:1)
[Warning][Deadcode] Function 'down' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.i:4078:1-4098:1)
[Warning][Deadcode] Function 'up' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.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_outl_p.i:4434:1-4440:1)
[Warning][Deadcode] Function 'kmalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:4446:1-4453:1)
[Warning][Deadcode] Function 'kzalloc' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:4455:1-4462:1)
[Warning][Deadcode] Function 'vmalloc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.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_outl_p.i:4524:1-4524:67)
[Warning][Deadcode] Function 'kfree' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:4527:1-4530:1)
[Warning][Deadcode] Function 'call_cdev_functions' has dead code:
  on lines 2778..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2778-2779)
  on line 2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2781-2781)
[Warning][Deadcode] Function 'call_interrupt_handler' has dead code:
  on line 3037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3037-3037)
[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_outl_p.i:4364-4365)
[Warning][Deadcode] Function 'call_tasklet_functions' has dead code:
  on lines 3100..3103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3100-3103)
[Warning][Deadcode] Function 'cdev_add' has dead code:
  on line 3863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3863-3863)
[Warning][Deadcode] Function 'misc_register' has dead code:
  on line 3506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3506-3506)
[Warning][Deadcode] Function 'zf_init' has dead code:
  on line 1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1789-1789)
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1804-1804)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1806-1806)
[Warning][Deadcode] Function 'zf_open' has dead code:
  on line 1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1699-1699)
[Warning][Deadcode] Function 'zf_set_timer' has dead code:
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1527-1527)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 363
  dead: 463 (446 in uncalled functions)
  total lines: 826
[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_outl_p.i:2668:9-2668: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_outl_p.i:2668:9-2668:28)
[Warning][Deadcode][CWE-571] condition 'fixed_cdev_used < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3495:7-3495: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_outl_p.i:2846:11-2847: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_outl_p.i:2668:9-2668:28)
[Warning][Deadcode][CWE-571] condition '! result' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2851:7-2851:14)
[Warning][Deadcode][CWE-570] condition 'nowayout' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1698:6-1698:14)
[Warning][Deadcode][CWE-571] condition '! nowayout' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1632:7-1632: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_outl_p.i:2668:9-2668: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_outl_p.i:1642:8-1642: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_outl_p.i:2668:9-2668: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_outl_p.i:2668:9-2668:28)
[Warning][Deadcode][CWE-571] condition '0 <= cdev_no' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:2763:5-2763: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_outl_p.i:3098:8-3099:50)
[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_outl_p.i:2668:9-2668: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_outl_p.i:2668:9-2668:28)
[Warning][Deadcode][CWE-571] condition '(int )number_timer_registered < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.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_outl_p.i:2668:9-2668: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_outl_p.i:2668:9-2668:28)
[Warning][Deadcode][CWE-571] condition 'action <= 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1786:6-1786:35)
[Warning][Deadcode][CWE-571] condition 'action >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1786:6-1786:35)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1803:5-1803:47)
[Warning][Deadcode][CWE-571] condition '(int )n == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1525:3-1525: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_outl_p.i:2672:9-2672: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_outl_p.i:2672:9-2672:27)
[Warning][Deadcode][CWE-571] condition '(int )new > 0xff' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:1528:25-1528:61)
[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_outl_p.i:4363:9-4363:43)
[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_outl_p.i:2767:10-2767: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_outl_p.i:2777:10-2777: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_outl_p.i:2791:10-2791: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_outl_p.i:3854:6-3854: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_outl_p.i:2811:10-2811:52)
[Warning][Deadcode][CWE-570] condition 'registered_irq[i].handler' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_p.i:3036:9-3036: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_outl_p.i:2668:9-2668:28)
[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_outl_p.i:2832:11-2833:35)
[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
