./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.169
vars: 34128, evals: 40399

|rho|=34128
|called|=68
|stable|=33475
|infl|=34068
|wpoint|=51
Found 3510 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
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=17203.49MB, max=65.90MB, minor=17197.66MB, major=123.45MB, promoted=117.62MB
    minor collections=8209  major collections=17 compactions=0


runtime: 00:00:20.233
vars: 66838, evals: 78140

|rho|=66838
|called|=70
|stable|=66057
|infl|=66792
|wpoint|=96
Found 6765 contexts for 168 functions. Top 5 functions:
504	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
254	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
254	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
252	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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=33905.99MB, max=115.27MB, minor=33896.47MB, major=232.78MB, promoted=223.26MB
    minor collections=16174  major collections=22 compactions=0


runtime: 00:00:30.296
vars: 99707, evals: 115704

|rho|=99707
|called|=44
|stable|=99098
|infl|=99680
|wpoint|=141
Found 10035 contexts for 168 functions. Top 5 functions:
758	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
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=50696.48MB, max=132.57MB, minor=50686.34MB, major=337.59MB, promoted=327.44MB
    minor collections=24181  major collections=24 compactions=0


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

|rho|=131073
|called|=87
|stable|=130531
|infl|=131010
|wpoint|=188
Found 0 contexts for 0 functions. Top 5 functions:

Memory statistics: total=66808.17MB, max=201.62MB, minor=66795.40MB, major=439.27MB, promoted=426.50MB
    minor collections=31865  major collections=27 compactions=0


runtime: 00:00:50.483
vars: 161235, evals: 185854

|rho|=161235
|called|=71
|stable|=160898
|infl|=161172
|wpoint|=227
Found 16156 contexts for 168 functions. Top 5 functions:
1227	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
614	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
614	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
614	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=82839.54MB, max=231.87MB, minor=82821.77MB, major=542.33MB, promoted=524.57MB
    minor collections=39507  major collections=28 compactions=0


runtime: 00:01:00.567
vars: 191107, evals: 219927

|rho|=191107
|called|=96
|stable|=190770
|infl|=191020
|wpoint|=268
Found 19107 contexts for 168 functions. Top 5 functions:
1456	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 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
728	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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=98779.78MB, max=266.65MB, minor=98761.42MB, major=639.17MB, promoted=620.81MB
    minor collections=47109  major collections=30 compactions=0


runtime: 00:01:10.646
vars: 219821, evals: 252427

|rho|=219821
|called|=71
|stable|=219484
|infl|=219761
|wpoint|=307
Found 21951 contexts for 168 functions. Top 5 functions:
1671	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
836	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
836	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
836	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713: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=114505.06MB, max=306.65MB, minor=114486.07MB, major=733.83MB, promoted=714.85MB
    minor collections=54608  major collections=31 compactions=0


runtime: 00:01:20.734
vars: 247619, evals: 284087

|rho|=247619
|called|=83
|stable|=246865
|infl|=247544
|wpoint|=342
Found 24698 contexts for 168 functions. Top 5 functions:
1876	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 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
938	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
810	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=130290.98MB, max=352.65MB, minor=130271.33MB, major=827.67MB, promoted=808.02MB
    minor collections=62135  major collections=32 compactions=0


runtime: 00:01:30.773
vars: 254490, evals: 293425

|rho|=254490
|called|=44
|stable|=252787
|infl|=254454
|wpoint|=343
Found 25255 contexts for 169 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
820	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=138782.41MB, max=352.65MB, minor=138762.54MB, major=875.95MB, promoted=856.08MB
    minor collections=66184  major collections=32 compactions=0


runtime: 00:01:40.841
vars: 281547, evals: 324227

|rho|=281547
|called|=85
|stable|=279844
|infl|=281480
|wpoint|=383
Found 27929 contexts for 169 functions. Top 5 functions:
2087	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1044	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1044	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1044	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=154085.41MB, max=405.54MB, minor=154052.33MB, major=977.72MB, promoted=944.64MB
    minor collections=73478  major collections=33 compactions=0


runtime: 00:01:50.924
vars: 309316, evals: 355813

|rho|=309316
|called|=62
|stable|=307613
|infl|=309262
|wpoint|=418
Found 30688 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 netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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
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=169942.83MB, max=405.54MB, minor=169909.02MB, major=1069.53MB, promoted=1035.72MB
    minor collections=81040  major collections=34 compactions=0


runtime: 00:02:01.008
vars: 335857, evals: 385878

|rho|=335857
|called|=86
|stable|=334154
|infl|=335780
|wpoint|=456
Found 33324 contexts for 169 functions. Top 5 functions:
2503	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 netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576: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
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=185282.01MB, max=466.38MB, minor=185246.90MB, major=1158.05MB, promoted=1122.94MB
    minor collections=88355  major collections=35 compactions=0


runtime: 00:02:11.111
vars: 362024, evals: 415646

|rho|=362024
|called|=41
|stable|=360321
|infl|=361991
|wpoint|=488
Found 35907 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=201243.61MB, max=466.38MB, minor=201207.71MB, major=1248.61MB, promoted=1212.72MB
    minor collections=95966  major collections=36 compactions=0


runtime: 00:02:21.158
vars: 371794, evals: 426972

|rho|=371794
|called|=67
|stable|=335915
|infl|=371751
|wpoint|=492
Found 36802 contexts for 204 functions. Top 5 functions:
2716	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1359	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1358	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
1185	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=210813.87MB, max=536.34MB, minor=210777.56MB, major=1304.50MB, promoted=1268.18MB
    minor collections=100529  major collections=36 compactions=0


runtime: 00:02:31.254
vars: 396885, evals: 457648

|rho|=396885
|called|=73
|stable|=361003
|infl|=396834
|wpoint|=524
Found 39307 contexts for 206 functions. Top 5 functions:
2911	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1455	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1454	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1453	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1265	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=227063.59MB, max=536.34MB, minor=227026.55MB, major=1395.28MB, promoted=1358.24MB
    minor collections=108278  major collections=37 compactions=0


runtime: 00:02:32.676
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=229079.22MB, max=536.34MB, minor=229042.05MB, major=1406.25MB, promoted=1369.09MB
    minor collections=109239  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.661s
Unsupported library function!
