./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.206
vars: 34083, evals: 40360

|rho|=34083
|called|=85
|stable|=33430
|infl|=34006
|wpoint|=51
Found 3504 contexts for 165 functions. Top 5 functions:
252	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 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
126	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
111	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=17182.14MB, max=65.90MB, minor=17176.30MB, major=123.29MB, promoted=117.45MB
    minor collections=8199  major collections=17 compactions=0


runtime: 00:00:20.291
vars: 66629, evals: 77839

|rho|=66629
|called|=73
|stable|=65848
|infl|=66579
|wpoint|=96
Found 6749 contexts for 168 functions. Top 5 functions:
502	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=33756.85MB, max=115.27MB, minor=33747.34MB, major=232.14MB, promoted=222.62MB
    minor collections=16102  major collections=21 compactions=0


runtime: 00:00:30.382
vars: 99383, evals: 115300

|rho|=99383
|called|=62
|stable|=98774
|infl|=99338
|wpoint|=141
Found 10007 contexts for 168 functions. Top 5 functions:
754	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
378	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
378	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
377	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
328	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=50488.28MB, max=132.57MB, minor=50478.15MB, major=336.45MB, promoted=326.32MB
    minor collections=24082  major collections=24 compactions=0


runtime: 00:00:40.470
vars: 131073, evals: 151374

|rho|=131073
|called|=87
|stable|=130531
|infl|=131010
|wpoint|=188
Found 10507 contexts for 141 functions. Top 5 functions:
811	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
423	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
397	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
371	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
317	contexts for entry state of alloc_skb on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:617:1

Memory statistics: total=66845.51MB, max=201.62MB, minor=66832.74MB, major=439.81MB, promoted=427.04MB
    minor collections=31882  major collections=27 compactions=0


runtime: 00:00:50.592
vars: 161639, evals: 186375

|rho|=161639
|called|=76
|stable|=161302
|infl|=161571
|wpoint|=227
Found 16192 contexts for 168 functions. Top 5 functions:
1232	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 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
616	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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=83114.62MB, max=231.87MB, minor=83096.85MB, major=544.27MB, promoted=526.50MB
    minor collections=39638  major collections=28 compactions=0


runtime: 00:01:00.655
vars: 191841, evals: 220698

|rho|=191841
|called|=51
|stable|=191504
|infl|=191805
|wpoint|=269
Found 19193 contexts for 168 functions. Top 5 functions:
1462	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
732	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
732	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
732	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
631	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=99146.52MB, max=266.65MB, minor=99128.14MB, major=641.84MB, promoted=623.47MB
    minor collections=47284  major collections=30 compactions=0


runtime: 00:01:10.750
vars: 220659, evals: 253396

|rho|=220659
|called|=75
|stable|=220322
|infl|=220598
|wpoint|=308
Found 22036 contexts for 168 functions. Top 5 functions:
1675	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 netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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
725	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=115008.75MB, max=306.65MB, minor=114989.75MB, major=737.68MB, promoted=718.68MB
    minor collections=54848  major collections=31 compactions=0


runtime: 00:01:20.824
vars: 248468, evals: 284997

|rho|=248468
|called|=44
|stable|=247756
|infl|=248448
|wpoint|=343
Found 24796 contexts for 168 functions. Top 5 functions:
1882	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
814	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=130811.98MB, max=352.65MB, minor=130792.30MB, major=832.67MB, promoted=812.99MB
    minor collections=62384  major collections=32 compactions=0


runtime: 00:01:30.871
vars: 255566, evals: 294613

|rho|=255566
|called|=61
|stable|=253863
|infl|=255514
|wpoint|=347
Found 25357 contexts for 169 functions. Top 5 functions:
1890	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
946	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
946	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
946	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
824	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=139424.56MB, max=352.65MB, minor=139404.66MB, major=881.87MB, promoted=861.97MB
    minor collections=66491  major collections=32 compactions=0


runtime: 00:01:40.969
vars: 282658, evals: 325528

|rho|=282658
|called|=80
|stable|=280955
|infl|=282592
|wpoint|=383
Found 28039 contexts for 169 functions. Top 5 functions:
2095	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1048	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1048	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1048	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
913	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=154787.70MB, max=405.54MB, minor=154754.60MB, major=983.80MB, promoted=950.70MB
    minor collections=73813  major collections=33 compactions=0


runtime: 00:01:51.032
vars: 310480, evals: 357088

|rho|=310480
|called|=78
|stable|=308777
|infl|=310411
|wpoint|=421
Found 30801 contexts for 169 functions. Top 5 functions:
2310	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1156	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1156	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1155	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1002	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=170627.92MB, max=405.54MB, minor=170594.07MB, major=1075.40MB, promoted=1041.55MB
    minor collections=81367  major collections=34 compactions=0


runtime: 00:02:01.098
vars: 337581, evals: 387897

|rho|=337581
|called|=78
|stable|=335878
|infl|=337511
|wpoint|=457
Found 33494 contexts for 169 functions. Top 5 functions:
2516	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1259	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1259	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1258	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1093	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=186369.68MB, max=466.38MB, minor=186334.53MB, major=1165.81MB, promoted=1130.66MB
    minor collections=88873  major collections=35 compactions=0


runtime: 00:02:11.197
vars: 362894, evals: 416616

|rho|=362894
|called|=37
|stable|=361191
|infl|=362865
|wpoint|=488
Found 35979 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
1171	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=202247.46MB, max=466.38MB, minor=202211.51MB, major=1256.95MB, promoted=1220.99MB
    minor collections=96444  major collections=36 compactions=0


runtime: 00:02:21.224
vars: 373902, evals: 429396

|rho|=373902
|called|=57
|stable|=338023
|infl|=373865
|wpoint|=494
Found 37006 contexts for 204 functions. Top 5 functions:
2732	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1367	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1366	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1365	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1193	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=212092.03MB, max=536.34MB, minor=212055.66MB, major=1314.00MB, promoted=1277.63MB
    minor collections=101138  major collections=36 compactions=0


runtime: 00:02:31.323
vars: 399238, evals: 460342

|rho|=399238
|called|=48
|stable|=363356
|infl|=399212
|wpoint|=526
Found 39549 contexts for 206 functions. Top 5 functions:
2928	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1465	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1464	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1461	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1272	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=228584.82MB, max=536.34MB, minor=228547.68MB, major=1405.62MB, promoted=1368.49MB
    minor collections=109003  major collections=37 compactions=0


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

/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
|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=229115.48MB, max=536.34MB, minor=229078.31MB, major=1408.97MB, promoted=1371.80MB
    minor collections=109256  major collections=37 compactions=0


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: 154.566s
Unsupported library function!
