./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/loops-crafted-1/discover_list.c


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


[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/loops-crafted-1/discover_list.c:162:1-166:1 with factor 25
[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] function smp_get_num is recursive, disable interval and interval_set contexts
[Info] function smp_get_llnum is recursive, disable interval and interval_set contexts
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] __tmpTR__int_1, toupper, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, resp, tmp___0, tmp___1, len, smp_rr, mnum_desc, smp_req, dword_resp_len, res, res, c2, tmp___3, c3, num, buf, ll, cp, res, tmp___3, c2, c3, num, buf, n, cp, bpos, k, len, c, cpos, no_ascii, i, a, func_code, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&opts} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:496:5-496:93)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:496:5-496:93)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:424:1-424:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:430:1-430:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:431:1-431:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:433:1-433:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:434:1-434:34)
[Error][Imprecise][Unsound] Function definition missing for smp_send_req (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:48)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:48)
[Info][Imprecise] Invalidating expressions: & smp_def_rrlen_arr, & __tmpTR__int_1, (struct smp_target_obj  const  *)top, & smp_rr, op->verbose (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:48)
[Info][Imprecise] Invalidating expressions: & res (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:48)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:459:1-459:20)
[Info][Imprecise] Invalidating expressions: (char * __restrict  )(buff + 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:193:1-193:33)
[Info][Imprecise] Invalidating expressions: & k (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:193:1-193:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:194:5-194:92)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:197:1-197:12)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:198:1-198:10)
[Info][Imprecise] Invalidating expressions: (char * __restrict  )(& buff[bpos]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:172)
[Info][Imprecise] Invalidating expressions: & __tmpTR__int_1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:172)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:202:5-202:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:157:3-157:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:213:1-213:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:215:1-215:8)
[Info][Imprecise] Invalidating expressions: (char * __restrict  )(buff + 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:217:1-217:33)
[Info][Imprecise] Invalidating expressions: & k (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:217:1-217:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:218:5-218:92)
[Warning][Deadcode] Function 'smp_is_naa5' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:169:1-172:1)
[Warning][Deadcode] Function 'smp_get_num' is uncalled: 62 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:223:1-310:1)
[Warning][Deadcode] Function 'smp_get_llnum' is uncalled: 77 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:311:1-412:1)
[Warning][Deadcode] Function 'dStrHex' has dead code:
  on line 186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:186-186)
  on line 191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:191-191)
  on lines 207..209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:207-209)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 91
  dead: 145 (140 in uncalled functions)
  total lines: 236
[Warning][Deadcode][CWE-570] condition 'len <= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:185:4-185:12)
[Warning][Deadcode][CWE-570] condition 'no_ascii < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:189:4-189:16)
[Warning][Deadcode][CWE-571] condition 'dword_resp_len < 0x100' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:423:1-423:62)
[Warning][Deadcode][CWE-571] condition 'bpos >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:172)
[Warning][Deadcode][CWE-571] condition 'bpos + 2 >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:202:5-202:101)
[Warning][Deadcode][CWE-571] condition 'no_ascii' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:203:4-203:12)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:204:3-204:175)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 < 82' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/discover_list.c:204:3-204:175)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Error][Imprecise][Unsound] Function definition missing
