./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/cdaudio_simpl1.cil-2.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/cdaudio_simpl1.cil-2.c:172:5-189:5 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-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:882:3-882:38)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:724:27-724:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:381:3-381:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:382:3-382:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1137:31-1137:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1157:31-1157:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1160:33-1160:69)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1163:35-1163:71)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1219:31-1219:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1269:31-1269:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1303:31-1303:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1341:31-1341:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1372:31-1372:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1387:31-1387:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1257:31-1257:68)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1488:3-1488:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1563:5-1563:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1915:5-1915:47)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1696:3-1696:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1697:3-1697:46)
[Warning][Deadcode] Function 'CdAudio435DeviceControl' has dead code:
  on line 1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1118-1118)
  on line 1139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1139-1139)
  on line 1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1165-1165)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1176-1176)
  on line 1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1180-1180)
  on lines 1183..1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1183-1184)
  on line 1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1186-1186)
  on lines 1188..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1188-1192)
  on line 1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1194-1194)
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1196-1197)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1221-1221)
  on line 1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1259-1259)
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1271-1271)
  on line 1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1285-1285)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1305-1305)
  on lines 1316..1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1316-1318)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1321-1321)
  on lines 1323..1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1323-1325)
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1329-1330)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1332-1332)
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1343-1343)
  on lines 1358..1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1358-1359)
  on line 1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1374-1374)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1389-1389)
  on lines 1405..1406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1405-1406)
  on line 1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1408-1408)
  on line 1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1438-1438)
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1490-1490)
[Warning][Deadcode] Function 'CdAudio535DeviceControl' has dead code:
  on line 637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:637-637)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:675-675)
  on lines 678..679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:678-679)
  on lines 682..683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:682-683)
  on lines 714..716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:714-716)
  on lines 734..738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:734-738)
  on line 740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:740-740)
  on lines 742..743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:742-743)
  on line 776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:776-776)
  on line 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:801-801)
[Warning][Deadcode] Function 'CdAudioAtapiDeviceControl' has dead code:
  on lines 1551..1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1551-1553)
  on line 1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1555-1555)
[Warning][Deadcode] Function 'CdAudioDeviceControl' has dead code:
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:330-330)
[Warning][Deadcode] Function 'CdAudioForwardIrpSynchronous' has dead code:
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1648-1648)
  on line 1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1653-1653)
[Warning][Deadcode] Function 'CdAudioHPCdrDeviceControl' has dead code:
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1612-1612)
  on line 1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1617-1617)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1636-1636)
[Warning][Deadcode] Function 'CdAudioPnp' has dead code:
  on line 243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:243-243)
  on line 309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:309-309)
[Warning][Deadcode] Function 'CdAudioPower' has dead code:
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1692-1692)
[Warning][Deadcode] Function 'CdAudioSendToNextDriver' has dead code:
  on line 377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:377-377)
[Warning][Deadcode] Function 'CdAudioStartDevice' has dead code:
  on line 170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:170-170)
  on line 172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:172-172)
  on lines 176..179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:176-179)
  on line 187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:187-187)
  on lines 194..196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:194-196)
  on line 199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:199-199)
  on line 204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:204-204)
[Warning][Deadcode] Function 'HPCdrCompletion' has dead code:
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1578-1578)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1937-1937)
  on line 1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1971-1971)
[Warning][Deadcode] Function 'IofCompleteRequest' has dead code:
  on line 1987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1987-1987)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2016-2017)
  on line 2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2021-2021)
  on line 2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2032-2032)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 2053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2053-2053)
  on line 2055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2055-2055)
  on line 2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2058-2058)
  on line 2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2060-2060)
  on lines 2065..2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2065-2066)
  on line 2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2068-2068)
  on line 2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2084-2084)
  on lines 2100..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2100-2101)
  on lines 2105..2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2105-2108)
  on lines 2110..2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2110-2111)
  on line 2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2120-2120)
