./run_relay.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race-4.i


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


duppy -c per-thread-array-join-counter-race-4.c
duppy'ing per-thread-array-join-counter-race-4.c to /mnt/goblint-svcomp/benchexec/tools-pldi/relay-sv/tmp.0wvVnsz341/ciltrees
gcc -D_GNUCC -E -DCIL=1 per-thread-array-join-counter-race-4.c -o /tmp/cil-ykuuUUQQ.i
../cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-m2qsNL5h.cil.c --doheapify_sep --heapify_locals --dotrans_alloc --domyptranal --dodumpfile /tmp/cil-ykuuUUQQ.i
Making cfg for assume_abort_if_not
Making cfg for thread
Making cfg for cleaner
Making cfg for main
Trans_alloc: void  <> pthread_t 
Trans_alloc: void  <> _Bool 
Trans_alloc: void  <> pthread_mutex_t 
Trans_alloc: main per-thread-array-join-counter-race-4.c:1044
gcc -D_GNUCC -E /tmp/cil-m2qsNL5h.cil.c -o /tmp/cil-0feBwdNf.cil.i
gcc -D_GNUCC -c -o ./per-thread-array-join-counter-race-4.o /tmp/cil-0feBwdNf.cil.i
per-thread-array-join-counter-race-4.c:424:43: warning: conflicting types for built-in function ‘malloc’; expected ‘void *(long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  424 | extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__))
      |                                           ^~~~~~
per-thread-array-join-counter-race-4.c:1:1: note: ‘malloc’ is declared in header ‘<stdlib.h>’
  +++ |+#include <stdlib.h>
    1 | typedef unsigned int size_t;
