./run_relay.sh /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/C-Thread-Pool/main.c


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


duppy -c main.c
duppy'ing main.c to /mnt/goblint-svcomp/goblint-bench/the-continuous-race/tools/svcomp24/relay-sv/tmp.a43DBISliD/ciltrees
gcc -D_GNUCC -E -DCIL=1 main.c -o /tmp/cil-faxOoT9r.i
../cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-445N4uZX.cil.c --doheapify_sep --heapify_locals --dotrans_alloc --domyptranal --dodumpfile /tmp/cil-faxOoT9r.i
Making cfg for thpool_init
Making cfg for thpool_add_work
Making cfg for thpool_wait
Making cfg for thpool_destroy
Making cfg for thpool_pause
Making cfg for thpool_resume
Making cfg for thpool_num_threads_working
Making cfg for thread_init
Making cfg for thread_hold
Making cfg for thread_do
Making cfg for thread_destroy
Making cfg for jobqueue_init
Making cfg for jobqueue_clear
Making cfg for jobqueue_push
Making cfg for jobqueue_pull
Making cfg for jobqueue_destroy
Making cfg for bsem_init
Making cfg for bsem_reset
Making cfg for bsem_post
Making cfg for bsem_post_all
Making cfg for bsem_wait
Making cfg for task
Making cfg for main
Trans_alloc: void  <> struct thpool_ 
Trans_alloc: void  <> struct thread *
Trans_alloc: thpool_init main.c:295
Trans_alloc: void  <> struct job 
Trans_alloc: thpool_add_work main.c:345
Trans_alloc: thpool_destroy main.c:382
Trans_alloc: void  <> struct thread 
Trans_alloc: thread_init main.c:457
Trans_alloc: thread_do main.c:488
Trans_alloc: void  <> struct bsem 
Trans_alloc: jobqueue_init main.c:558
gcc -D_GNUCC -E /tmp/cil-445N4uZX.cil.c -o /tmp/cil-4aUqnUxc.cil.i
gcc -D_GNUCC -c -o ./main.o /tmp/cil-4aUqnUxc.cil.i
main.c: In function ‘task’:
main.c:724:77: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
  724 |   printf((char const   * __restrict  )"Thread #%u working on %d\n", (int )tmp, (int )arg);
      |                                                                             ^
main.c: In function ‘thpool_init’:
main.c:320:5: warning: ‘free’ called on unallocated object ‘_a309_11211_main_1’ [-Wfree-nonheap-object]
  320 |     free((void *)thpool_p);
      |     ^~~~~~~~~~~~~~~~~~~~~~
main.c:295:16: note: declared here
  295 | struct thpool_ *thpool_init(int num_threads )
      |                ^~~~~~~~~~~~~~~~~~
main.c:328:5: warning: ‘free’ called on unallocated object ‘_a309_11211_main_1’ [-Wfree-nonheap-object]
  328 |     free((void *)thpool_p);
      |     ^~~~~~~~~~~~~~~~~~~~~~
main.c:295:16: note: declared here
  295 | struct thpool_ *thpool_init(int num_threads )
      |                ^~~~~~~~~~~~~~~~~~
main.c: In function ‘thpool_destroy’:
main.c:393:5: warning: ‘free’ called on unallocated object ‘_a382_13785_main_1’ [-Wfree-nonheap-object]
  393 |     return;
      |     ^~~~~~~              
main.c:382:8: note: declared here
  382 | void thpool_destroy(struct thpool_ *thpool_p )
      |        ^~~~~~~~~~~~~~~~~~
main.c:393:5: warning: ‘free’ called on unallocated object ‘_a382_13785_main_2’ [-Wfree-nonheap-object]
  393 |     return;
      |     ^~~~~~~                
main.c:382:8: note: declared here
  382 | void thpool_destroy(struct thpool_ *thpool_p )
      |        ^~~~~~~~~~~~~~~~~~
main.c:424:3: warning: ‘free’ called on unallocated object ‘_a382_13785_main_1’ [-Wfree-nonheap-object]
  424 |   return;
      |   ^~~~~~~              
