./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.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-4_1-thread_local_vars.i
Converting
Type-checking race-4_1-thread_local_vars
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module race-4_1-thread_local_vars file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 392
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-4_1-thread_local_vars file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 498
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 *pthread_mutex_init$$mutex, const pthread_mutexattr_t *mutexattr)
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-4_1-thread_local_vars file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 505
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 *pthread_mutex_lock$$mutex)
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-4_1-thread_local_vars file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 510
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 *pthread_mutex_unlock$$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-4_1-thread_local_vars file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 501
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 *pthread_mutex_destroy$$mutex)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1779:4)
[Debug][Analyzer] Base EvalInt t2 query answering bot instead of {([thread_ath9k@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1719:7, thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {}), ([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {thread_ath9k@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1719:7})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1725:4)
[Warning][Unknown] Unknown address in {&status} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1725:4)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1717:4)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1705:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1746:7)
[Debug][Analyzer] Base EvalInt t1 query answering bot instead of {([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {})} (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1790:4)
[Warning][Unknown] Unknown address in {&status} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1790:4)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:55:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:60:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:65:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:70:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:75:1)
[Warning][Race] Memory location pdev@race-4_1-thread_local_vars.i:1696:5 (race with conf. 110):
  read with {lock:mutex} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1700:4)
  read with {thread:([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1760:6)
  read with {thread:([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1772:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1793:4)
  write with {lock:mutex} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1699:4)
  write with {thread:([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1759:6)
  write with {thread:([thread_usb@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1781:7, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1771:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i:1792:4)

Summary for all memory locations:
	safe:            3
	vulnerable:      0
	unsafe:          1
	-------------------
	total:           4
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
Unwinding recursion pthread_create iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thread_usb.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1745 function thread_usb thread 1
Unwinding recursion pthread_create iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thread_usb.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1745 function thread_usb thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thread_ath9k.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1704 function thread_ath9k thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop thread_ath9k.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1704 function thread_ath9k thread 2
Unwinding recursion __spawned_thread iteration 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Unwinding loop thread_ath9k.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1704 function thread_ath9k thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Not unwinding loop thread_ath9k.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i line 1704 function thread_ath9k thread 3
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-4_1-thread_local_vars.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1699 1700 1701 1705 1706 1725 1726 1746 1747 1759 1760 1761 1771 1772 1773 1779 1780 1790 1791 1792 1793 1794 
The number of races before goblint filter: 289
The number of races after goblint filter: 115
Race categories: 18
	1699(1) - 1699(1) pdev:
		pdev#18 pdev#24
		pdev#18 pdev#27
		pdev#21 pdev#24
		pdev#21 pdev#27
	1699(1) - 1700(1) pdev:
		pdev#18 pdev#25
		pdev#18 pdev#26
		pdev#18 pdev#28
		pdev#18 pdev#29
		pdev#21 pdev#25
		pdev#21 pdev#26
		pdev#21 pdev#28
		pdev#21 pdev#29
	1700(1) - 1699(1) pdev:
		pdev#19 pdev#24
		pdev#19 pdev#27
		pdev#20 pdev#24
		pdev#20 pdev#27
		pdev#22 pdev#24
		pdev#22 pdev#27
		pdev#23 pdev#24
		pdev#23 pdev#27
	1759(1) - 1699(1) pdev:
		pdev#9 pdev#18
		pdev#9 pdev#21
		pdev#12 pdev#18
		pdev#12 pdev#21
		pdev#9 pdev#24
		pdev#9 pdev#27
		pdev#12 pdev#24
		pdev#12 pdev#27
	1759(1) - 1700(1) pdev:
		pdev#9 pdev#19
		pdev#9 pdev#20
		pdev#9 pdev#22
		pdev#9 pdev#23
		pdev#12 pdev#19
		pdev#12 pdev#20
		pdev#12 pdev#22
		pdev#12 pdev#23
		pdev#9 pdev#25
		pdev#9 pdev#26
		pdev#9 pdev#28
		pdev#9 pdev#29
		pdev#12 pdev#25
		pdev#12 pdev#26
		pdev#12 pdev#28
		pdev#12 pdev#29
	1760(1) - 1699(1) pdev:
		pdev#10 pdev#18
		pdev#10 pdev#21
		pdev#11 pdev#18
		pdev#11 pdev#21
		pdev#13 pdev#18
		pdev#13 pdev#21
		pdev#14 pdev#18
		pdev#14 pdev#21
		pdev#10 pdev#24
		pdev#10 pdev#27
		pdev#11 pdev#24
		pdev#11 pdev#27
		pdev#13 pdev#24
		pdev#13 pdev#27
		pdev#14 pdev#24
		pdev#14 pdev#27
	1771(1) - 1699(1) pdev:
		pdev#15 pdev#18
		pdev#15 pdev#21
		pdev#15 pdev#24
		pdev#15 pdev#27
	1771(1) - 1700(1) pdev:
		pdev#15 pdev#19
		pdev#15 pdev#20
		pdev#15 pdev#22
		pdev#15 pdev#23
		pdev#15 pdev#25
		pdev#15 pdev#26
		pdev#15 pdev#28
		pdev#15 pdev#29
	1772(1) - 1699(1) pdev:
		pdev#16 pdev#18
		pdev#16 pdev#21
		pdev#17 pdev#18
		pdev#17 pdev#21
		pdev#16 pdev#24
		pdev#16 pdev#27
		pdev#17 pdev#24
		pdev#17 pdev#27
	1792(1) - 1699(1) pdev:
		pdev#6 pdev#18
		pdev#6 pdev#21
		pdev#6 pdev#24
		pdev#6 pdev#27
	1792(1) - 1700(1) pdev:
		pdev#6 pdev#19
		pdev#6 pdev#20
		pdev#6 pdev#22
		pdev#6 pdev#23
		pdev#6 pdev#25
		pdev#6 pdev#26
		pdev#6 pdev#28
		pdev#6 pdev#29
	1792(1) - 1759(1) pdev:
		pdev#6 pdev#9
		pdev#6 pdev#12
	1792(1) - 1760(1) pdev:
		pdev#6 pdev#10
		pdev#6 pdev#11
		pdev#6 pdev#13
		pdev#6 pdev#14
	1792(1) - 1771(1) pdev:
		pdev#6 pdev#15
	1792(1) - 1772(1) pdev:
		pdev#6 pdev#16
		pdev#6 pdev#17
	1793(1) - 1699(1) pdev:
		pdev#7 pdev#18
		pdev#7 pdev#21
		pdev#8 pdev#18
		pdev#8 pdev#21
		pdev#7 pdev#24
		pdev#7 pdev#27
		pdev#8 pdev#24
		pdev#8 pdev#27
	1793(1) - 1759(1) pdev:
		pdev#7 pdev#9
		pdev#7 pdev#12
		pdev#8 pdev#9
		pdev#8 pdev#12
	1793(1) - 1771(1) pdev:
		pdev#7 pdev#15
		pdev#8 pdev#15
Runtime Symex: 0.670701s
Adding SC constraints
Shared __CPROVER_threads_exited: 6R/4W
Shared __CPROVER_next_thread_id: 5R/4W
Shared t1: 2R/2W
Shared t2: 4R/3W
Shared mutex: 10R/12W
Shared pdev: 18R/11W
Shared ldv_usb_state: 6R/6W
size of program expression: 1364 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0176606s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0182296s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00229665s
Solving with Deagle's Closure solver
22047 variables, 87076 clauses
ClosureSolver finishes with 95 conflicts, 1455 decisions, and 49129 propagations. 193 theory propagations and 0 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00881749s
Runtime decision procedure: 0.0421911s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-4_1-thread_local_vars.i function ieee80211_register_hw
[nodatarace.assertion.0] line 1719 No data races on variable pdev between line 1699 and line 1699: SUCCESS
[nodatarace.assertion.1] line 1719 No data races on variable pdev between line 1699 and line 1700: SUCCESS
[nodatarace.assertion.2] line 1719 No data races on variable pdev between line 1700 and line 1699: SUCCESS
[nodatarace.assertion.3] line 1719 No data races on variable pdev between line 1759 and line 1699: SUCCESS
[nodatarace.assertion.4] line 1719 No data races on variable pdev between line 1759 and line 1700: SUCCESS
[nodatarace.assertion.5] line 1719 No data races on variable pdev between line 1760 and line 1699: SUCCESS
[nodatarace.assertion.6] line 1719 No data races on variable pdev between line 1771 and line 1699: SUCCESS
[nodatarace.assertion.7] line 1719 No data races on variable pdev between line 1771 and line 1700: SUCCESS
[nodatarace.assertion.8] line 1719 No data races on variable pdev between line 1772 and line 1699: SUCCESS
[nodatarace.assertion.9] line 1719 No data races on variable pdev between line 1792 and line 1699: SUCCESS
[nodatarace.assertion.10] line 1719 No data races on variable pdev between line 1792 and line 1700: SUCCESS
[nodatarace.assertion.11] line 1719 No data races on variable pdev between line 1792 and line 1759: SUCCESS
[nodatarace.assertion.12] line 1719 No data races on variable pdev between line 1792 and line 1760: SUCCESS
[nodatarace.assertion.13] line 1719 No data races on variable pdev between line 1792 and line 1771: SUCCESS
[nodatarace.assertion.14] line 1719 No data races on variable pdev between line 1792 and line 1772: SUCCESS
[nodatarace.assertion.15] line 1719 No data races on variable pdev between line 1793 and line 1699: SUCCESS
[nodatarace.assertion.16] line 1719 No data races on variable pdev between line 1793 and line 1759: SUCCESS
[nodatarace.assertion.17] line 1719 No data races on variable pdev between line 1793 and line 1771: SUCCESS

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