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


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


./cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-tKhpeDOK.cil.c /mnt/goblint-svcomp/goblint-bench/bench/concrat/race-challenges/per-thread-array-join-counter.i

************************* STARTING *************************

per-thread-array-join-counter.i:1023: Warning: assigning pointer to non-pointer: (void)*^{arg:per-thread-array-join-counter.i:1022}
 ->
 int
per-thread-array-join-counter.i:1060: Warning: assigning number to pointer
functions declared and used but not defined:
  __VERIFIER_nondet_int
  abort
  pthread_cond_signal
  pthread_cond_wait
  pthread_join
Warning: Possible data race: &data:per-thread-array-join-counter.i:1020 is not protected!
 references:
  dereference of &data:per-thread-array-join-counter.i:1020 at per-thread-array-join-counter.i:1025
    &data:per-thread-array-join-counter.i:1020
  locks acquired:
    concrete data_mutex:per-thread-array-join-counter.i:1021
    data_mutex:per-thread-array-join-counter.i:1021
    data_mutex:per-thread-array-join-counter.i:1021
  in: main at per-thread-array-join-counter.i:1049 -> per-thread-array-join-counter.i:1060

  dereference of &data:per-thread-array-join-counter.i:1020 at per-thread-array-join-counter.i:1071
    &data:per-thread-array-join-counter.i:1020
  locks acquired:
    <empty>
  in: main at per-thread-array-join-counter.i:1049


Warning: Possible data race: alloc:per-thread-array-join-counter.i:1052 is not protected!
 references:
  dereference of tids:per-thread-array-join-counter.i:1017 at per-thread-array-join-counter.i:1037
    alloc:per-thread-array-join-counter.i:1052 => tids:per-thread-array-join-counter.i:1017
  locks acquired:
    *flags_mutex:per-thread-array-join-counter.i:1019
    non linear concrete *flags_mutex + i:per-thread-array-join-counter.i:1056
  in: main at per-thread-array-join-counter.i:1049 -> per-thread-array-join-counter.i:1058

  dereference of tids:per-thread-array-join-counter.i:1017 at per-thread-array-join-counter.i:1060
    alloc:per-thread-array-join-counter.i:1052 => tids:per-thread-array-join-counter.i:1017
  locks acquired:
    <empty>
  in: main at per-thread-array-join-counter.i:1049

  dereference of tids:per-thread-array-join-counter.i:1017 at per-thread-array-join-counter.i:1070
    alloc:per-thread-array-join-counter.i:1052 => tids:per-thread-array-join-counter.i:1017
  locks acquired:
    <empty>
  in: main at per-thread-array-join-counter.i:1049


Warning: Possible data race: alloc:per-thread-array-join-counter.i:1053 is protected by non-linear or concrete lock(s):
  *flags_mutex:per-thread-array-join-counter.i:1019
  non linear concrete *flags_mutex + i:per-thread-array-join-counter.i:1056
 references:
  dereference of flags:per-thread-array-join-counter.i:1018 at per-thread-array-join-counter.i:1028
    alloc:per-thread-array-join-counter.i:1053 => flags:per-thread-array-join-counter.i:1018
  locks acquired:
    *flags_mutex:per-thread-array-join-counter.i:1019
    non linear concrete *flags_mutex + i:per-thread-array-join-counter.i:1056
  in: main at per-thread-array-join-counter.i:1049 -> per-thread-array-join-counter.i:1060

  dereference of flags:per-thread-array-join-counter.i:1018 at per-thread-array-join-counter.i:1036
    alloc:per-thread-array-join-counter.i:1053 => flags:per-thread-array-join-counter.i:1018
  locks acquired:
    *flags_mutex:per-thread-array-join-counter.i:1019
    non linear concrete *flags_mutex + i:per-thread-array-join-counter.i:1056
  in: main at per-thread-array-join-counter.i:1049 -> per-thread-array-join-counter.i:1058

  dereference of flags:per-thread-array-join-counter.i:1018 at per-thread-array-join-counter.i:1042
    alloc:per-thread-array-join-counter.i:1053 => flags:per-thread-array-join-counter.i:1018
  locks acquired:
    *flags_mutex:per-thread-array-join-counter.i:1019
    non linear concrete *flags_mutex + i:per-thread-array-join-counter.i:1056
  in: main at per-thread-array-join-counter.i:1049 -> per-thread-array-join-counter.i:1058


*************************** DONE ***************************

LockSmith run for: 0.040633 seconds

gcc -D_GNUCC -E /tmp/cil-tKhpeDOK.cil.c -o /tmp/cil-uwltY7DG.cil.i
