./deagle --no-assertions --datarace --64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c


--------------------------------------------------------------------------------


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_cond_wait> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_711291139 __annonCompField1;
  union __anonunion____missing_field_name_214694447 __annonCompField2;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_wait"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1574
signed int (pthread_cond_t *, pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_wait> line 7
signed int (pthread_cond_t *cond, pthread_mutex_t *mutex)
file <builtin-library-pthread_cond_signal> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_711291139 __annonCompField1;
  union __anonunion____missing_field_name_214694447 __annonCompField2;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_signal"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 710
signed int (pthread_cond_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_signal> line 7
signed int (pthread_cond_t *cond)
file <builtin-library-pthread_cond_init> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_711291139 __annonCompField1;
  union __anonunion____missing_field_name_214694447 __annonCompField2;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2l] __g_refs;
  unsigned int [2l] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2l] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 707
signed int (pthread_cond_t *, const pthread_condattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_init> line 7
signed int (pthread_cond_t *cond, const pthread_condattr_t *attr)
file <builtin-library-pthread_rwlock_wrlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_wrlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 705
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_wrlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_wrlock$$lock)
file <builtin-library-pthread_mutex_lock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 700
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_destroy> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 699
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_destroy> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_mutex_init> line 27: warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 697
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
file <builtin-library-pthread_mutex_trylock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_trylock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 5224
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_trylock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_rwlock_unlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_unlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 706
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_unlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_unlock$$lock)
file <builtin-library-pthread_mutex_unlock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 701
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_rwlock_init> line 16: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 702
signed int (pthread_rwlock_t *, const pthread_rwlockattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_init> line 16
signed int (pthread_rwlock_t *pthread_rwlock_init$$lock, const pthread_rwlockattr_t *attr)
file <builtin-library-pthread_rwlock_rdlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_rdlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 704
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_rdlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_rdlock$$lock)
Removal of function pointers and virtual functions
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1042 function _socket: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1074 function _connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1104 function _write: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1124 function _read: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1144 function _close: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1288 function _getpeername: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1309 function _getsockname: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 879 function socket_free: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 927 function abort_sockets: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 2564 function sk_alloc: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 2580 function sock_init_data: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1731 function inet_write: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1742 function inet_read: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1770 function inet_close: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1792 function inet_abort: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1667 function inet_stream_connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 1685 function inet_stream_connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 4996 function tcp_input_state: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 5105 function tcp_input_state: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 5606 function tcp_data_queue: replacing function pointer by 15 possible targets
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 15 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
set limit type 2
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
**** WARNING: no body for function sigemptyset
**** WARNING: no body for function sigaddset
**** WARNING: no body for function pthread_sigmask
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function open
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function ioctl
**** WARNING: no body for function vsnprintf
**** WARNING: no body for function system
**** WARNING: no body for function inet_pton
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function __isoc99_sscanf
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function prctl
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
pointer handling for concurrency is unsound
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop wait_for_threads.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 4591 function wait_for_threads thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Not unwinding loop wait_for_threads.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 4591 function wait_for_threads thread 0
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 1
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 2
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 3
**** WARNING: no body for function sigwait

runtime: 00:00:10.175
vars: 34244, evals: 40497

|rho|=34244
|called|=65
|stable|=33591
|infl|=34188
|wpoint|=53
Found 3527 contexts for 165 functions. Top 5 functions:
254	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
128	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
128	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
128	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
113	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=17234.50MB, max=65.90MB, minor=17228.66MB, major=123.64MB, promoted=117.80MB
    minor collections=8223  major collections=17 compactions=0


runtime: 00:00:20.282
vars: 66705, evals: 77960

|rho|=66705
|called|=70
|stable|=65924
|infl|=66659
|wpoint|=96
Found 6753 contexts for 168 functions. Top 5 functions:
503	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
252	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
252	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
252	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
220	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=33835.14MB, max=115.27MB, minor=33825.62MB, major=232.60MB, promoted=223.08MB
    minor collections=16140  major collections=22 compactions=0


runtime: 00:00:30.376
vars: 99998, evals: 115981

|rho|=99998
|called|=60
|stable|=99389
|infl|=99955
|wpoint|=143
Found 10069 contexts for 168 functions. Top 5 functions:
759	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
380	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
380	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
380	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
330	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=50788.05MB, max=132.57MB, minor=50777.91MB, major=338.45MB, promoted=328.30MB
    minor collections=24225  major collections=24 compactions=0


runtime: 00:00:40.469
vars: 131150, evals: 151449

|rho|=131150
|called|=103
|stable|=130609
|infl|=131073
|wpoint|=189
Found 13161 contexts for 168 functions. Top 5 functions:
999	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
500	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
500	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
500	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
432	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=66882.09MB, max=201.62MB, minor=66867.21MB, major=442.55MB, promoted=427.68MB
    minor collections=31899  major collections=27 compactions=0


runtime: 00:00:50.562
vars: 161771, evals: 186508

|rho|=161771
|called|=58
|stable|=161434
|infl|=161721
|wpoint|=227
Found 16205 contexts for 168 functions. Top 5 functions:
1234	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
618	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
618	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
618	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
532	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=83190.81MB, max=231.87MB, minor=83173.04MB, major=545.12MB, promoted=527.35MB
    minor collections=39675  major collections=28 compactions=0


