./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 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.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/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1480:5-1483:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1489:5-1495:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1501:5-1507:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54 with factor 12
[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 globalReturnsTrueOrFalse uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[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] printf, __ctype_b_loc, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, data, result, data, data, data, tmp, tmp___0, data, numWritten, numBytes, tmp, tmp___0, numWritten, numBytes, i, numBytes, doubleNumber, unsignedNumber, wideChar, sizeTNumber, longLongIntNumber, longNumber, intNumber, line, line, __x, __x, __x
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Imprecise] Invalidating expressions: (time_t *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1568:5-1568:41)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1568:5-1568:41)
[Info][Imprecise] Invalidating expressions: (char * __restrict  )(inputBuffer) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1555:13-1555:77)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdin (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1555:13-1555:77)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdin has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1555:13-1555:77)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1555:13-1555:77)
[Info][Imprecise] Invalidating expressions: & tmp___0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1555:13-1555:77)
[Info][Imprecise] Invalidating expressions: & data (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1557:13-1557:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1592:13-1592:30)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:379:1-383:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:384:1-388:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:389:15-393:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:394:1-398:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:399:1-403:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:404:1-408:1)
[Warning][Deadcode] Function 'printWLine' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1419:1-1425:1)
[Warning][Deadcode] Function 'printShortLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1430:1-1433:1)
[Warning][Deadcode] Function 'printFloatLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1434:1-1437:1)
[Warning][Deadcode] Function 'printLongLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1438:1-1441:1)
[Warning][Deadcode] Function 'printLongLongLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1442:1-1445:1)
[Warning][Deadcode] Function 'printSizeTLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1446:1-1449:1)
[Warning][Deadcode] Function 'printHexCharLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1450:1-1453:1)
[Warning][Deadcode] Function 'printWcharLine' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1454:1-1460:1)
[Warning][Deadcode] Function 'printUnsignedLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1461:1-1464:1)
[Warning][Deadcode] Function 'printHexUnsignedCharLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1465:1-1468:1)
[Warning][Deadcode] Function 'printDoubleLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1469:1-1472:1)
[Warning][Deadcode] Function 'printStructLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1473:1-1476:1)
[Warning][Deadcode] Function 'printBytesLine' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1477:1-1485:1)
[Warning][Deadcode] Function 'decodeHexChars' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1486:1-1497:1)
[Warning][Deadcode] Function 'decodeHexWChars' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1498:2-1509:1)
[Warning][Deadcode] Function 'globalReturnsTrue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1510:1-1513:1)
[Warning][Deadcode] Function 'globalReturnsFalse' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1514:1-1517:1)
[Warning][Deadcode] Function 'globalReturnsTrueOrFalse' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1518:1-1521:1)
[Warning][Deadcode] Function 'good1' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1528:1-1528:16)
[Warning][Deadcode] Function 'good2' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1529:1-1529:16)
[Warning][Deadcode] Function 'good3' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1530:1-1530:16)
[Warning][Deadcode] Function 'good4' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1531:1-1531:16)
[Warning][Deadcode] Function 'good5' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1532:1-1532:16)
[Warning][Deadcode] Function 'good6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1533:1-1533:16)
[Warning][Deadcode] Function 'good7' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1534:1-1534:16)
[Warning][Deadcode] Function 'good8' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1535:1-1535:16)
[Warning][Deadcode] Function 'good9' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1536:1-1536:16)
[Warning][Deadcode] Function 'bad1' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1537:1-1537:15)
[Warning][Deadcode] Function 'bad2' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1538:1-1538:15)
[Warning][Deadcode] Function 'bad3' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1539:1-1539:15)
[Warning][Deadcode] Function 'bad4' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1540:1-1540:15)
[Warning][Deadcode] Function 'bad5' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1541:1-1541:15)
[Warning][Deadcode] Function 'bad6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1542:1-1542:15)
[Warning][Deadcode] Function 'bad7' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1543:1-1543:15)
[Warning][Deadcode] Function 'bad8' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1544:1-1544:15)
[Warning][Deadcode] Function 'bad9' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1545:1-1545:15)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 34
  dead: 70 (70 in uncalled functions)
  total lines: 104
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-571] condition '(unsigned long )line != (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1414:8-1414:27)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
[Warning][Deadcode][CWE-570] condition 'tmp >= 14U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int_fgets_add_54_bad.i:1554:9-1554:54)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
