./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.183
vars: 33496, evals: 39607

|rho|=33496
|called|=85
|stable|=32843
|infl|=33419
|wpoint|=51
Found 3454 contexts for 165 functions. Top 5 functions:
246	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
124	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
124	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
124	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
110	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=16830.54MB, max=65.90MB, minor=16824.71MB, major=121.24MB, promoted=115.41MB
    minor collections=8031  major collections=17 compactions=0


runtime: 00:00:20.298
vars: 65697, evals: 76808

|rho|=65697
|called|=76
|stable|=64916
|infl|=65648
|wpoint|=96
Found 6653 contexts for 168 functions. Top 5 functions:
496	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
250	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
250	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
248	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
216	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=33294.79MB, max=115.27MB, minor=33286.33MB, major=228.33MB, promoted=219.87MB
    minor collections=15883  major collections=21 compactions=0


runtime: 00:00:30.398
vars: 98574, evals: 114391

|rho|=98574
|called|=62
|stable|=97965
|infl|=98532
|wpoint|=141
Found 9923 contexts for 168 functions. Top 5 functions:
750	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
376	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
376	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
375	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
324	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=50059.43MB, max=132.57MB, minor=50049.31MB, major=333.85MB, promoted=323.72MB
    minor collections=23877  major collections=24 compactions=0


runtime: 00:00:40.481
vars: 130237, evals: 150390

|rho|=130237
|called|=88
|stable|=129696
|infl|=130171
|wpoint|=186
Found 13080 contexts for 168 functions. Top 5 functions:
990	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
496	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
496	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
495	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
429	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=66398.50MB, max=175.32MB, minor=66387.84MB, major=435.25MB, promoted=424.59MB
    minor collections=31670  major collections=27 compactions=0


runtime: 00:00:50.576
vars: 160201, evals: 184660

|rho|=160201
|called|=86
|stable|=159864
|infl|=160126
|wpoint|=227
Found 16053 contexts for 168 functions. Top 5 functions:
1220	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
611	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
611	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
610	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
528	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=82287.60MB, max=231.87MB, minor=82269.85MB, major=539.84MB, promoted=522.09MB
    minor collections=39244  major collections=28 compactions=0


runtime: 00:01:00.624
vars: 189886, evals: 218504

|rho|=189886
|called|=77
|stable|=189549
|infl|=189821
|wpoint|=268
Found 18987 contexts for 168 functions. Top 5 functions:
1448	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
725	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
725	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
724	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
624	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=98127.36MB, max=266.65MB, minor=98109.03MB, major=635.86MB, promoted=617.53MB
    minor collections=46798  major collections=30 compactions=0


runtime: 00:01:10.715
vars: 218445, evals: 250844

|rho|=218445
|called|=61
|stable|=218108
|infl|=218392
|wpoint|=305
Found 21823 contexts for 168 functions. Top 5 functions:
1658	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
830	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
830	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
830	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
716	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=113810.92MB, max=306.65MB, minor=113791.97MB, major=730.14MB, promoted=711.19MB
    minor collections=54277  major collections=31 compactions=0


runtime: 00:01:20.807
vars: 246416, evals: 282680

|rho|=246416
|called|=82
|stable|=245662
|infl|=246345
|wpoint|=342
Found 24580 contexts for 168 functions. Top 5 functions:
1867	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
935	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
935	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
934	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
806	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=129623.44MB, max=352.65MB, minor=129603.83MB, major=824.51MB, promoted=804.89MB
    minor collections=61817  major collections=32 compactions=0


runtime: 00:01:30.842
vars: 254107, evals: 292911

|rho|=254107
|called|=30
|stable|=252377
|infl|=254082
|wpoint|=343
Found 25234 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
819	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=138437.03MB, max=352.65MB, minor=138417.18MB, major=875.01MB, promoted=855.15MB
    minor collections=66020  major collections=32 compactions=0


runtime: 00:01:40.886
vars: 279941, evals: 322468

|rho|=279941
|called|=90
|stable|=278238
|infl|=279864
|wpoint|=380
Found 27769 contexts for 169 functions. Top 5 functions:
2075	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1039	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1039	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1038	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
903	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=153295.14MB, max=405.54MB, minor=153262.12MB, major=973.64MB, promoted=940.61MB
    minor collections=73102  major collections=33 compactions=0


runtime: 00:01:50.945
vars: 307065, evals: 353166

|rho|=307065
|called|=80
|stable|=305362
|infl|=306996
|wpoint|=417
Found 30464 contexts for 169 functions. Top 5 functions:
2283	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1142	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1142	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1142	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
993	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=168641.30MB, max=405.54MB, minor=168607.55MB, major=1062.59MB, promoted=1028.85MB
    minor collections=80420  major collections=34 compactions=0


runtime: 00:02:01.033
vars: 333870, evals: 383631

|rho|=333870
|called|=91
|stable|=332167
|infl|=333790
|wpoint|=454
Found 33125 contexts for 169 functions. Top 5 functions:
2487	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1244	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1244	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1244	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1081	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=184180.29MB, max=466.38MB, minor=184145.25MB, major=1152.36MB, promoted=1117.32MB
    minor collections=87829  major collections=35 compactions=0


runtime: 00:02:11.128
vars: 360965, evals: 414453

|rho|=360965
|called|=56
|stable|=359262
|infl|=360922
|wpoint|=490
Found 35821 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
1169	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=200252.56MB, max=466.38MB, minor=200216.73MB, major=1243.60MB, promoted=1207.76MB
    minor collections=95493  major collections=36 compactions=0


runtime: 00:02:21.168
vars: 369728, evals: 424558

|rho|=369728
|called|=31
|stable|=333959
|infl|=369714
|wpoint|=488
Found 36571 contexts for 187 functions. Top 5 functions:
2702	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1353	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1352	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1351	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1182	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=209567.85MB, max=536.34MB, minor=209531.60MB, major=1298.36MB, promoted=1262.11MB
    minor collections=99935  major collections=36 compactions=0


runtime: 00:02:31.235
vars: 394390, evals: 454841

|rho|=394390
|called|=71
|stable|=358508
|infl|=394338
|wpoint|=519
Found 39057 contexts for 206 functions. Top 5 functions:
2891	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:658:1
1445	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3713:1
1444	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3692:1
1443	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3576:1
1257	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=225697.47MB, max=536.34MB, minor=225660.51MB, major=1387.79MB, promoted=1350.83MB
    minor collections=107627  major collections=37 compactions=0


runtime: 00:02:33.626
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=229138.38MB, max=536.34MB, minor=229101.21MB, major=1406.87MB, promoted=1369.70MB
    minor collections=109267  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-pure
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle-pure/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: 156.616s
Unsupported library function!
