./goblint --conf conf/svcomp.json --set ana.base.privatization none2 --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/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.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
:-1: Warning: Incompatible declaration for pthread_create (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:32 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic 
	Failed assumption that union __anonunion_pthread_attr_t_145707745 and union pthread_attr_t are isomorphic (different array sizes)
union __anonunion_pthread_attr_t_145707745 {
   char __size[56] ;
   long __align ;
};

union pthread_attr_t {
   char __size[36] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_mutex_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:38 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic 
	Failed assumption that union __anonunion_pthread_mutex_t_109907136 and union __anonunion_pthread_mutex_t_335460617 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 7 != 6.)
union __anonunion_pthread_mutex_t_109907136 {
   struct __pthread_mutex_s __data ;
   char __size[40] ;
   long __align ;
};

union __anonunion_pthread_mutex_t_335460617 {
   struct __pthread_mutex_s __data ;
   char __size[24] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_mutex_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:41 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic 
	Failed assumption that union __anonunion_pthread_mutex_t_109907136 and union __anonunion_pthread_mutex_t_335460617 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 7 != 6.)
union __anonunion_pthread_mutex_t_109907136 {
   struct __pthread_mutex_s __data ;
   char __size[40] ;
   long __align ;
};

union __anonunion_pthread_mutex_t_335460617 {
   struct __pthread_mutex_s __data ;
   char __size[24] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_mutex_trylock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:43 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic 
	Failed assumption that union __anonunion_pthread_mutex_t_109907136 and union __anonunion_pthread_mutex_t_335460617 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 7 != 6.)
union __anonunion_pthread_mutex_t_109907136 {
   struct __pthread_mutex_s __data ;
   char __size[40] ;
   long __align ;
};

union __anonunion_pthread_mutex_t_335460617 {
   struct __pthread_mutex_s __data ;
   char __size[24] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_mutex_lock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:45 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic 
	Failed assumption that union __anonunion_pthread_mutex_t_109907136 and union __anonunion_pthread_mutex_t_335460617 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 7 != 6.)
union __anonunion_pthread_mutex_t_109907136 {
   struct __pthread_mutex_s __data ;
   char __size[40] ;
   long __align ;
};

union __anonunion_pthread_mutex_t_335460617 {
   struct __pthread_mutex_s __data ;
   char __size[24] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_mutex_unlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i:47 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i (0)) 
	Failed assumption that pthread_mutex_t and pthread_mutex_t are isomorphic 
	Failed assumption that union __anonunion_pthread_mutex_t_109907136 and union __anonunion_pthread_mutex_t_335460617 are isomorphic (different number of fields in __pthread_mutex_s and __pthread_mutex_s: 7 != 6.)
union __anonunion_pthread_mutex_t_109907136 {
   struct __pthread_mutex_s __data ;
   char __size[40] ;
   long __align ;
};

union __anonunion_pthread_mutex_t_335460617 {
   struct __pthread_mutex_s __data ;
   char __size[24] ;
   long __align ;
};
 
[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] malloc wrapper: ldv_xmalloc
[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) )

[Info] runtime: 00:00:10.265
[Info] vars: 12940, evals: 7846

[Info] |called|=54

Memory statistics: total=26472.90MB, max=305.32MB, minor=26466.47MB, major=472.71MB, promoted=466.28MB
    minor collections=12628  major collections=17 compactions=0


[Info] runtime: 00:00:20.375
[Info] vars: 18705, evals: 14623

[Info] |called|=51

Memory statistics: total=54762.37MB, max=614.13MB, minor=54754.00MB, major=893.91MB, promoted=885.54MB
    minor collections=26118  major collections=19 compactions=0


[Info] runtime: 00:00:30.416
[Info] vars: 28187, evals: 21509

[Info] |called|=36

Memory statistics: total=78810.64MB, max=812.19MB, minor=78799.56MB, major=1417.24MB, promoted=1406.15MB
    minor collections=37585  major collections=21 compactions=0

