./goblint --conf conf/svcomp.json --set ana.malloc.unique_address_count 1 --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/openssl/s3_srvr.blast.16.i.cil-1.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 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] Enabled octagon domain ONLY for:
[Info] malloc, abort, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, method, blastFlag, ret, s, cb, num1, state, buf, tmp___13, s, tmp, tmp___9, ver, tmp
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&(alloc@sid:17(#0))} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1106:3-1106:23)
[Info][Unsound] Unknown address in {&(alloc@sid:23(#0))} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1106:3-1106:23)
[Info][Unsound] Unknown address in {&(alloc@sid:41(#0))} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1106:3-1106:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1106:3-1106:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1141:3-1141:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1152:3-1152:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1524:79-1524:108)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1435:91-1435:112)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1699:80-1699:116)
[Warning][Deadcode] Function 'ssl3_get_server_method' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1040:1-1053:1)
[Warning][Deadcode] Function 'SSLv3_server_method' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1056:1-1075:1)
[Warning][Deadcode] Function 'sslv3_base_method' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1799:1-1807:1)
[Warning][Deadcode] Function 'ssl3_accept' has dead code:
  on line 1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1278-1278)
  on line 1280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1280-1280)
  on lines 1285..1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1285-1286)
  on lines 1291..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1291-1292)
  on lines 1296..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1296-1300)
  on lines 1305..1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1305-1306)
  on line 1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1311-1311)
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1315-1316)
  on lines 1321..1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1321-1324)
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1329-1330)
  on lines 1332..1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1332-1333)
  on lines 1338..1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1338-1340)
  on lines 1345..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1345-1347)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1350-1350)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1712-1712)
  on line 1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1796-1796)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 254
  dead: 48 (15 in uncalled functions)
  total lines: 302
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1168:10-1168:11)
[Warning][Deadcode][CWE-570] condition 's->state == 12292' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1171:9-1171:26)
[Warning][Deadcode][CWE-570] condition 's->state == 16384' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1174:11-1174:28)
[Warning][Deadcode][CWE-570] condition 's->state == 8192' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1177:13-1177:29)
[Warning][Deadcode][CWE-570] condition 's->state == 24576' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1180:15-1180:32)
[Warning][Deadcode][CWE-570] condition 's->state == 8195' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1183:17-1183:33)
[Warning][Deadcode][CWE-570] condition 's->state == 8480' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1186:19-1186:35)
[Warning][Deadcode][CWE-570] condition 's->state == 8481' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1189:21-1189:37)
[Warning][Deadcode][CWE-570] condition 's->state == 8482' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1192:23-1192:39)
[Warning][Deadcode][CWE-570] condition 's->state == 8465' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1198:27-1198:43)
[Warning][Deadcode][CWE-570] condition 's->state == 8497' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1207:33-1207:49)
[Warning][Deadcode][CWE-570] condition 's->state == 8513' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1213:37-1213:53)
[Warning][Deadcode][CWE-570] condition 's->state == 8529' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1219:41-1219:57)
[Warning][Deadcode][CWE-570] condition 's->state == 8545' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1225:45-1225:61)
[Warning][Deadcode][CWE-570] condition 's->state == 8561' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1231:49-1231:65)
[Warning][Deadcode][CWE-570] condition 's->state == 8577' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1240:55-1240:71)
[Warning][Deadcode][CWE-570] condition 's->state == 8593' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1246:59-1246:75)
[Warning][Deadcode][CWE-570] condition 's->state == 8609' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1252:63-1252:79)
[Warning][Deadcode][CWE-570] condition 's->state == 8641' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1258:67-1258:83)
[Warning][Deadcode][CWE-570] condition 's->state == 8657' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1264:71-1264:87)
[Warning][Deadcode][CWE-570] condition 's->state == 8673' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1270:75-1270:91)
[Warning][Deadcode][CWE-571] condition 's->state == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openssl/s3_srvr.blast.16.i.cil-1.c:1273:77-1273:90)
SV-COMP result: unknown
[Warning][Analyzer] Invariant Apron: coefficient is not int: 9.22337203686e+18
[Warning][Analyzer] Invariant Apron: coefficient is not int: 9.22337203901e+18
[Info][Witness] witness generation summary:
  total generation entries: 1
