./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/ntdrivers-simplified/floppy_simpl4.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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:550:7-566:7 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] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1306:5-1306:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1307:5-1307:48)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1519:29-1519:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1520:29-1520:72)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1410:29-1410:81)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1418:29-1418:96)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1433:29-1433:84)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1441:29-1441:99)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:117:3-117:45)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1501:29-1501:87)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1502:29-1502:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:248:21-248:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:249:21-249:64)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:489:3-489:59)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:505:3-505:59)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:979:5-979:48)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:631:3-631:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:279:21-279:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:280:21-280:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:309:21-309:44)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:310:21-310:64)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:317:21-317:77)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:333:21-333:77)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:368:19-368:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:369:19-369:62)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:385:19-385:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:386:19-386:62)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:402:19-402:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:413:19-413:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:414:19-414:62)
[Warning][Deadcode] Function 'FloppyProcessQueuedRequests' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:647:1-653:1)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:886:1-908:1)
[Warning][Deadcode] Function 'FlQueueIrpToThread' has dead code:
  on line 154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:154-154)
[Warning][Deadcode] Function 'FloppyDeviceControl' has dead code:
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1302-1302)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1401-1401)
  on line 1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1515-1515)
[Warning][Deadcode] Function 'FloppyPnp' has dead code:
  on line 229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:229-229)
  on line 244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:244-244)
  on line 275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:275-275)
  on line 305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:305-305)
  on line 321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:321-321)
  on line 326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:326-326)
  on line 364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:364-364)
  on line 381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:381-381)
  on line 409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:409-409)
[Warning][Deadcode] Function 'FloppyQueueRequest' has dead code:
  on line 1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1614-1614)
[Warning][Deadcode] Function 'FloppyStartDevice' has dead code:
  on line 493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:493-493)
  on line 498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:498-498)
  on lines 557..558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:557-558)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:562-562)
  on line 565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:565-565)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' has dead code:
  on line 854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:854-854)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' has dead code:
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:875-875)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' has dead code:
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:920-920)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' has dead code:
  on line 941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:941-941)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:998-998)
  on lines 1014..1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1014-1015)
  on line 1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1031-1031)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1081-1081)
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1092-1092)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' has dead code:
  on line 1114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1114-1114)
[Warning][Deadcode] Function 'PsCreateSystemThread' has dead code:
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1136-1136)
[Warning][Deadcode] Function 'ZwClose' has dead code:
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1157-1157)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1628-1628)
[Warning][Deadcode] Function 'main' has dead code:
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:725-725)
  on line 749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:749-749)
  on line 790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:790-790)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 590
  dead: 45 (8 in uncalled functions)
  total lines: 635
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:550:14-550:15)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:360:23-360:30)
[Warning][Deadcode][CWE-571] condition 'PagingReferenceCount == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1591:7-1591:32)
[Warning][Deadcode][CWE-571] condition 'status >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:707:7-707:18)
[Warning][Deadcode][CWE-571] condition 'InterfaceType >= MaximumInterfaceType' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:553:13-553:50)
[Warning][Deadcode][CWE-571] condition 'PagingReferenceCount == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1602:9-1602:34)
[Warning][Deadcode][CWE-571] condition 'PagingReferenceCount == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:193:7-193:32)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:377:23-377:30)
[Warning][Deadcode][CWE-571] condition 'pended == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1610:9-1610:20)
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:724:9-724:19)
[Warning][Deadcode][CWE-571] condition '__cil_tmp7 == 3221225494UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:980:9-980:34)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:405:23-405:30)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:240:25-240:32)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1013:7-1013:14)
[Warning][Deadcode][CWE-571] condition 'ntStatus >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:571:9-571:22)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1026:11-1026:21)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:789:11-789:20)
[Warning][Deadcode][CWE-571] condition 's != UNLOADED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:796:11-796:24)
[Warning][Deadcode][CWE-571] condition 'status != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:797:13-797:25)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:271:25-271:32)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:799:17-799:25)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1067:9-1067:28)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1079:11-1079:20)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:301:25-301:32)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1298:9-1298:16)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:491:7-491:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:1511:33-1511:40)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:496:9-496:28)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:319:25-319:32)
[Warning][Deadcode][CWE-571] condition 'pended == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:150:7-150:18)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c:324:27-324:46)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
