./goblint --conf conf/svcomp.json --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/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.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/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1481:5-1484:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1490:5-1496:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1502:5-1508:5 with factor 2
[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, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] printf, __ctype_b_loc, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, data___0, data, dataCopy, result, data, dataCopy, data___0, result, numWritten, numBytes, tmp, tmp___0, numWritten, numBytes, i, numBytes, doubleNumber, unsignedNumber, wideChar, sizeTNumber, longLongIntNumber, longNumber, intNumber, line, line, __x, __x, __x
[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/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1589:5-1589:41)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1589:5-1589:41)
[Info][Imprecise] Invalidating expressions: & data (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1567:5-1567:39)
[Info][Imprecise] Invalidating expressions: stdin (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1567:5-1567:39)
[Info][Unsound] Unknown address in stdin has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1567:5-1567:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1567:5-1567:39)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:425:1-429:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:430:1-434:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:435:15-439:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:440:1-444:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:445:1-449:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:450:1-454:1)
[Warning][Deadcode] Function 'printWLine' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1420:1-1426:1)
[Warning][Deadcode] Function 'printIntLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1427:1-1430:1)
[Warning][Deadcode] Function 'printShortLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1431:1-1434:1)
[Warning][Deadcode] Function 'printFloatLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1435:1-1438:1)
[Warning][Deadcode] Function 'printLongLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1439:1-1442:1)
[Warning][Deadcode] Function 'printSizeTLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1447:1-1450:1)
[Warning][Deadcode] Function 'printHexCharLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1451:1-1454:1)
[Warning][Deadcode] Function 'printWcharLine' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1455:1-1461:1)
[Warning][Deadcode] Function 'printUnsignedLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1462:1-1465:1)
[Warning][Deadcode] Function 'printHexUnsignedCharLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1466:1-1469:1)
[Warning][Deadcode] Function 'printDoubleLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1470:1-1473:1)
[Warning][Deadcode] Function 'printStructLine' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1474:1-1477:1)
[Warning][Deadcode] Function 'printBytesLine' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1478:1-1486:1)
[Warning][Deadcode] Function 'decodeHexChars' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1487:1-1498:1)
[Warning][Deadcode] Function 'decodeHexWChars' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1499:2-1510:1)
[Warning][Deadcode] Function 'globalReturnsTrue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1511:1-1514:1)
[Warning][Deadcode] Function 'globalReturnsFalse' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1515:1-1518:1)
[Warning][Deadcode] Function 'globalReturnsTrueOrFalse' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1519:1-1522:1)
[Warning][Deadcode] Function 'good1' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1529:1-1529:16)
[Warning][Deadcode] Function 'good2' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1530:1-1530:16)
[Warning][Deadcode] Function 'good3' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1531:1-1531:16)
[Warning][Deadcode] Function 'good4' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1532:1-1532:16)
[Warning][Deadcode] Function 'good5' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1533:1-1533:16)
[Warning][Deadcode] Function 'good6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1534:1-1534:16)
[Warning][Deadcode] Function 'good7' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1535:1-1535:16)
[Warning][Deadcode] Function 'good8' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1536:1-1536:16)
[Warning][Deadcode] Function 'good9' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1537:1-1537:16)
[Warning][Deadcode] Function 'bad1' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1538:1-1538:15)
[Warning][Deadcode] Function 'bad2' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1539:1-1539:15)
[Warning][Deadcode] Function 'bad3' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1540:1-1540:15)
[Warning][Deadcode] Function 'bad4' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1541:1-1541:15)
[Warning][Deadcode] Function 'bad5' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1542:1-1542:15)
[Warning][Deadcode] Function 'bad6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1543:1-1543:15)
[Warning][Deadcode] Function 'bad7' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1544:1-1544:15)
[Warning][Deadcode] Function 'bad8' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1545:1-1545:15)
[Warning][Deadcode] Function 'bad9' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1546:1-1546:15)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 35
  dead: 70 (70 in uncalled functions)
  total lines: 105
[Warning][Deadcode][CWE-571] condition '(unsigned long )line != (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/Juliet_Test/CWE191_Integer_Underflow__int64_t_fscanf_sub_31_good.i:1415:8-1415:27)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