main.c:382:8: note: declared here
  382 | void thpool_destroy(struct thpool_ *thpool_p )
      |        ^~~~~~~~~~~~~~~~~~
main.c:424:3: warning: ‘free’ called on unallocated object ‘_a382_13785_main_2’ [-Wfree-nonheap-object]
  424 |   return;
      |   ^~~~~~~                
main.c:382:8: note: declared here
  382 | void thpool_destroy(struct thpool_ *thpool_p )
      |        ^~~~~~~~~~~~~~~~~~
main.c: In function ‘thread_do’:
main.c:546:3: warning: ‘free’ called on unallocated object ‘_a488_16026_main_1’ [-Wfree-nonheap-object]
  546 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~  
main.c:488:18: note: declared here
  488 | static void *thread_do(struct thread *thread_p )
      |                  ^~~~~~~~~~~~~~~~~~
main.c:546:3: warning: ‘free’ called on unallocated object ‘_a488_16026_main_2’ [-Wfree-nonheap-object]
  546 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~          
main.c:488:6: note: declared here
  488 | static void *thread_do(struct thread *thread_p )
      |      ^~~~~~~~~~~~~~~~~~
Generating stats for steens
DONE!
Generating stats for cil
DONE!
Generating stats for anders
DONE!
Generating stats for noalias
DONE!
Dumped in 4 seconds
Sun Mar 17 16:39:13 UTC 2024
WARNING: tempfile is deprecated; consider using mktemp instead.
reserved status file: /tmp//temp.statusOMbSU4
running analysis on ./tmp.a43DBISliD/ciltrees
Registered summary type: rs_scc
Registered summary type: rs
Registered summary type: ss
Registered summary type: rad_ss
Args: 
 ./race_anal.exe -cg ./tmp.a43DBISliD/ciltrees -r -u benchexec -st /tmp//temp.statusOMbSU4 -su client.cfg
Checking for data races
-----
Loading Cil Varinfo ID ranges for lookup tables
Loading ranges from .vids_ckeys_fixed
Setting Cil Varinfo ID ranges
Finished parsing config group: SUMMARY_DB
Finished parsing config group: REQUEST
Finished parsing config group: DISTRIBUTED
Finished parsing config group: FILE_SERVER
Finished parsing config group: LOCK_FUNCS
Finished parsing config group: THREAD_FUNCS
Finished parsing config group: EXIT_FUNCS
Finished parsing config group: BUILTIN_FUNCS
Finished parsing config group: ALIAS_ANALYSIS
Finished parsing config group: ENTRY_POINTS
Finished parsing config group: SYM_EX
Done reading config file
myIP: 127.0.0.1
using /tmp/relay_scratch to store acquired files
using: /tmp//temp.statusOMbSU4 to track status
Initializing Steensgaard AA info
Loading function info
Loading tempVar info
Using old PTA results
Old PTA results loaded
Initializing Andersen's AA info
Using old PTA results: ./tmp.a43DBISliD/ciltrees/.pta_results.anders
Old PTA results loaded
Reached end of ./tmp.a43DBISliD/ciltrees/calls.anders call graph file
Num funcs: 46
Scc_cg: Pruned 23 funcs w/out bodies for scc DAG
summary database will use:
	./tmp.a43DBISliD/ciltrees/relay_sums
Initializing summary rad_ss
Checking leftover state: rad_ss
[Er]: Checkpoint: No left-over status file
Initializing summary ss
Checking leftover state: ss
[Er]: Checkpoint: No left-over status file
Initializing summary rs
BS: Not doing any post-reboot cleanup
[Er]: Multiple lock summaries for pthread_mutex_unlock:17.f
[Er]: makeSimpleLock: Couldn't find global kernel_sem
[Er]: makeSimpleLock: Couldn't find global kernel_flag
[Er]: Multiple lock summaries for pthread_mutex_lock:16.f
Initializing summary rs_scc
BS: Not doing any post-reboot cleanup
SH: initEscapeable found (1, 1) thread (acts, formals)

Entry points use roots: true
file server will use: 14440
[Er]: Request fault handler with Connection refused
[Er]: Request retrying
[Er]: retry succeeded!

