./goblint --conf conf/svcomp.json --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.213
[Info] vars: 8267, evals: 6437

[Info] |called|=71

Memory statistics: total=24106.26MB, max=151.80MB, minor=24093.09MB, major=321.24MB, promoted=308.06MB
    minor collections=11498  major collections=19 compactions=0


[Info] runtime: 00:00:20.247
[Info] vars: 9430, evals: 9650

[Info] |called|=49

Memory statistics: total=48234.92MB, max=174.57MB, minor=48215.07MB, major=519.38MB, promoted=499.54MB
    minor collections=23003  major collections=23 compactions=0


[Info] runtime: 00:00:30.282
[Info] vars: 17643, evals: 18403

[Info] |called|=54

Memory statistics: total=78695.55MB, max=230.87MB, minor=78672.88MB, major=733.49MB, promoted=710.83MB
    minor collections=37528  major collections=26 compactions=0


[Info] runtime: 00:00:40.306
[Info] vars: 17648, evals: 20886

[Info] |called|=63

Memory statistics: total=102978.09MB, max=265.50MB, minor=102948.90MB, major=927.43MB, promoted=898.23MB
    minor collections=49105  major collections=29 compactions=0


[Info] runtime: 00:00:50.334
[Info] vars: 20724, evals: 25053

[Info] |called|=59

Memory statistics: total=126647.86MB, max=265.50MB, minor=126611.82MB, major=1162.64MB, promoted=1126.60MB
    minor collections=60391  major collections=32 compactions=0


[Info] runtime: 00:01:00.392
[Info] vars: 25332, evals: 29531

[Info] |called|=36

Memory statistics: total=148912.39MB, max=351.13MB, minor=148867.93MB, major=1472.28MB, promoted=1427.82MB
    minor collections=71005  major collections=35 compactions=0