per-thread-array-join-counter-race-4.c:426:43: warning: conflicting types for built-in function ‘calloc’; expected ‘void *(long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  426 | extern void *calloc (size_t __nmemb, size_t __size)
      |                                           ^~~~~~
per-thread-array-join-counter-race-4.c:1:1: note: ‘calloc’ is declared in header ‘<stdlib.h>’
  +++ |+#include <stdlib.h>
    1 | typedef unsigned int size_t;
per-thread-array-join-counter-race-4.c: In function ‘thread’:
per-thread-array-join-counter-race-4.c:1021:7: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
 1021 |   int i = (int)arg;
      |       ^
per-thread-array-join-counter-race-4.c: In function ‘main’:
per-thread-array-join-counter-race-4.c:1056:51: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
 1056 |     pthread_mutex_lock(&threads_alive_mutex);
      |                                                   ^
per-thread-array-join-counter-race-4.c:1066:3: warning: ‘free’ called on unallocated object ‘_a1044_48228_per_1’ [-Wfree-nonheap-object]
 1066 |   return datas[0];
      |   ^~~~~~~~~~~~~~~~             
per-thread-array-join-counter-race-4.c:1044:11: note: declared here
 1044 | int main() {
      |           ^~                
Generating stats for steens
DONE!
Generating stats for cil
DONE!
Generating stats for anders
DONE!
Generating stats for noalias
DONE!
Dumped in 4 seconds
Mon Nov 13 09:57:40 UTC 2023
WARNING: tempfile is deprecated; consider using mktemp instead.
reserved status file: /tmp//temp.statusYaqAB1
running analysis on ./tmp.0wvVnsz341/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.0wvVnsz341/ciltrees -r -u benchexec -st /tmp//temp.statusYaqAB1 -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.statusYaqAB1 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.0wvVnsz341/ciltrees/.pta_results.anders
Old PTA results loaded
Reached end of ./tmp.0wvVnsz341/ciltrees/calls.anders call graph file
Num funcs: 14
Scc_cg: Pruned 10 funcs w/out bodies for scc DAG
summary database will use:
	./tmp.0wvVnsz341/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:9.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:8.f
Initializing summary rs_scc
BS: Not doing any post-reboot cleanup
SH: initEscapeable found (1, 2) 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) #1
=================================
Summarizing function: assume_abort_if_not : per-thread-array-join-counter-race-4.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: assume_abort_if_not:12.f
=======

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

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

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #0
=================================
Summarizing function: main : per-thread-array-join-counter-race-4.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: main:32.f
=======

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

SS Sum:
 |-> $SSTOP
SIZES: 32.f : 34
>>> PROGRESS 2/4 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #2
=================================
Summarizing function: cleaner : per-thread-array-join-counter-race-4.c
-----
doing symstate
Prev ldiffCache hits: 8	misses: 5

Prev GAPostCache hits: 0	misses: 0

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

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

SS Sum:
 |-> Vval: 0
SIZES: 25.f : 91
>>> PROGRESS 3/4 SCCs DONE!

=================================
getting next SCC from server
Acquiring needed summaries
=================================
Starting an SCC (1) #3
=================================
Summarizing function: thread : per-thread-array-join-counter-race-4.c
-----
doing symstate
Prev ldiffCache hits: 0	misses: 6

Prev GAPostCache hits: 0	misses: 0

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

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

SS Sum:
 |-> Vval: 0
SIZES: 22.f : 34
>>> PROGRESS 4/4 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: 2

doing symstate
Prev ldiffCache hits: 8	misses: 3

doing symstate
now checking thread roots: thread(22.f), thread(22.f)
now checking thread roots: thread(25.f), cleaner(25.f)
now checking thread roots: cleaner(22.f), thread(22.f)
now checking thread roots: cleaner(25.f), cleaner(25.f)
done with pair, sending notification
checking a thread-creation pair
Prev ldiffCache hits: 8	misses: 3

doing symstate
now checking thread roots: thread(32.f), main(32.f)
New race added to race reports
New race added to race reports
New race added to race reports
now checking thread roots: cleaner(32.f), main(32.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
done with pair, sending notification
checking a thread-creation pair
now checking thread roots: main(32.f), main(32.f)
done with pair, sending notification
completed all thread pairs
Sorting races

Printing races

****
Possible race between access to:

datas_mutex @ per-thread-array-join-counter-race-4.c:1019 and
datas_mutex @ per-thread-array-join-counter-race-4.c:1019
	Cluster ID: 2
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1024:(22.f)] and
	[per-thread-array-join-counter-race-4.c:1049:(32.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = {[REP: 11]#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1055 48729 w/ func: thread
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

datas_mutex @ per-thread-array-join-counter-race-4.c:1019 and
datas_mutex @ per-thread-array-join-counter-race-4.c:1019
	Cluster ID: 6
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1039:(25.f)] and
	[per-thread-array-join-counter-race-4.c:1049:(32.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = {[REP: 11]#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1053 48615 w/ func: cleaner
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

threads_total @ per-thread-array-join-counter-race-4.c:1013 and
threads_total @ per-thread-array-join-counter-race-4.c:1013
	Cluster ID: 4
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1029:(25.f)] and
	[per-thread-array-join-counter-race-4.c:1045:(32.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1053 48615 w/ func: cleaner
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

datas_mutex @ per-thread-array-join-counter-race-4.c:1019 and
datas_mutex @ per-thread-array-join-counter-race-4.c:1019
	Cluster ID: 1
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1022:(22.f)] and
	[per-thread-array-join-counter-race-4.c:1049:(32.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1055 48729 w/ func: thread
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

datas_mutex @ per-thread-array-join-counter-race-4.c:1019 and
datas_mutex @ per-thread-array-join-counter-race-4.c:1019
	Cluster ID: 5
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1030:(25.f)] and
	[per-thread-array-join-counter-race-4.c:1049:(32.f)]

	Confidence: Syntactic

LS for 1st access:
L+ = empty;
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1053 48615 w/ func: cleaner
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 9] and
[REP: 9]
	Cluster ID: 0
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1023:(22.f)] and
	[per-thread-array-join-counter-race-4.c:1066:(32.f)]

	Confidence: used PTA nodes lblSet(1, 1)

LS for 1st access:
L+ = {[REP: 11]#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1055 48729 w/ func: thread
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):

****
Possible race between access to:

[REP: 9] and
[REP: 9]
	Cluster ID: 3
	Escapes? true / true 
	Accessed at locs:
	[per-thread-array-join-counter-race-4.c:1037:(25.f)] and
	[per-thread-array-join-counter-race-4.c:1066:(32.f)]

	Confidence: used PTA nodes lblSet(1, 1)

LS for 1st access:
L+ = {[REP: 11]#g} (1)
	(rep. lock)
LS for 2nd access:
L+ = empty;
	Th. 1 spawned: per-thread-array-join-counter-race-4.c:1053 48615 w/ func: cleaner
	Th. 2 spawned: #entry_point:0 0 w/ func: main

Different possible paths & LS (first 4):



$$$$$$
Total Warnings: 7


Printing Alias assumptions used by warnings
-----
nc	0	[REP: 9]#g/[REP: 9]#g	1	1
nc	3	[REP: 9]#g/[REP: 9]#g	1	1


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

writeState: Not needed for Steens PTA
Elapsed time (secs): 0.025186
Top heap size (MB): 0
Current heap size (MB): 0
Lifetime allocated bytes (MB): 5
Collections -- minor: 11 major: 2 compactions: 0
Bytes per word: 8
Exhausted tries: 1
return value is 0
ran 1 times
cleared status file: /tmp//temp.statusYaqAB1
Mon Nov 13 09:57:43 UTC 2023
server.exe: no process found
