./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_peterson.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_peterson.i:604:2-607:2 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:612:2-615:2 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:696:2-699:2 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:725:2-728:2 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:775:4-778:4 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[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"
[Info] Enabled congruence domain.
[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_peterson.i:815:3-815: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_peterson.i:815:3-815: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_peterson.i:815:3-815: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_peterson.i:815:3-815:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:821:3-821: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_peterson.i:821:3-821: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_peterson.i:821:3-821: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_peterson.i:821:3-821:20)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:178:1-182:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:183:1-187:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:188:1-192:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:193:1-197:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.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_peterson.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_peterson.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_peterson.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_peterson.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_peterson.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_peterson.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_peterson.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_peterson.i:617:1-630:1)
[Warning][Deadcode] Function '__CS_assert' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:631:1-637:1)
[Warning][Deadcode] Function '__CS_assume' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:638:1-641:1)
[Warning][Deadcode] Function 'thr1' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:689:1-717:1)
[Warning][Deadcode] Function 'thr2' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:718:1-746:1)
[Warning][Deadcode] Function '__CS_pthread_create' has dead code:
  on lines 667..668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.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_peterson.i:646-648)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 122
  dead: 92 (87 in uncalled functions)
  total lines: 214
[Warning][Deadcode][CWE-570] condition '(int )__CS_thread_index == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.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_peterson.i:775:7-775: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_peterson.i:775:7-775: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_peterson.i:775:7-775: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_peterson.i:775:7-775:25)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:19:73-19:74)
[Warning][Deadcode][CWE-571] condition '(int )__CS_thread_allocated[0] == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:806:6-806:35)
[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_peterson.i:816:7-816:35)
[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_peterson.i:822:7-822:35)
[Warning][Deadcode][CWE-571] condition '(int )thread != 123' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.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_peterson.i:644:6-644:36)
[Warning][Deadcode][CWE-570] condition '(int )thread == 123' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_peterson.i:650:7-650:83)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Warning][Unsound][Call] No suitable function to call
