./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/diskperf_simpl1.cil.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/diskperf_simpl1.cil.c:404:7-411:7 with factor 25
[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, 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/diskperf_simpl1.cil.c:427:5-427:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:428:5-428:48)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:204:3-204:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:205:3-205:46)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:255:3-255:59)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:272:3-272:59)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:892:5-892:47)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:554:5-554:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:556:7-556:62)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:229:3-229:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:230:3-230:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:447:3-447:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:448:3-448:46)
[Warning][Deadcode] Function 'DiskPerfIoCompletion' is uncalled: 32 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:300:1-353:1)
[Warning][Deadcode] Function 'DiskPerfDispatchPnp' has dead code:
  on line 112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:112-112)
[Warning][Deadcode] Function 'DiskPerfDispatchPower' has dead code:
  on line 225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:225-225)
[Warning][Deadcode] Function 'DiskPerfForwardIrpSynchronous' has dead code:
  on line 259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:259-259)
  on line 264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:264-264)
[Warning][Deadcode] Function 'DiskPerfRegisterDevice' has dead code:
  on line 558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:558-558)
[Warning][Deadcode] Function 'DiskPerfSendToNextDriver' has dead code:
  on line 200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:200-200)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' has dead code:
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:848-848)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:888-888)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:911-911)
  on line 944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:944-944)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on line 994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:994-994)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1005-1005)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1026-1026)
  on line 1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1028-1028)
  on line 1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1031-1031)
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1033-1033)
  on lines 1038..1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1038-1039)
  on line 1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1041-1041)
  on line 1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1057-1057)
  on lines 1073..1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1073-1074)
  on lines 1078..1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1078-1081)
  on lines 1083..1084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1083-1084)
  on line 1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1093-1093)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 57 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:57-57)
[Warning][Deadcode] Function 'main' has dead code:
  on line 702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:702-702)
  on line 731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:731-731)
  on lines 774..775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:774-775)
  on lines 782..783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:782-783)
  on line 795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:795-795)
  on line 806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:806-806)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:808-808)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 402
  dead: 71 (32 in uncalled functions)
  total lines: 473
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1025:7-1025:21)
[Warning][Deadcode][CWE-570] condition 's != DC' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:793:19-793:26)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:805:17-805:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:196:7-196:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:221:7-221:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1072:7-1072:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1076:9-1076:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition 'routine == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:882:9-882:21)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:1088:11-1088:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '__cil_tmp7 == 18446744072635809814UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:893:9-893:34)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:257:7-257:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:262:9-262:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:701:9-701:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:939:11-939:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition '! output' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:557:11-557:19)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:980:9-980:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:992:11-992:20)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:773:7-773:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:781:9-781:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1.cil.c:404:14-404:15)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
