./goblint --conf conf/svcomp.json --set ana.base.privatization vojdani --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.261
[Info] vars: 7392, evals: 5420

[Info] |called|=60

Memory statistics: total=22887.96MB, max=200.75MB, minor=22877.00MB, major=437.02MB, promoted=426.06MB
    minor collections=10918  major collections=19 compactions=0


[Info] runtime: 00:00:20.351
[Info] vars: 9462, evals: 8762

[Info] |called|=71

Memory statistics: total=45836.25MB, max=403.80MB, minor=45818.55MB, major=768.38MB, promoted=750.68MB
    minor collections=21859  major collections=22 compactions=0


[Info] runtime: 00:00:30.394
[Info] vars: 14472, evals: 12878

[Info] |called|=60

Memory statistics: total=72429.75MB, max=464.37MB, minor=72407.86MB, major=1141.83MB, promoted=1119.95MB
    minor collections=34539  major collections=25 compactions=0


[Info] runtime: 00:00:40.490
[Info] vars: 20491, evals: 20915

[Info] |called|=58

Memory statistics: total=99525.31MB, max=706.25MB, minor=99500.39MB, major=1603.77MB, promoted=1578.85MB
    minor collections=47459  major collections=27 compactions=0


[Info] runtime: 00:00:50.535
[Info] vars: 21072, evals: 23473

[Info] |called|=71

Memory statistics: total=124068.45MB, max=812.19MB, minor=124038.15MB, major=1931.94MB, promoted=1901.63MB
    minor collections=59161  major collections=28 compactions=0


[Info] runtime: 00:01:00.586
[Info] vars: 24148, evals: 27210

[Info] |called|=83

Memory statistics: total=147904.16MB, max=934.02MB, minor=147868.13MB, major=2311.00MB, promoted=2274.98MB
    minor collections=70525  major collections=30 compactions=0