[Warning][Deadcode] Function 'SendSrbSynchronous' has dead code:
  on lines 120..121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:120-121)
  on lines 123..124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:123-124)
  on line 128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:128-128)
[Warning][Deadcode] Function 'ZwClose' has dead code:
  on line 2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2138-2138)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 60 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:60-60)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1776-1776)
  on line 1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1795-1795)
  on line 1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1827-1827)
  on line 1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1835-1835)
  on line 1847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1847-1847)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1888-1888)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 812
  dead: 124
  total lines: 936
[Warning][Deadcode][CWE-571] condition '! inquiryDataPtr' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:166:9-166:25)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1255:33-1255:43)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1646:7-1646:14)
[Warning][Deadcode][CWE-570] condition '__cil_tmp105 == 3221225488UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1258:35-1258:62)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1826:9-1826:16)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1651:9-1651:28)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2052:7-2052:21)
[Warning][Deadcode][CWE-570] condition '__cil_tmp4 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:883:7-883:32)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1834:11-1834:20)
[Warning][Deadcode][CWE-570] condition '__cil_tmp106 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1270:35-1270:62)
[Warning][Deadcode][CWE-571] condition 'status' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1665:7-1665:13)
[Warning][Deadcode][CWE-570] condition '__cil_tmp115 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1437:35-1437:62)
[Warning][Deadcode][CWE-570] condition 's != DC' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1845:19-1845:26)
[Warning][Deadcode][CWE-570] condition '__cil_tmp107 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1284:35-1284:62)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:712:29-712:40)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1688:7-1688:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:373:7-373:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1884:7-1884:14)
[Warning][Deadcode][CWE-571] condition '__cil_tmp108 != 3221225532UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:725:31-725:58)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1301:33-1301:43)
[Warning][Deadcode][CWE-570] condition '__cil_tmp116 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1489:7-1489:34)
[Warning][Deadcode][CWE-570] condition '__cil_tmp93 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1138:35-1138:61)
[Warning][Deadcode][CWE-570] condition '__cil_tmp109 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1304:35-1304:62)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2099:7-2099:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2103:9-2103:18)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1155:33-1155:43)
[Warning][Deadcode][CWE-571] condition 'routine == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1908:11-1908:23)
[Warning][Deadcode][CWE-571] condition '__cil_tmp95 != 3221225532UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1158:35-1158:61)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2115:11-2115:21)
[Warning][Deadcode][CWE-571] condition '__cil_tmp96 != 3221225532UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1161:37-1161:63)
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:203:7-203:17)
[Warning][Deadcode][CWE-570] condition '__cil_tmp97 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1164:39-1164:65)
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:208:7-208:17)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1534:9-1534:19)
[Warning][Deadcode][CWE-570] condition '__cil_tmp112 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1342:35-1342:62)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:775:29-775:40)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1357:33-1357:44)
[Warning][Deadcode][CWE-571] condition 'pended == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1574:9-1574:20)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1966:11-1966:21)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1208:33-1208:44)
[Warning][Deadcode][CWE-571] condition '! irp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:116:7-116:12)
[Warning][Deadcode][CWE-570] condition '__cil_tmp113 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1373:35-1373:62)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:800:29-800:40)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1983:7-1983:14)
[Warning][Deadcode][CWE-571] condition 'status == status' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:270:15-270:31)
[Warning][Deadcode][CWE-570] condition '__cil_tmp104 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1220:35-1220:62)
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1775:9-1775:19)
[Warning][Deadcode][CWE-570] condition '__cil_tmp114 == 2147483670UL' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1388:35-1388:62)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1610:9-1610:16)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:819:29-819:39)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2007:9-2007:28)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1615:11-1615:30)
[Warning][Deadcode][CWE-571] condition 'status < 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:668:29-668:39)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2015:9-2015:23)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1404:33-1404:44)
[Warning][Deadcode][CWE-570] condition 'status >= 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:1240:33-1240:44)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-2.c:2019:11-2019:20)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
