./deagle --no-assertions --datarace --64 /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/level-ip/main.c line 1042 function _socket: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1074 function _connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1104 function _write: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1124 function _read: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1144 function _close: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1288 function _getpeername: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1309 function _getsockname: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 879 function socket_free: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 927 function abort_sockets: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 2564 function sk_alloc: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 2580 function sock_init_data: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1731 function inet_write: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1742 function inet_read: replacing function pointer by 6 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1770 function inet_close: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1792 function inet_abort: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1667 function inet_stream_connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 1685 function inet_stream_connect: replacing function pointer by 2 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 4996 function tcp_input_state: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c line 5105 function tcp_input_state: replacing function pointer by 15 possible targets
file /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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.178
vars: 34088, evals: 40364

|rho|=34088
|called|=76
|stable|=33435
|infl|=34020
|wpoint|=51
Found 3505 contexts for 165 functions. Top 5 functions:
253	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
128	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
128	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
126	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
111	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=17204.23MB, max=65.90MB, minor=17198.39MB, major=123.34MB, promoted=117.51MB
    minor collections=8209  major collections=17 compactions=0


runtime: 00:00:20.268
vars: 67230, evals: 78523

|rho|=67230
|called|=78
|stable|=66449
|infl|=67180
|wpoint|=98
Found 6810 contexts for 168 functions. Top 5 functions:
507	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
254	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
254	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
254	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
222	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=34086.84MB, max=115.27MB, minor=34077.31MB, major=234.43MB, promoted=224.91MB
    minor collections=16260  major collections=22 compactions=0


runtime: 00:00:30.331
vars: 100081, evals: 116118

|rho|=100081
|called|=68
|stable|=99472
|infl|=100030
|wpoint|=142
Found 10077 contexts for 168 functions. Top 5 functions:
760	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
381	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
381	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
380	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
330	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=50932.55MB, max=132.57MB, minor=50922.40MB, major=339.16MB, promoted=329.01MB
    minor collections=24294  major collections=24 compactions=0


runtime: 00:00:40.429
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/the-continuous-race/benchmarks/level-ip/main.c:658:1
500	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
500	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
500	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
432	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=66963.06MB, max=201.62MB, minor=66948.19MB, major=443.07MB, promoted=428.20MB
    minor collections=31937  major collections=27 compactions=0


runtime: 00:00:50.536
vars: 162145, evals: 186922

|rho|=162145
|called|=76
|stable|=161808
|infl|=162077
|wpoint|=228
Found 16247 contexts for 168 functions. Top 5 functions:
1236	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
619	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
619	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
618	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
534	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=83456.87MB, max=231.87MB, minor=83439.08MB, major=546.91MB, promoted=529.13MB
    minor collections=39801  major collections=28 compactions=0


runtime: 00:01:00.614
vars: 192330, evals: 221214

|rho|=192330
|called|=76
|stable|=191993
|infl|=192262
|wpoint|=270
Found 19240 contexts for 168 functions. Top 5 functions:
1463	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
733	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
733	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
732	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
633	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=99479.57MB, max=266.65MB, minor=99461.18MB, major=644.27MB, promoted=625.88MB
    minor collections=47442  major collections=30 compactions=0


runtime: 00:01:10.704
vars: 221039, evals: 253896

|rho|=221039
|called|=85
|stable|=220702
|infl|=220966
|wpoint|=308
Found 22069 contexts for 168 functions. Top 5 functions:
1679	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
841	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
841	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
840	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
725	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=115368.10MB, max=306.65MB, minor=115349.09MB, major=739.52MB, promoted=720.51MB
    minor collections=55019  major collections=31 compactions=0


runtime: 00:01:20.783
vars: 248468, evals: 285147

|rho|=248468
|called|=35
|stable|=247901
|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/the-continuous-race/benchmarks/level-ip/main.c:658:1
942	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
942	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
942	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
814	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=131075.84MB, max=352.65MB, minor=131056.17MB, major=833.27MB, promoted=813.61MB
    minor collections=62509  major collections=32 compactions=0


runtime: 00:01:30.837
vars: 255541, evals: 294595

|rho|=255541
|called|=62
|stable|=253838
|infl|=255488
|wpoint|=346
Found 25354 contexts for 169 functions. Top 5 functions:
1890	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
946	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
946	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
946	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
824	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=139519.07MB, max=352.65MB, minor=139499.18MB, major=881.94MB, promoted=862.05MB
    minor collections=66536  major collections=33 compactions=0


runtime: 00:01:40.927
vars: 282658, evals: 325505

|rho|=282658
|called|=75
|stable|=280948
|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/the-continuous-race/benchmarks/level-ip/main.c:658:1
1048	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1048	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1048	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
913	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=154879.72MB, max=405.54MB, minor=154846.63MB, major=983.75MB, promoted=950.65MB
    minor collections=73857  major collections=33 compactions=0


runtime: 00:01:50.962
vars: 310150, evals: 356680

|rho|=310150
|called|=98
|stable|=308447
|infl|=310061
|wpoint|=421
Found 30771 contexts for 169 functions. Top 5 functions:
2304	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
1154	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1154	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1152	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1002	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=170524.41MB, max=405.54MB, minor=170490.58MB, major=1074.77MB, promoted=1040.94MB
    minor collections=81317  major collections=34 compactions=0


runtime: 00:02:01.040
vars: 336387, evals: 386491

|rho|=336387
|called|=92
|stable|=334684
|infl|=336312
|wpoint|=458
Found 33376 contexts for 169 functions. Top 5 functions:
2507	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
1254	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1254	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1254	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1089	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=185767.05MB, max=466.38MB, minor=185731.93MB, major=1162.30MB, promoted=1127.18MB
    minor collections=88585  major collections=35 compactions=0


runtime: 00:02:11.170
vars: 362603, evals: 416199

|rho|=362603
|called|=38
|stable|=360900
|infl|=362573
|wpoint|=488
Found 35960 contexts for 169 functions. Top 5 functions:
2694	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
1348	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1348	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1348	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1171	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=201898.01MB, max=466.38MB, minor=201862.07MB, major=1255.07MB, promoted=1219.14MB
    minor collections=96278  major collections=36 compactions=0


runtime: 00:02:21.200
vars: 373235, evals: 428610

|rho|=373235
|called|=98
|stable|=337356
|infl|=373160
|wpoint|=495
Found 36938 contexts for 204 functions. Top 5 functions:
2726	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
1365	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1364	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1361	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1190	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=211787.17MB, max=536.34MB, minor=211750.83MB, major=1311.78MB, promoted=1275.44MB
    minor collections=100993  major collections=36 compactions=0


runtime: 00:02:31.259
vars: 397806, evals: 458738

|rho|=397806
|called|=68
|stable|=361924
|infl|=397757
|wpoint|=524
Found 39400 contexts for 206 functions. Top 5 functions:
2916	contexts for entry state of skb_push on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:658:1
1458	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1457	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1455	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1269	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=227911.44MB, max=536.34MB, minor=227874.36MB, major=1401.21MB, promoted=1364.13MB
    minor collections=108682  major collections=37 compactions=0


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

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/level-ip/main.c:658:1
1467	contexts for entry state of checksum on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3713:1
1466	contexts for entry state of sum_every_16bits on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3692:1
1465	contexts for entry state of netdev_transmit on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:3576:1
1274	contexts for entry state of list_add_tail on /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/level-ip/main.c:745:1

Memory statistics: total=229274.71MB, max=536.34MB, minor=229237.54MB, major=1409.04MB, promoted=1371.86MB
    minor collections=109332  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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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/the-continuous-race/benchmarks/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.266s
Unsupported library function!
