./run_relay.sh /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/libfaketime/main.c


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


duppy -c main.c
duppy'ing main.c to /mnt/goblint-svcomp/goblint-bench/the-continuous-race/tools/svcomp24/relay-sv/tmp.RtuNBVRgE5/ciltrees
gcc -D_GNUCC -E -DCIL=1 main.c -o /tmp/cil-ZjYzcY9L.i
../cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-6g3VyTZj.cil.c --doheapify_sep --heapify_locals --dotrans_alloc --domyptranal --dodumpfile /tmp/cil-ZjYzcY9L.i
Making cfg for handler
Making cfg for pthread_test
Making cfg for main
Trans_alloc: pthread_test main.c:319
Trans_alloc: main main.c:388
gcc -D_GNUCC -E /tmp/cil-6g3VyTZj.cil.c -o /tmp/cil-BYOA284C.cil.i
gcc -D_GNUCC -c -o ./main.o /tmp/cil-BYOA284C.cil.i
/tmp/cil-6g3VyTZj.cil.c:5:7: warning: conflicting types for built-in function ‘malloc’; expected ‘void *(long unsigned int)’ [-Wbuiltin-declaration-mismatch]
    5 | void *malloc(unsigned int  ) ;
      |       ^~~~~~
/tmp/cil-6g3VyTZj.cil.c:1:1: note: ‘malloc’ is declared in header ‘<stdlib.h>’
  +++ |+#include <stdlib.h>
    1 | /* Generated by CIL v. 1.3.7 */
main.c: In function ‘main’:
main.c:484:3: warning: ‘ftime’ is deprecated [-Wdeprecated-declarations]
  484 |   ftime(& tb);
      |   ^~~~~
main.c:277:46: note: declared here
  277 | extern int ( __attribute__((__nonnull__(1))) ftime)(struct timeb *__timebuf )  __attribute__((__deprecated__)) ;
      |                                              ^~~~~
main.c: In function ‘pthread_test’:
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_1’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~  
main.c:319:17: note: declared here
  319 | void *pthread_test(void *args )
      |                 ^~~~~~~~~~~~~~~   
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_2’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~         
main.c:319:17: note: declared here
  319 | void *pthread_test(void *args )
      |                 ^~~~~~~~~~~~~~~   
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_3’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~   
main.c:319:20: note: declared here
  319 | void *pthread_test(void *args )
      |                    ^~~~~~~~~~~~      
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_4’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~             
main.c:319:16: note: declared here
  319 | void *pthread_test(void *args )
      |                ^~~~~~~~~~~~~~~~  
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_5’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~       
main.c:319:16: note: declared here
  319 | void *pthread_test(void *args )
      |                ^~~~~~~~~~~~~~~~  
main.c:385:3: warning: ‘free’ called on unallocated object ‘_a319_11862_main_6’ [-Wfree-nonheap-object]
  385 |   return ((void *)0);
      |   ^~~~~~~~~~~~~~~~~~~        
main.c:319:17: note: declared here
  319 | void *pthread_test(void *args )
      |                 ^~~~~~~~~~~~~~~   
main.c: In function ‘main’:
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_1’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~           
main.c:388:7: note: declared here
  388 | int main(int argc , char **argv )
      |       ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_2’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~              
main.c:388:11: note: declared here
  388 | int main(int argc , char **argv )
      |           ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_3’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~           
main.c:388:13: note: declared here
  388 | int main(int argc , char **argv )
      |             ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_4’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~         
main.c:388:18: note: declared here
  388 | int main(int argc , char **argv )
      |                  ^~~~~~~~~~~~~~~~  
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_5’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~           
main.c:388:10: note: declared here
  388 | int main(int argc , char **argv )
      |          ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_6’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~          
main.c:388:19: note: declared here
  388 | int main(int argc , char **argv )
      |                   ^~~~~~~~~~~~~~~   
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_7’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~          
main.c:388:17: note: declared here
  388 | int main(int argc , char **argv )
      |                 ^~~~~~~~~~~~~~~~~ 
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_8’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~               
main.c:388:9: note: declared here
  388 | int main(int argc , char **argv )
      |         ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_9’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~               
main.c:388:9: note: declared here
  388 | int main(int argc , char **argv )
      |         ^~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_10’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~         
main.c:388:17: note: declared here
  388 | int main(int argc , char **argv )
      |                 ^~~~~~~~~~~~~~~~~  
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_11’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~         
main.c:388:16: note: declared here
  388 | int main(int argc , char **argv )
      |                ^~~~~~~~~~~~~~~~~~ 
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_12’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~         
main.c:388:14: note: declared here
  388 | int main(int argc , char **argv )
      |              ^~~~~~~~~~~~~~~~~~~
main.c:525:3: warning: ‘free’ called on unallocated object ‘_a388_14786_main_13’ [-Wfree-nonheap-object]
  525 |   return (0);
      |   ^~~~~~~~~~~          
main.c:388:8: note: declared here
  388 | int main(int argc , char **argv )
      |        ^~~~~~~~~~~~~~~~~~~
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:58 UTC 2024
WARNING: tempfile is deprecated; consider using mktemp instead.
reserved status file: /tmp//temp.statusX4qCDR
running analysis on ./tmp.RtuNBVRgE5/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.RtuNBVRgE5/ciltrees -r -u benchexec -st /tmp//temp.statusX4qCDR -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.statusX4qCDR 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.RtuNBVRgE5/ciltrees/.pta_results.anders
Old PTA results loaded
Reached end of ./tmp.RtuNBVRgE5/ciltrees/calls.anders call graph file
Num funcs: 33
Scc_cg: Pruned 30 funcs w/out bodies for scc DAG
summary database will use:
	./tmp.RtuNBVRgE5/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:23.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:22.f
Initializing summary rs_scc
BS: Not doing any post-reboot cleanup
SH: initEscapeable found (0, 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) #0
=================================
Summarizing function: handler : 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: handler:33.f
=======

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

SS Sum:
 |-> $SSBOT
SIZES: 33.f : 34
>>> PROGRESS 1/3 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: 1	misses: 1

Prev GAPostCache hits: 0	misses: 0

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

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

SS Sum:
 |-> Vval: 0
SIZES: 66.f : 94
>>> PROGRESS 2/3 SCCs DONE!

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

Prev GAPostCache hits: 0	misses: 0

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

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

SS Sum:
 |-> Vval: 0
SIZES: 43.f : 34
>>> PROGRESS 3/3 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: 26	misses: 5

doing symstate
Prev ldiffCache hits: 20	misses: 1

doing symstate
now checking thread roots: pthread_test(43.f), pthread_test(43.f)
done with pair, sending notification
checking a thread-creation pair
Prev ldiffCache hits: 20	misses: 1

doing symstate
now checking thread roots: pthread_test(66.f), main(66.f)
done with pair, sending notification
checking a thread-creation pair
now checking thread roots: main(66.f), main(66.f)
done with pair, sending notification
completed all thread pairs
Sorting races

Printing races



$$$$$$
Total Warnings: 0


Printing Alias assumptions used by warnings
-----


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

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