trying to clear old summaries / local srcs, etc.
Starting bottomup analysis
-----
[Er]: Checkpoint: No left-over status file
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #4
=================================
Summarizing function: bsem_wait : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 0

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: bsem_wait:45.f
=======

SUMS (nm, lo, un, wr, re):	bsem_wait	0	0	1	1	

SS Sum:
 |-> $SSBOT
SIZES: 45.f : 234
>>> PROGRESS 1/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #5
=================================
Summarizing function: task : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 3

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: task:113.f
=======

SUMS (nm, lo, un, wr, re):	task	0	0	0	0	

SS Sum:
 |-> $SSBOT
SIZES: 113.f : 34
>>> PROGRESS 2/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #18
=================================
Summarizing function: bsem_post : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 2

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: bsem_post:43.f
=======

SUMS (nm, lo, un, wr, re):	bsem_post	0	0	1	0	

SS Sum:
 |-> $SSBOT
SIZES: 43.f : 205
>>> PROGRESS 3/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #17
=================================
Summarizing function: jobqueue_pull : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 3

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: jobqueue_pull:39.f
=======

SUMS (nm, lo, un, wr, re):	jobqueue_pull	0	0	4	4	

SS Sum:
 |-> $SSTOP
SIZES: 39.f : 675
>>> PROGRESS 4/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #0
=================================
Summarizing function: thread_do : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 4

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thread_do:33.f
=======

SUMS (nm, lo, un, wr, re):	thread_do	0	0	9	13	

SS Sum:
 |-> Vval: 0
SIZES: 33.f : 182
>>> PROGRESS 5/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #7
=================================
Summarizing function: bsem_post_all : main.c
-----
doing symstate
Prev ldiffCache hits: 22	misses: 8

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: bsem_post_all:44.f
=======

SUMS (nm, lo, un, wr, re):	bsem_post_all	0	0	1	0	

SS Sum:
 |-> $SSBOT
SIZES: 44.f : 205
>>> PROGRESS 6/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #20
=================================
Summarizing function: bsem_init : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 3

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: bsem_init:41.f
=======

SUMS (nm, lo, un, wr, re):	bsem_init	0	0	1	1	

SS Sum:
 |-> $SSBOT
SIZES: 41.f : 105
>>> PROGRESS 7/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #16
=================================
Summarizing function: bsem_reset : main.c
-----
doing symstate
Prev ldiffCache hits: 4	misses: 2

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: bsem_reset:42.f
=======

SUMS (nm, lo, un, wr, re):	bsem_reset	0	0	1	1	

SS Sum:
 |-> $SSBOT
SIZES: 42.f : 105
>>> PROGRESS 8/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #15
=================================
Summarizing function: jobqueue_clear : main.c
-----
doing symstate
Prev ldiffCache hits: 2	misses: 1

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: jobqueue_clear:37.f
=======

SUMS (nm, lo, un, wr, re):	jobqueue_clear	0	0	4	5	

SS Sum:
 |-> $SSBOT
SIZES: 37.f : 820
>>> PROGRESS 9/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #13
=================================
Summarizing function: jobqueue_destroy : main.c
-----
doing symstate
Prev ldiffCache hits: 9	misses: 4

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: jobqueue_destroy:40.f
=======

SUMS (nm, lo, un, wr, re):	jobqueue_destroy	0	0	4	5	

SS Sum:
 |-> $SSBOT
SIZES: 40.f : 843
>>> PROGRESS 10/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #21
=================================
Summarizing function: thread_destroy : main.c
-----
doing symstate
Prev ldiffCache hits: 13	misses: 4

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thread_destroy:35.f
=======

SUMS (nm, lo, un, wr, re):	thread_destroy	0	0	0	0	

SS Sum:
 |-> $SSBOT
SIZES: 35.f : 34
>>> PROGRESS 11/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #3
=================================
Summarizing function: thpool_destroy : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 1

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_destroy:28.f
=======

SUMS (nm, lo, un, wr, re):	thpool_destroy	0	0	5	10	

SS Sum:
 |-> $SSBOT
SIZES: 28.f : 1170
>>> PROGRESS 12/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #9
=================================
Summarizing function: thpool_wait : main.c
-----
doing symstate
Prev ldiffCache hits: 26	misses: 5

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_wait:25.f
=======

