./goblint --conf conf/svcomp25.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] Specification: CHECK( init(main()), LTL(G ! data-race) ) -> enabling soundness analyses "access, race"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] dev_size, __X__, i___0, count, tmp, key, a, count, i___0, j, i___1, j___0, k, size, r, top, expression, t1, t2, t3, filp, tmp, buf, tmp___0, count, off, filp, tmp, buf, tmp___0, count, off, result, dev, tmp, whence, newpos, off, filp, f_pos, cmd, retval, arg, tmp, count, f_pos, quantum, q_pos, dptr, filp, buf, dev, count, f_pos, quantum, q_pos, filp, buf, dev, qset, dev, i___0, tmp, tmp, from, tmp, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:12:1-12:158)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:68:1-72:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:73:1-77:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:78:1-82:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:83:1-87:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:88:1-92:1)
[Warning][Deadcode] Function 'scull_ioctl' is uncalled: 51 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:809:1-865:1)
[Warning][Deadcode] Function 'scull_llseek' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:866:1-886:1)
[Warning][Deadcode] Function 'scull_init_module' has dead code:
  on lines 897..898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:897-898)
[Warning][Deadcode] Function 'scull_open' has dead code:
  on line 733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:733-733)
[Warning][Deadcode] Function 'scull_read' has dead code:
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:753-753)
[Warning][Deadcode] Function 'scull_write' has dead code:
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:786-786)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 111
  dead: 77 (72 in uncalled functions)
  total lines: 188
[Warning][Deadcode][CWE-570] condition '! (__X__ <= 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:771:7-771:20)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:785:7-785:27)
[Warning][Race] Memory location dev_qset (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:715:5-715:13)
  write with [region:{dev_qset}, thread:[main, loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:928:3-928:36]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3-723:24)
  write with [region:{dev_qset}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3-723:24)
  write with [region:{dev_qset}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:723:3-723:24)
  read with [region:{dev_qset}, thread:[main, loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:928:3-928:36]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:7-720:22)
  read with [region:{dev_qset}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:7-720:22)
  read with [region:{dev_qset}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:720:7-720:22)
  read with [region:{dev_qset}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:748:30-748:45)
  read with [region:{dev_qset}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_qset) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:781:30-781:45)
[Warning][Race] Memory location dev_data (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:713:5-713:13)
  write with [region:{dev_data}, thread:[main, loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:928:3-928:36]] (conf. 110)  (exp: & dev_data) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3-724:15)
  write with [region:{dev_data}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_data) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3-724:15)
  write with [region:{dev_data}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_data) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:724:3-724:15)
  read with [region:{dev_data}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_data) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:765:7-765:57)
  read with [region:{dev_data}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_data) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:796:7-796:55)
[Warning][Deadcode][CWE-570] condition '! (__X__ == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:804:7-804:20)
[Warning][Race] Memory location dev_size (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:716:5-716:13)
  write with [region:{dev_size}, thread:[main, loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:928:3-928:36]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3-721:15)
  write with [region:{dev_size}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3-721:15)
  write with [region:{dev_size}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:721:3-721:15)
  write with [region:{dev_size}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:803:5-803:21)
  read with [region:{dev_size}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:755:7-755:24)
  read with [region:{dev_size}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:757:7-757:30)
  read with [region:{dev_size}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:758:5-758:29)
  read with [region:{dev_size}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_size) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:802:7-802:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:732:7-732:27)
[Warning][Deadcode][CWE-570] condition '! (__X__ >= 2)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:736:7-736:20)
[Warning][Race] Memory location dev_quantum (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:714:5-714:16)
  write with [region:{dev_quantum}, thread:[main, loader@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:928:3-928:36]] (conf. 110)  (exp: & dev_quantum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3-722:30)
  write with [region:{dev_quantum}, lock:{lock}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_quantum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3-722:30)
  write with [region:{dev_quantum}, lock:{lock}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_quantum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:722:3-722:30)
  read with [region:{dev_quantum}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:929:3-929:37]] (conf. 110)  (exp: & dev_quantum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:748:7-748:28)
  read with [region:{dev_quantum}, thread:[main, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:930:3-930:37]] (conf. 110)  (exp: & dev_quantum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:781:7-781:28)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:752:7-752:27)
[Warning][Deadcode][CWE-571] condition 'f_pos + count >= dev_size' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/scull.i:757:7-757:30)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 4
  vulnerable: 0
  unsafe: 4
  total memory locations: 8
