./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.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] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:604:2-607:2 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:612:2-615:2 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:702:4-705:4 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:694:2-713:2 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:745:4-748:4 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:737:2-756:2 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:3-808:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:800:2-809:2 with factor 3
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:845:3-845:20)
[Warning][Unsound][Call][CWE-685] Potential call to function thr2 with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:845:3-845:20)
[Warning][Unsound][Call][CWE-685] Potential call to function thr1 with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:845:3-845:20)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:845:3-845:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:851:3-851:20)
[Warning][Unsound][Call][CWE-685] Potential call to function thr2 with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:851:3-851:20)
[Warning][Unsound][Call][CWE-685] Potential call to function thr1 with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:851:3-851:20)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:851:3-851:20)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:178:1-182:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:183:1-187:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:188:1-192:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:193:1-197:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:198:1-202:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:569:1-572:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_destroy' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:573:1-581:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:582:1-587:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_unlock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:588:1-596:1)
[Warning][Deadcode] Function '__CS_pthread_cond_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:597:1-600:1)
[Warning][Deadcode] Function '__CS_pthread_cond_signal' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:601:1-608:1)
[Warning][Deadcode] Function '__CS_pthread_cond_broadcast' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:609:1-616:1)
[Warning][Deadcode] Function '__CS_pthread_cond_wait' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:617:1-630:1)
[Warning][Deadcode] Function '__CS_assert' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:631:1-637:1)
[Warning][Deadcode] Function 'thr1' is uncalled: 31 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:689:1-731:1)
[Warning][Deadcode] Function 'thr2' is uncalled: 31 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:732:1-774:1)
[Warning][Deadcode] Function '__CS_pthread_create' has dead code:
  on lines 667..668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:667-668)
[Warning][Deadcode] Function '__CS_pthread_join' has dead code:
  on lines 646..648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:646-648)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 127
  dead: 110 (105 in uncalled functions)
  total lines: 237
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:800:6-800:24)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-570] condition 'i < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:800:6-800:24)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:800:6-800:24)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:19:73-19:74)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition '(int )thread != 123' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:644:6-644:36)
[Warning][Deadcode][CWE-570] condition '(int )thread > 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:644:6-644:36)
[Warning][Deadcode][CWE-571] condition '(int )__CS_thread_allocated[0] == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:836:6-836:35)
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:800:6-800:24)
[Warning][Deadcode][CWE-570] condition '(int )thread == 123' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:650:7-650:83)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition '(int )__CS_ret != (int )__CS_ret_PREEMPTED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:846:7-846:35)
[Warning][Deadcode][CWE-570] condition '(int )__CS_thread_index == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:666:6-666:28)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
[Warning][Deadcode][CWE-571] condition '(int )__CS_ret != (int )__CS_ret_PREEMPTED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:852:7-852:35)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_dekker.i:805:7-805:25)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Warning][Unsound][Call] No suitable function to call
