./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.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/pthread-ext/47_ticket_lock_hc_backoff_vs.i
Converting
Type-checking 47_ticket_lock_hc_backoff_vs
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 47_ticket_lock_hc_backoff_vs file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 409
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)
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
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 711 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 711 function main thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 0
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop thr1.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 0
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Not unwinding loop thr1.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 1
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thr1.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 1
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop thr1.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 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-abort> line 6 function abort thread 2
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 2
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thr1.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop thr1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i li[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:711:3)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:72:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:77:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:82:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:87:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:92:1)
[Warning][Race] Memory location t@47_ticket_lock_hc_backoff_vs.i:690:19 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:693:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:693:3)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:694:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:694:3)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:695:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:695:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:695:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:695:3)
[Warning][Race] Memory location s@47_ticket_lock_hc_backoff_vs.i:689:19 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:702:55)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:702:55)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:704:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:704:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:704:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:704:5)
[Warning][Race] Memory location c@47_ticket_lock_hc_backoff_vs.i:697:10 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:12)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:12)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:3)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:73)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i:703:73)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          3
	-------------------
	total:           3
ne 702 function thr1 thread 2
Not unwinding loop thr1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 702 function thr1 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop thr1.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/47_ticket_lock_hc_backoff_vs.i line 700 function thr1 thread 2
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/pthread-ext/47_ticket_lock_hc_backoff_vs.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 693 694 695 696 702 703 704 705 711 712 
The number of races before goblint filter: 216
The number of races after goblint filter: 180
Race categories: 4
	703(1) - 703(1) c:
		c#2 c#8
		c#2 c#9
		c#2 c#10
		c#2 c#11
		c#2 c#12
		c#2 c#13
		c#3 c#8
		c#3 c#10
		c#3 c#11
		c#3 c#13
		c#4 c#8
		c#4 c#9
		c#4 c#10
		c#4 c#11
		c#4 c#12
		c#4 c#13
		c#5 c#8
		c#5 c#9
		c#5 c#10
		c#5 c#11
		c#5 c#12
		c#5 c#13
		c#6 c#8
		c#6 c#10
		c#6 c#11
		c#6 c#13
		c#7 c#8
		c#7 c#9
		c#7 c#10
		c#7 c#11
		c#7 c#12
		c#7 c#13
		c#2 c#14
		c#2 c#15
		c#2 c#16
		c#2 c#17
		c#2 c#18
		c#2 c#19
		c#3 c#14
		c#3 c#16
		c#3 c#17
		c#3 c#19
		c#4 c#14
		c#4 c#15
		c#4 c#16
		c#4 c#17
		c#4 c#18
		c#4 c#19
		c#5 c#14
		c#5 c#15
		c#5 c#16
		c#5 c#17
		c#5 c#18
		c#5 c#19
		c#6 c#14
		c#6 c#16
		c#6 c#17
		c#6 c#19
		c#7 c#14
		c#7 c#15
		c#7 c#16
		c#7 c#17
		c#7 c#18
		c#7 c#19
		c#8 c#14
		c#8 c#15
		c#8 c#16
		c#8 c#17
		c#8 c#18
		c#8 c#19
		c#9 c#14
		c#9 c#16
		c#9 c#17
		c#9 c#19
		c#10 c#14
		c#10 c#15
		c#10 c#16
		c#10 c#17
		c#10 c#18
		c#10 c#19
		c#11 c#14
		c#11 c#15
		c#11 c#16
		c#11 c#17
		c#11 c#18
		c#11 c#19
		c#12 c#14
		c#12 c#16
		c#12 c#17
		c#12 c#19
		c#13 c#14
		c#13 c#15
		c#13 c#16
		c#13 c#17
		c#13 c#18
		c#13 c#19
	702(1) - 704(1) s:
		s#2 s#13
		s#2 s#17
		s#3 s#13
		s#3 s#17
		s#6 s#13
		s#6 s#17
		s#7 s#13
		s#7 s#17
		s#2 s#21
		s#2 s#25
		s#3 s#21
		s#3 s#25
		s#6 s#21
		s#6 s#25
		s#7 s#21
		s#7 s#25
		s#10 s#21
		s#10 s#25
		s#11 s#21
		s#11 s#25
		s#14 s#21
		s#14 s#25
		s#15 s#21
		s#15 s#25
	704(1) - 702(1) s:
		s#5 s#10
		s#5 s#11
		s#5 s#14
		s#5 s#15
		s#9 s#10
		s#9 s#11
		s#9 s#14
		s#9 s#15
		s#5 s#18
		s#5 s#19
		s#5 s#22
		s#5 s#23
		s#9 s#18
		s#9 s#19
		s#9 s#22
		s#9 s#23
		s#13 s#18
		s#13 s#19
		s#13 s#22
		s#13 s#23
		s#17 s#18
		s#17 s#19
		s#17 s#22
		s#17 s#23
	704(1) - 704(1) s:
		s#4 s#13
		s#4 s#17
		s#5 s#12
		s#5 s#13
		s#5 s#16
		s#5 s#17
		s#8 s#13
		s#8 s#17
		s#9 s#12
		s#9 s#13
		s#9 s#16
		s#9 s#17
		s#4 s#21
		s#4 s#25
		s#5 s#20
		s#5 s#21
		s#5 s#24
		s#5 s#25
		s#8 s#21
		s#8 s#25
		s#9 s#20
		s#9 s#21
		s#9 s#24
		s#9 s#25
		s#12 s#21
		s#12 s#25
		s#13 s#20
		s#13 s#21
		s#13 s#24
		s#13 s#25
		s#16 s#21
		s#16 s#25
		s#17 s#20
		s#17 s#21
		s#17 s#24
		s#17 s#25
Runtime Symex: 0.51531s
Unsupported __VERIFIER_atomic_* function!