SUMS (nm, lo, un, wr, re):	thpool_wait	0	0	0	2	

SS Sum:
 |-> $SSBOT
SIZES: 25.f : 345
>>> PROGRESS 13/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #14
=================================
Summarizing function: jobqueue_push : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 3

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: jobqueue_push:38.f
=======

SUMS (nm, lo, un, wr, re):	jobqueue_push	0	0	6	2	

SS Sum:
 |-> $SSBOT
SIZES: 38.f : 666
>>> PROGRESS 14/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #10
=================================
Summarizing function: thpool_add_work : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 4

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_add_work:24.f
=======

SUMS (nm, lo, un, wr, re):	thpool_add_work	0	0	8	3	

SS Sum:
 |-> $SSTOP
SIZES: 24.f : 725
>>> PROGRESS 15/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #12
=================================
Summarizing function: thread_init : main.c
-----
doing symstate
Prev ldiffCache hits: 7	misses: 3

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thread_init:32.f
=======

SUMS (nm, lo, un, wr, re):	thread_init	0	0	3	3	

SS Sum:
 |-> $SSTOP
SIZES: 32.f : 122
>>> PROGRESS 16/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #19
=================================
Summarizing function: jobqueue_init : main.c
-----
doing symstate
Prev ldiffCache hits: 1	misses: 2

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: jobqueue_init:36.f
=======

SUMS (nm, lo, un, wr, re):	jobqueue_init	0	0	5	2	

SS Sum:
 |-> $SSTOP
SIZES: 36.f : 363
>>> PROGRESS 17/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #11
=================================
Summarizing function: thpool_init : main.c
-----
doing symstate
Prev ldiffCache hits: 2	misses: 2

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_init:23.f
=======

SUMS (nm, lo, un, wr, re):	thpool_init	0	0	13	9	

SS Sum:
 |-> Mayptr (0):   lv = _a309_11211_main_1
              lv = (*$NULL)(sum)

SIZES: 23.f : 34
>>> PROGRESS 18/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #1
=================================
Summarizing function: main : main.c
-----
doing symstate
Prev ldiffCache hits: 34	misses: 4

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: main:116.f
=======

SUMS (nm, lo, un, wr, re):	main	0	0	17	12	

SS Sum:
 |-> Vval: 0
SIZES: 116.f : 34
>>> PROGRESS 19/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #2
=================================
Summarizing function: thpool_num_threads_working : main.c
-----
doing symstate
Prev ldiffCache hits: 60	misses: 10

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_num_threads_working:29.f
=======

SUMS (nm, lo, un, wr, re):	thpool_num_threads_working	0	0	0	1	

SS Sum:
 |-> Vval: thpool_p->num_threads_working
SIZES: 29.f : 138
>>> PROGRESS 20/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #6
=================================
Summarizing function: thpool_resume : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 0

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_resume:27.f
=======

SUMS (nm, lo, un, wr, re):	thpool_resume	0	0	1	0	

SS Sum:
 |-> $SSBOT
SIZES: 27.f : 34
>>> PROGRESS 21/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #8
=================================
Summarizing function: thpool_pause : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 0

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thpool_pause:26.f
=======

SUMS (nm, lo, un, wr, re):	thpool_pause	0	0	0	2	

SS Sum:
 |-> $SSBOT
SIZES: 26.f : 269
>>> PROGRESS 22/23 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #22
=================================
Summarizing function: thread_hold : main.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 1

Prev GAPostCache hits: 0	misses: 0

doing lockset
doing guarded access
=================================
Finished an SCC (1)
=================================
Summary for function: thread_hold:34.f
=======

SUMS (nm, lo, un, wr, re):	thread_hold	0	0	1	1	

SS Sum:
 |-> $SSBOT
SIZES: 34.f : 34
>>> PROGRESS 23/23 SCCs DONE!

=================================
getting next SCC from server
Bottomup analysis complete
-----



Beginning Thread Analysis:
-----
[Er]: No entry-points file!
Expected # thread-creation site pairs: 3
checking a thread-creation pair
Prev ldiffCache hits: 0	misses: 1

