./run_relay.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-index-bitmask-race-3.i


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


duppy -c per-thread-index-bitmask-race-3.c
duppy'ing per-thread-index-bitmask-race-3.c to /mnt/goblint-svcomp/benchexec/tools-pldi/relay-sv/tmp.VXYbm0jGFf/ciltrees
gcc -D_GNUCC -E -DCIL=1 per-thread-index-bitmask-race-3.c -o /tmp/cil-KS4Yvqnd.i
../cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-1GUXEG6P.cil.c --doheapify_sep --heapify_locals --dotrans_alloc --domyptranal --dodumpfile /tmp/cil-KS4Yvqnd.i
Making cfg for assume_abort_if_not
Making cfg for thread
Making cfg for main
Trans_alloc: void  <> pthread_t 
Trans_alloc: void  <> int 
Trans_alloc: main per-thread-index-bitmask-race-3.c:1048
gcc -D_GNUCC -E /tmp/cil-1GUXEG6P.cil.c -o /tmp/cil-dNkqd3dD.cil.i
gcc -D_GNUCC -c -o ./per-thread-index-bitmask-race-3.o /tmp/cil-dNkqd3dD.cil.i
per-thread-index-bitmask-race-3.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-index-bitmask-race-3.c:1:1: note: ‘malloc’ is declared in header ‘<stdlib.h>’
  +++ |+#include <stdlib.h>
    1 | typedef unsigned int size_t;
per-thread-index-bitmask-race-3.c: In function ‘thread’:
per-thread-index-bitmask-race-3.c:1041:7: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
 1041 |   int j = (int)arg;
      |       ^
per-thread-index-bitmask-race-3.c: In function ‘main’:
per-thread-index-bitmask-race-3.c:1060:51: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
 1060 |   }
      |                                                   ^
per-thread-index-bitmask-race-3.c:1064:3: warning: ‘free’ called on unallocated object ‘_a1052_49613_per_1’ [-Wfree-nonheap-object]
 1064 |   free(tids);
      |   ^~~~~~~~~~~       
per-thread-index-bitmask-race-3.c:1048:11: note: declared here
 1048 | int main() {
      |           ^~                
Generating stats for steens
DONE!
Generating stats for cil
DONE!
Generating stats for anders
DONE!
Generating stats for noalias
DONE!
Dumped in 5 seconds
Mon Nov 13 09:58:03 UTC 2023
WARNING: tempfile is deprecated; consider using mktemp instead.
reserved status file: /tmp//temp.statusUtvky3
running analysis on ./tmp.VXYbm0jGFf/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.VXYbm0jGFf/ciltrees -r -u benchexec -st /tmp//temp.statusUtvky3 -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.statusUtvky3 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.VXYbm0jGFf/ciltrees/.pta_results.anders
Old PTA results loaded
Reached end of ./tmp.VXYbm0jGFf/ciltrees/calls.anders call graph file
Num funcs: 11
Scc_cg: Pruned 8 funcs w/out bodies for scc DAG
summary database will use:
	./tmp.VXYbm0jGFf/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:7.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:6.f
Initializing summary rs_scc
Fatal error: exception Not_found
BS: Not doing any post-reboot cleanup
Elapsed time (secs): 0.010273
Top heap size (MB): 0
Current heap size (MB): 0
Lifetime allocated bytes (MB): 3
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.statusUtvky3
Mon Nov 13 09:58:03 UTC 2023
