./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i


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


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/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
Converting
Type-checking race-2_5-container_of
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module race-2_5-container_of file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i line 524
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_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module race-2_5-container_of file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i line 519
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: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module race-2_5-container_of file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i line 515
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_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module race-2_5-container_of file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i line 406
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_mutex_init> line 27: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module race-2_5-container_of file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i line 512
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)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 1 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Unknown value in {&data} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1749:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1710:2)
[Warning][Unknown] Unknown value in {&data} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1751:4)
[Debug][Analyzer] Base EvalInt t1 query answering bot instead of {([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1714:2, main], {})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1722:2)
[Warning][Unknown] Unknown address in {&status} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1722:2)
[Debug][Analyzer] Base EvalInt t2 query answering bot instead of {([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1715:2, main], {})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1735:2)
[Warning][Unknown] Unknown value in {&data.lock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1736:2)
[Warning][Deadcode] Function "__bswap_16" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:64:1)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:69:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:74:15)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:79:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:84:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:89:1)
[Warning][Race] Memory location data.shared.b@race-2_5-container_of.i:1748:18 (race with conf. 110):
  read with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1714:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1697:5)
  read with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1715:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1697:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1733:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1753:4)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1759:3)
  write with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1714:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1700:5)
  write with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1715:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1700:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1727:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1757:3)
[Warning][Race] Memory location data.shared.a@race-2_5-container_of.i:1748:18 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1730:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1752:4)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1758:3)
  write with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1714:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1694:2)
  write with {lock:data.lock, thread:([my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1715:2, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1694:2)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1724:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i:1756:3)

Summary for all memory locations:
	safe:           12
	vulnerable:      0
	unsafe:          2
	-------------------
	total:          14
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
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/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1694 1695 1697 1698 1700 1701 1710 1711 1722 1723 1724 1725 1727 1728 1730 1731 1733 1734 1735 1736 1752 1753 1754 1756 1757 1758 1759 1760 
The number of races before goblint filter: 214
The number of races after goblint filter: 22
Race categories: 7
	1752(1) - 1695(1) main::1::1::data!0@1:
		main::1::1::data!0@1#11..shared..a main::1::1::data!0@1#19..shared..a
		main::1::1::data!0@1#12..shared..a main::1::1::data!0@1#19..shared..a
		main::1::1::data!0@1#11..shared..a main::1::1::data!0@1#26..shared..a
		main::1::1::data!0@1#12..shared..a main::1::1::data!0@1#26..shared..a
	1753(1) - 1701(1) main::1::1::data!0@1:
		main::1::1::data!0@1#11..shared..b main::1::1::data!0@1#21..shared..b
		main::1::1::data!0@1#12..shared..b main::1::1::data!0@1#21..shared..b
		main::1::1::data!0@1#11..shared..b main::1::1::data!0@1#30..shared..b
		main::1::1::data!0@1#12..shared..b main::1::1::data!0@1#30..shared..b
	1756(1) - 1695(1) main::1::1::data!0@1:
		main::1::1::data!0@1#13..shared..a main::1::1::data!0@1#19..shared..a
		main::1::1::data!0@1#13..shared..a main::1::1::data!0@1#26..shared..a
	1757(1) - 1698(1) main::1::1::data!0@1:
		main::1::1::data!0@1#13..shared..b main::1::1::data!0@1#19..shared..b
		main::1::1::data!0@1#13..shared..b main::1::1::data!0@1#28..shared..b
	1757(1) - 1701(1) main::1::1::data!0@1:
		main::1::1::data!0@1#13..shared..b main::1::1::data!0@1#21..shared..b
		main::1::1::data!0@1#13..shared..b main::1::1::data!0@1#30..shared..b
	1758(1) - 1695(1) main::1::1::data!0@1:
		main::1::1::data!0@1#14..shared..a main::1::1::data!0@1#19..shared..a
		main::1::1::data!0@1#15..shared..a main::1::1::data!0@1#19..shared..a
		main::1::1::data!0@1#14..shared..a main::1::1::data!0@1#26..shared..a
		main::1::1::data!0@1#15..shared..a main::1::1::data!0@1#26..shared..a
	1759(1) - 1701(1) main::1::1::data!0@1:
		main::1::1::data!0@1#14..shared..b main::1::1::data!0@1#21..shared..b
		main::1::1::data!0@1#15..shared..b main::1::1::data!0@1#21..shared..b
		main::1::1::data!0@1#14..shared..b main::1::1::data!0@1#30..shared..b
		main::1::1::data!0@1#15..shared..b main::1::1::data!0@1#30..shared..b
Runtime Symex: 0.377287s
Adding SC constraints
Shared __CPROVER_threads_exited: 4R/3W
Shared __CPROVER_next_thread_id: 3R/3W
Shared t1: 2R/2W
Shared t2: 2R/2W
Shared main::1::1::data!0@1..lock: 6R/7W
Shared main::1::1::data!0@1..shared..a: 11R/12W
Shared main::1::1::data!0@1..shared..b: 13R/12W
size of program expression: 889 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0110678s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.011134s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000858395s
Solving with Deagle's Closure solver
16515 variables, 59287 clauses
ClosureSolver finishes with 20 conflicts, 215 decisions, and 12573 propagations. 365 theory propagations and 0 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00366325s
Runtime decision procedure: 0.0251474s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i function my_drv_probe
[nodatarace.assertion.0] line 1715 No data races on variable main::1::1::data!0@1 between line 1752 and line 1695: SUCCESS
[nodatarace.assertion.1] line 1715 No data races on variable main::1::1::data!0@1 between line 1753 and line 1701: SUCCESS
[nodatarace.assertion.2] line 1715 No data races on variable main::1::1::data!0@1 between line 1756 and line 1695: SUCCESS
[nodatarace.assertion.3] line 1715 No data races on variable main::1::1::data!0@1 between line 1757 and line 1698: SUCCESS
[nodatarace.assertion.4] line 1715 No data races on variable main::1::1::data!0@1 between line 1757 and line 1701: SUCCESS
[nodatarace.assertion.5] line 1715 No data races on variable main::1::1::data!0@1 between line 1758 and line 1695: SUCCESS
[nodatarace.assertion.6] line 1715 No data races on variable main::1::1::data!0@1 between line 1759 and line 1701: SUCCESS

** 0 of 7 failed (1 iterations)
VERIFICATION SUCCESSFUL
