./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/smtprc-tid.i


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


/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:141:15: warning: conflicting types for built-in function ‘strftime’; expected ‘long unsigned int(char *, long unsigned int,  const char *, const void *)’ [-Wbuiltin-declaration-mismatch]
  141 | extern size_t strftime (char *__restrict __s, size_t __maxsize,
      |               ^~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1: note: ‘strftime’ is declared in header ‘<time.h>’
    1 | typedef unsigned char __u_char;
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:899:14: warning: conflicting types for built-in function ‘malloc’; expected ‘void *(long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  899 | extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__))
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1: note: ‘malloc’ is declared in header ‘<stdlib.h>’
    1 | typedef unsigned char __u_char;
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:901:14: warning: conflicting types for built-in function ‘calloc’; expected ‘void *(long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  901 | extern void *calloc (size_t __nmemb, size_t __size)
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:901:14: note: ‘calloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:903:14: warning: conflicting types for built-in function ‘realloc’; expected ‘void *(void *, long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  903 | extern void *realloc (void *__ptr, size_t __size)
      |              ^~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:903:14: note: ‘realloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:913:14: warning: conflicting types for built-in function ‘alloca’; expected ‘void *(long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  913 | extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
      |              ^~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:917:12: warning: conflicting types for built-in function ‘posix_memalign’; expected ‘int(void **, long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  917 | extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
      |            ^~~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:919:14: warning: conflicting types for built-in function ‘aligned_alloc’; expected ‘void *(long unsigned int,  long unsigned int)’ [-Wbuiltin-declaration-mismatch]
  919 | extern void *aligned_alloc (size_t __alignment, size_t __size)
      |              ^~~~~~~~~~~~~
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:919:14: note: ‘aligned_alloc’ is declared in header ‘<stdlib.h>’
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i: In function ‘main’:
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1032:47: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
 1032 |     pthread_create(&tid, ((void *)0), thread, (int *)i);
      |                                               ^
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1032:39: warning: passing argument 3 of ‘pthread_create’ from incompatible pointer type [-Wincompatible-pointer-types]
 1032 |     pthread_create(&tid, ((void *)0), thread, (int *)i);
      |                                       ^~~~~~
      |                                       |
      |                                       void * (*)(int)
/mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:394:15: note: expected ‘void * (*)(void *)’ but argument is of type ‘void * (*)(int)’
  394 |       void *(*__start_routine) (void *),
      |       ~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~
....==================
WARNING: ThreadSanitizer: data race (pid=11)
  Write of size 8 at 0x7b0800000020 by thread T2:
    #0 thread /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1022 (a.out+0x1cc6)

  Previous read of size 8 at 0x7b0800000020 by thread T1:
    #0 cleaner /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1013 (a.out+0x1bd5)

  Location is heap block of size 32 at 0x7b0800000020 allocated by main thread:
    #0 malloc ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:655 (libtsan.so.0+0x31c57)
    #1 main /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1027 (a.out+0x1d28)

  Thread T2 (tid=23, 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/smtprc-tid.i:1032 (a.out+0x1de3)

  Thread T1 (tid=14, 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/smtprc-tid.i:1030 (a.out+0x1db7)

SUMMARY: ThreadSanitizer: data race /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/smtprc-tid.i:1022 in thread
==================
ThreadSanitizer: reported 1 warnings

SV-COMP result: false