doing symstate
Prev ldiffCache hits: 19	misses: 5

doing symstate
now checking thread roots: thread_do(33.f), thread_do(33.f)
done with pair, sending notification
checking a thread-creation pair
Prev ldiffCache hits: 19	misses: 5

doing symstate
now checking thread roots: thread_do(116.f), main(116.f)
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
New race added to race reports
done with pair, sending notification
checking a thread-creation pair
now checking thread roots: main(116.f), main(116.f)
done with pair, sending notification
completed all thread pairs
Sorting races

Printing races

****
Possible race between access to:

threads_keepalive @ main.c:279 and
threads_keepalive @ main.c:279
	Cluster ID: 15
	Escapes? true / true 
	Accessed at locs:
	[main.c:521:(33.f), main.c:523:(33.f)] and
	[main.c:305:(23.f), main.c:396:(28.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.front and
_a309_11211_main_1.jobqueue.front @ main.c:295
	Cluster ID: 19
	Escapes? true / true 
	Accessed at locs:
	[main.c:620:(39.f)] and
	[main.c:564:(36.f), main.c:585:(37.f), main.c:601:(38.f), main.c:625:(39.f), main.c:630:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.front and
_a309_11211_main_1.jobqueue.front @ main.c:295
	Cluster ID: 0
	Escapes? true / true 
	Accessed at locs:
	[main.c:625:(39.f), main.c:630:(39.f)] and
	[main.c:564:(36.f), main.c:585:(37.f), main.c:601:(38.f), main.c:625:(39.f), main.c:630:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.front and
_a309_11211_main_1.jobqueue.front @ main.c:295
	Cluster ID: 10
	Escapes? true / true 
	Accessed at locs:
	[main.c:620:(39.f)] and
	[main.c:625:(39.f), main.c:630:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = {_a309_11211_main_1.jobqueue.rwmutex#g:46} (1)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

(0)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main
(1)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main
****
Possible race between access to:

[REP: 1].jobqueue.front and
_a309_11211_main_1.jobqueue.front @ main.c:295
	Cluster ID: 1
	Escapes? true / true 
	Accessed at locs:
	[main.c:625:(39.f), main.c:630:(39.f)] and
	[main.c:625:(39.f), main.c:630:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = {_a309_11211_main_1.jobqueue.rwmutex#g:46} (1)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.has_jobs and
_a309_11211_main_1.jobqueue.has_jobs @ main.c:295
	Cluster ID: 21
	Escapes? true / true 
	Accessed at locs:
	[main.c:632:(39.f)] and
	[main.c:567:(36.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.len and
_a309_11211_main_1.jobqueue.len @ main.c:295
	Cluster ID: 22
	Escapes? true / true 
	Accessed at locs:
	[main.c:622:(39.f), main.c:624:(39.f), main.c:631:(39.f)] and
	[main.c:563:(36.f), main.c:588:(37.f), main.c:608:(38.f), main.c:627:(39.f), main.c:631:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.len and
_a309_11211_main_1.jobqueue.len @ main.c:295
	Cluster ID: 11
	Escapes? true / true 
	Accessed at locs:
	[main.c:627:(39.f), main.c:631:(39.f)] and
	[main.c:370:(25.f), main.c:581:(37.f), main.c:600:(38.f), main.c:608:(38.f), main.c:622:(39.f), main.c:624:(39.f), main.c:631:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.len and
_a309_11211_main_1.jobqueue.len @ main.c:295
	Cluster ID: 2
	Escapes? true / true 
	Accessed at locs:
	[main.c:627:(39.f), main.c:631:(39.f)] and
	[main.c:563:(36.f), main.c:588:(37.f), main.c:608:(38.f), main.c:627:(39.f), main.c:631:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.len and
_a309_11211_main_1.jobqueue.len @ main.c:295
	Cluster ID: 12
	Escapes? true / true 
	Accessed at locs:
	[main.c:622:(39.f), main.c:624:(39.f), main.c:631:(39.f)] and
	[main.c:627:(39.f), main.c:631:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = {_a309_11211_main_1.jobqueue.rwmutex#g:46} (1)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

(0)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main
****
Possible race between access to:

[REP: 1].jobqueue.len and
_a309_11211_main_1.jobqueue.len @ main.c:295
	Cluster ID: 3
	Escapes? true / true 
	Accessed at locs:
	[main.c:627:(39.f), main.c:631:(39.f)] and
	[main.c:627:(39.f), main.c:631:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = {_a309_11211_main_1.jobqueue.rwmutex#g:46} (1)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.rear and
_a309_11211_main_1.jobqueue.rear @ main.c:295
	Cluster ID: 4
	Escapes? true / true 
	Accessed at locs:
	[main.c:626:(39.f)] and
	[main.c:565:(36.f), main.c:586:(37.f), main.c:602:(38.f), main.c:606:(38.f), main.c:626:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.rear and
_a309_11211_main_1.jobqueue.rear @ main.c:295
	Cluster ID: 5
	Escapes? true / true 
	Accessed at locs:
	[main.c:626:(39.f)] and
	[main.c:626:(39.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = {_a309_11211_main_1.jobqueue.rwmutex#g:46} (1)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].num_threads_alive and
_a309_11211_main_1.num_threads_alive @ main.c:295
	Cluster ID: 6
	Escapes? true / true 
	Accessed at locs:
	[main.c:519:(33.f), main.c:544:(33.f)] and
	[main.c:315:(23.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].thcount_lock#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].num_threads_alive and
_a309_11211_main_1.num_threads_alive @ main.c:295
	Cluster ID: 13
	Escapes? true / true 
	Accessed at locs:
	[main.c:519:(33.f), main.c:544:(33.f)] and
	[main.c:339:(23.f), main.c:395:(28.f), main.c:402:(28.f), main.c:412:(28.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].thcount_lock#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].num_threads_working and
_a309_11211_main_1.num_threads_working @ main.c:295
	Cluster ID: 7
	Escapes? true / true 
	Accessed at locs:
	[main.c:525:(33.f), main.c:536:(33.f), main.c:537:(33.f)] and
	[main.c:316:(23.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].thcount_lock#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

(0)
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main
****
Possible race between access to:

[REP: 1].num_threads_working and
_a309_11211_main_1.num_threads_working @ main.c:295
	Cluster ID: 14
	Escapes? true / true 
	Accessed at locs:
	[main.c:525:(33.f), main.c:536:(33.f)] and
	[main.c:371:(25.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].thcount_lock#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].prev and
_a351_12928_main_1.prev @ main.c:345
	Cluster ID: 23
	Escapes? true / true 
	Accessed at locs:
	[main.c:630:(39.f)] and
	[main.c:598:(38.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].prev and
[REP: 1].prev
	Cluster ID: 24
	Escapes? true / true 
	Accessed at locs:
	[main.c:630:(39.f)] and
	[main.c:605:(38.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].v and
[REP: 1].v
	Cluster ID: 8
	Escapes? true / true 
	Accessed at locs:
	[main.c:682:(43.f)] and
	[main.c:663:(41.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].jobqueue.rwmutex#g, [REP: 1].mutex#g} (2)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].v and
[REP: 1].v
	Cluster ID: 26
	Escapes? true / true 
	Accessed at locs:
	[main.c:706:(45.f)] and
	[main.c:663:(41.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].mutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].v and
[REP: 1].v
	Cluster ID: 9
	Escapes? true / true 
	Accessed at locs:
	[main.c:709:(45.f)] and
	[main.c:663:(41.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = {[REP: 1].mutex#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].arg and
_a351_12928_main_1.arg @ main.c:345
	Cluster ID: 16
	Escapes? true / true 
	Accessed at locs:
	[main.c:531:(33.f)] and
	[main.c:358:(24.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].function and
_a351_12928_main_1.function @ main.c:345
	Cluster ID: 17
	Escapes? true / true 
	Accessed at locs:
	[main.c:530:(33.f)] and
	[main.c:357:(24.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].id and
[REP: 1].id
	Cluster ID: 18
	Escapes? true / true 
	Accessed at locs:
	[main.c:507:(33.f)] and
	[main.c:469:(32.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].jobqueue.has_jobs and
_a309_11211_main_1.jobqueue.has_jobs @ main.c:295
	Cluster ID: 20
	Escapes? true / true 
	Accessed at locs:
	[main.c:522:(33.f)] and
	[main.c:567:(36.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 1].thpool_p and
[REP: 1].thpool_p
	Cluster ID: 25
	Escapes? true / true 
	Accessed at locs:
	[main.c:510:(33.f)] and
	[main.c:468:(32.f)]

	Confidence: used PTA nodes lblSet(6, 6)

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: main.c:470 15625 w/ func: thread_do
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):



$$$$$$
Total Warnings: 27


Printing Alias assumptions used by warnings
-----
nc	19	[REP: 1].jobqueue.front#g/_a309_11211_main_1.jobqueue.front#g:46	6	6
nc	0	[REP: 1].jobqueue.front#g/_a309_11211_main_1.jobqueue.front#g:46	6	6
nc	10	[REP: 1].jobqueue.front#g/_a309_11211_main_1.jobqueue.front#g:46	6	6
nc	1	[REP: 1].jobqueue.front#g/_a309_11211_main_1.jobqueue.front#g:46	6	6
nc	21	[REP: 1].jobqueue.has_jobs#g/_a309_11211_main_1.jobqueue.has_jobs#g:46	6	6
nc	22	[REP: 1].jobqueue.len#g/_a309_11211_main_1.jobqueue.len#g:46	6	6
nc	11	[REP: 1].jobqueue.len#g/_a309_11211_main_1.jobqueue.len#g:46	6	6
nc	2	[REP: 1].jobqueue.len#g/_a309_11211_main_1.jobqueue.len#g:46	6	6
nc	12	[REP: 1].jobqueue.len#g/_a309_11211_main_1.jobqueue.len#g:46	6	6
nc	3	[REP: 1].jobqueue.len#g/_a309_11211_main_1.jobqueue.len#g:46	6	6
nc	4	[REP: 1].jobqueue.rear#g/_a309_11211_main_1.jobqueue.rear#g:46	6	6
nc	5	[REP: 1].jobqueue.rear#g/_a309_11211_main_1.jobqueue.rear#g:46	6	6
nc	6	[REP: 1].num_threads_alive#g/_a309_11211_main_1.num_threads_alive#g:46	6	6
nc	13	[REP: 1].num_threads_alive#g/_a309_11211_main_1.num_threads_alive#g:46	6	6
nc	7	[REP: 1].num_threads_working#g/_a309_11211_main_1.num_threads_working#g:46	6	6
nc	14	[REP: 1].num_threads_working#g/_a309_11211_main_1.num_threads_working#g:46	6	6
nc	23	[REP: 1].prev#g/_a351_12928_main_1.prev#g:54	6	6
nc	24	[REP: 1].prev#g/[REP: 1].prev#g	6	6
nc	8	[REP: 1].v#g/[REP: 1].v#g	6	6
nc	26	[REP: 1].v#g/[REP: 1].v#g	6	6
nc	9	[REP: 1].v#g/[REP: 1].v#g	6	6
nc	16	[REP: 1].arg#g/_a351_12928_main_1.arg#g:54	6	6
nc	17	[REP: 1].function#g/_a351_12928_main_1.function#g:54	6	6
nc	18	[REP: 1].id#g/[REP: 1].id#g	6	6
nc	20	[REP: 1].jobqueue.has_jobs#g/_a309_11211_main_1.jobqueue.has_jobs#g:46	6	6
nc	25	[REP: 1].thpool_p#g/[REP: 1].thpool_p#g	6	6


writeState: writing new state for Andersen to ./tmp.a43DBISliD/ciltrees/.pta_temp.anders

writeState: Not needed for Steens PTA
Elapsed time (secs): 0.047547
Top heap size (MB): 1
Current heap size (MB): 1
Lifetime allocated bytes (MB): 13
Collections -- minor: 13 major: 3 compactions: 0
Bytes per word: 8
Exhausted tries: 1
return value is 0
ran 1 times
cleared status file: /tmp//temp.statusOMbSU4
Sun Mar 17 16:39:16 UTC 2024
server.exe: no process found
