./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/s3.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/loops/s3.i:1143:3-1647:3 with factor 2
[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] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] malloc, abort, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, method, ret, s, blastFlag, cb, num1, state, buf, new_state, s, ver, tmp
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&(alloc@sid:17)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1084:3-1084:18)
[Info][Unsound] Unknown address in {&(alloc@sid:31)} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1084:3-1084:18)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1084:3-1084:18)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1117:3-1117:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1132:3-1132:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1251:74-1251:118)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1296:74-1296:106)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1251:74-1251:118)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1296:74-1296:106)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1251:74-1251:118)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1296:74-1296:106)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1564:76-1564:104)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1570:74-1570:111)
[Warning][Deadcode] Function 'ssl3_get_client_method' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1028:1-1041:1)
[Warning][Deadcode] Function 'SSLv3_client_method' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1044:1-1063:1)
[Warning][Deadcode] Function 'sslv3_base_method' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1663:1-1671:1)
[Warning][Deadcode] Function 'ssl3_connect' has dead code:
  on line 1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1247-1247)
  on line 1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1660-1660)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 229
  dead: 17 (15 in uncalled functions)
  total lines: 246
[Warning][Deadcode][CWE-570] condition 's->state == 4433' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1188:37-1188:53)
[Warning][Deadcode][CWE-571] condition 's->state == 12292' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1146:9-1146:26)
[Warning][Deadcode][CWE-570] condition 's->state == 4448' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1191:39-1191:55)
[Warning][Deadcode][CWE-570] condition 's->state == 4449' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1194:41-1194:57)
[Warning][Deadcode][CWE-570] condition 's->state == 4464' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1197:43-1197:59)
[Warning][Deadcode][CWE-570] condition 's->state == 4465' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1200:45-1200:61)
[Warning][Deadcode][CWE-570] condition 's->state == 4466' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1203:47-1203:63)
[Warning][Deadcode][CWE-570] condition 's->state == 4467' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1206:49-1206:65)
[Warning][Deadcode][CWE-570] condition 's->state == 4480' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1209:51-1209:67)
[Warning][Deadcode][CWE-570] condition 's->state == 4481' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1212:53-1212:69)
[Warning][Deadcode][CWE-570] condition 's->state == 4496' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1215:55-1215:71)
[Warning][Deadcode][CWE-570] condition 's->state == 4497' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1218:57-1218:73)
[Warning][Deadcode][CWE-570] condition 's->state == 4512' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1221:59-1221:75)
[Warning][Deadcode][CWE-570] condition 's->state == 4513' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1224:61-1224:77)
[Warning][Deadcode][CWE-570] condition 's->state == 4528' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1227:63-1227:79)
[Warning][Deadcode][CWE-570] condition 's->state == 4529' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1230:65-1230:81)
[Warning][Deadcode][CWE-570] condition 's->state == 4560' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1233:67-1233:83)
[Warning][Deadcode][CWE-570] condition 's->state == 4561' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1236:69-1236:85)
[Warning][Deadcode][CWE-570] condition 's->state == 4352' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1239:71-1239:87)
[Warning][Deadcode][CWE-570] condition 's->state == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1242:73-1242:86)
[Warning][Deadcode][CWE-571] condition '! skip' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1618:11-1618:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1143:10-1143:11)
[Warning][Deadcode][CWE-571] condition '! skip' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1618:11-1618:17)
[Warning][Deadcode][CWE-571] condition 'blastFlag == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1303:77-1303:91)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1143:10-1143:11)
[Warning][Deadcode][CWE-570] condition 's->state == 16384' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1149:11-1149:28)
[Warning][Deadcode][CWE-570] condition 's->state == 20480' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1155:15-1155:32)
[Warning][Deadcode][CWE-570] condition 's->state == 4099' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1158:17-1158:33)
[Warning][Deadcode][CWE-570] condition 's->state == 4369' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1164:21-1164:37)
[Warning][Deadcode][CWE-570] condition 's->state == 4384' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1167:23-1167:39)
[Warning][Deadcode][CWE-570] condition 's->state == 4385' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1170:25-1170:41)
[Warning][Deadcode][CWE-570] condition 's->state == 4400' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1173:27-1173:43)
[Warning][Deadcode][CWE-570] condition 's->state == 4401' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1176:29-1176:45)
[Warning][Deadcode][CWE-570] condition 's->state == 4416' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1179:31-1179:47)
[Warning][Deadcode][CWE-570] condition 'blastFlag == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1387:77-1387:91)
[Warning][Deadcode][CWE-570] condition 's->state == 4417' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1182:33-1182:49)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1143:10-1143:11)
[Warning][Deadcode][CWE-570] condition 's->state == 4432' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/s3.i:1185:35-1185:51)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