runtime: 00:01:00.641
vars: 191152, evals: 219966

|rho|=191152
|called|=74
|stable|=190815
|infl|=191087
|wpoint|=268
Found 19113 contexts for 168 functions. Top 5 functions:
1458	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
730	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
730	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
730	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
628	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=98849.58MB, max=266.65MB, minor=98831.22MB, major=639.79MB, promoted=621.42MB
    minor collections=47143  major collections=30 compactions=0


runtime: 00:01:10.716
vars: 219986, evals: 252686

|rho|=219986
|called|=67
|stable|=219649
|infl|=219930
|wpoint|=307
Found 21965 contexts for 168 functions. Top 5 functions:
1672	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
838	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
838	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
836	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
721	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=114688.10MB, max=306.65MB, minor=114669.11MB, major=735.35MB, promoted=716.37MB
    minor collections=54695  major collections=31 compactions=0


runtime: 00:01:20.784
vars: 247980, evals: 284442

|rho|=247980
|called|=62
|stable|=247219
|infl|=247927
|wpoint|=344
Found 24741 contexts for 168 functions. Top 5 functions:
1879	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
940	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
940	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
940	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
812	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=130497.63MB, max=352.65MB, minor=130477.98MB, major=829.71MB, promoted=810.06MB
    minor collections=62234  major collections=32 compactions=0


runtime: 00:01:30.823
vars: 254965, evals: 293890

|rho|=254965
|called|=95
|stable|=253262
|infl|=254883
|wpoint|=347
Found 25300 contexts for 169 functions. Top 5 functions:
1883	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
942	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
942	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
942	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
822	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=139038.52MB, max=352.65MB, minor=139018.65MB, major=878.74MB, promoted=858.87MB
    minor collections=66307  major collections=32 compactions=0


runtime: 00:01:40.890
vars: 281815, evals: 324539

|rho|=281815
|called|=87
|stable|=280112
|infl|=281739
|wpoint|=382
Found 27953 contexts for 169 functions. Top 5 functions:
2090	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1046	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1046	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1046	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
909	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=154296.76MB, max=405.54MB, minor=154263.68MB, major=980.10MB, promoted=947.02MB
    minor collections=73579  major collections=33 compactions=0


runtime: 00:01:50.961
vars: 309256, evals: 355760

|rho|=309256
|called|=53
|stable|=307553
|infl|=309211
|wpoint|=418
Found 30681 contexts for 169 functions. Top 5 functions:
2302	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1152	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1152	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1151	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
999	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=169989.93MB, max=405.54MB, minor=169956.12MB, major=1070.45MB, promoted=1036.64MB
    minor collections=81063  major collections=34 compactions=0


runtime: 00:02:01.015
vars: 335776, evals: 385776

|rho|=335776
|called|=77
|stable|=334073
|infl|=335707
|wpoint|=455
Found 33321 contexts for 169 functions. Top 5 functions:
2502	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1252	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1252	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1251	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1086	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=185302.57MB, max=466.38MB, minor=185267.46MB, major=1158.91MB, promoted=1123.81MB
    minor collections=88365  major collections=35 compactions=0


runtime: 00:02:11.111
vars: 362129, evals: 415742

|rho|=362129
|called|=44
|stable|=360426
|infl|=362093
|wpoint|=488
Found 35916 contexts for 169 functions. Top 5 functions:
2694	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1348	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1348	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1348	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1170	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=201379.28MB, max=466.38MB, minor=201343.38MB, major=1250.58MB, promoted=1214.68MB
    minor collections=96031  major collections=36 compactions=0


runtime: 00:02:21.154
vars: 372321, evals: 427539

|rho|=372321
|called|=81
|stable|=336442
|infl|=372260
|wpoint|=493
Found 36854 contexts for 204 functions. Top 5 functions:
2718	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1361	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1360	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1357	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1187	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=211147.20MB, max=536.34MB, minor=211110.89MB, major=1307.40MB, promoted=1271.09MB
    minor collections=100688  major collections=36 compactions=0


runtime: 00:02:31.265
vars: 397178, evals: 458036

|rho|=397178
|called|=47
|stable|=361296
|infl|=397161
|wpoint|=524
Found 39336 contexts for 206 functions. Top 5 functions:
2914	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1457	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1456	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1455	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1267	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=227388.02MB, max=536.34MB, minor=227350.97MB, major=1397.94MB, promoted=1360.89MB
    minor collections=108433  major collections=37 compactions=0


runtime: 00:02:32.542
vars: 400142, evals: 461244

|rho|=400142
|called|=25
|stable|=364260
|infl|=400136
|wpoint|=525
Found 39651 contexts for 206 functions. Top 5 functions:
2938	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1467	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1466	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1465	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1274	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:745:1

Memory statistics: total=229151.03MB, max=536.34MB, minor=229113.86MB, major=1407.68MB, promoted=1370.51MB
    minor collections=109274  major collections=37 compactions=0


/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
Fatal error: exception Failure("Problems evaluating expression to function calls!")
Unwinding loop stop_stack_handler.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 4523 function stop_stack_handler thread 4
Not unwinding loop stop_stack_handler.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c line 4523 function stop_stack_handler thread 4
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 
The number of races before goblint filter: 32
The number of races after goblint filter: 0
Race categories: 0
Runtime Symex: 155.575s
Unsupported library function!
