./sv-sanitizers.py -j 4 --property /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp --data-model ILP32 /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i


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


/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:424:14: 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__))
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1: note: ‘malloc’ is declared in header ‘<stdlib.h>’
    1 | typedef unsigned int size_t;
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:426:14: 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)
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:426:14: note: ‘calloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:428:14: warning: conflicting types for built-in function ‘realloc’; expected ‘void *(void *, long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  428 | extern void *realloc (void *__ptr, size_t __size)
      |              ^~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:428:14: note: ‘realloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:438:14: warning: conflicting types for built-in function ‘alloca’; expected ‘void *(long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  438 | extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:442:12: warning: conflicting types for built-in function ‘posix_memalign’; expected ‘int(void **, long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  442 | extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
      |            ^~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:444:14: warning: conflicting types for built-in function ‘aligned_alloc’; expected ‘void *(long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  444 | extern void *aligned_alloc (size_t __alignment, size_t __size)
      |              ^~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:444:14: note: ‘aligned_alloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:598:15: warning: conflicting types for built-in function ‘strftime’; expected ‘long unsigned int(char *, long unsigned int,  const char *, const void *)’ [-Wbuiltin-declaration-mismatch]
  598 | extern size_t strftime (char *__restrict __s, size_t __maxsize,
      |               ^~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1: note: ‘strftime’ is declared in header ‘<time.h>’
    1 | typedef unsigned int size_t;
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i: In function ‘thread’:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1021:11: warning: initialization of ‘int’ from ‘void *’ makes integer from pointer without a cast [-Wint-conversion]
 1021 |   int i = arg;
      |           ^~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i: In function ‘main’:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1055:52: warning: passing argument 4 of ‘pthread_create’ makes pointer from integer without a cast [-Wint-conversion]
 1055 |     pthread_create(&tids[i], ((void *)0), &thread, i);
      |                                                    ^
      |                                                    |
      |                                                    int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:730:24: note: expected ‘void * restrict’ but argument is of type ‘int’
  730 |       void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
      |       ~~~~~~~~~~~~~~~~~^~~~~
......==================
WARNING: ThreadSanitizer: data race (pid=13)
  Read of size 4 at 0x55e87a733084 by thread T1 (mutexes: write M0):
    #0 cleaner /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1036 (a.out+0x1df2)

  Previous write of size 4 at 0x55e87a733084 by main thread:
    #0 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1056 (a.out+0x208a)

  Location is global 'threads_alive' of size 4 at 0x55e87a733084 (a.out+0x000000005084)

  Mutex M0 (0x7b1800000000) created at:
    #0 pthread_mutex_init ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1227 (libtsan.so.0+0x4bee1)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1051 (a.out+0x1fde)

  Thread T1 (tid=16, running) created by main thread at:
    #0 pthread_create ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:969 (libtsan.so.0+0x605b8)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1053 (a.out+0x2019)

SUMMARY: ThreadSanitizer: data race /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1036 in cleaner
==================
==================
WARNING: ThreadSanitizer: data race (pid=13)
  Write of size 8 at 0x7b0800000020 by main thread:
    #0 free ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:711 (libtsan.so.0+0x37ab8)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1059 (a.out+0x20ea)

  Previous read of size 8 at 0x7b0800000020 by thread T1:
    [failed to restore the stack]

  Thread T1 (tid=16, running) created by main thread at:
    #0 pthread_create ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:969 (libtsan.so.0+0x605b8)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1053 (a.out+0x2019)

SUMMARY: ThreadSanitizer: data race /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1059 in main
==================
==================
WARNING: ThreadSanitizer: data race (pid=13)
  Read of size 4 at 0x55e87a7330a0 by main thread:
    #0 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1060 (a.out+0x20f9)

  Previous write of size 4 at 0x55e87a7330a0 by thread T4 (mutexes: write M3):
    #0 thread /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1023 (a.out+0x1c7d)

  Location is global 'data' of size 4 at 0x55e87a7330a0 (a.out+0x0000000050a0)

  Mutex M3 (0x55e87a7330c0) created at:
    #0 pthread_mutex_lock ../../../../src/libsanitizer/sanitizer_common/sanitizer_common_interceptors.inc:4240 (libtsan.so.0+0x53908)
    #1 thread /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1022 (a.out+0x1c62)

  Thread T4 (tid=25, finished) created by main thread at:
    #0 pthread_create ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:969 (libtsan.so.0+0x605b8)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1055 (a.out+0x2063)

SUMMARY: ThreadSanitizer: data race /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter-race.i:1060 in main
==================
ThreadSanitizer: reported 3 warnings

SV-COMP result: false
