Showing error 174

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1448
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

1418#line 143
1419  __cil_tmp19 = (void *)0;
1420#line 143
1421  __cil_tmp20 = (unsigned long )__cil_tmp19;
1422#line 143
1423  __cil_tmp21 = (unsigned long )ks0108_pardevice;
1424#line 143
1425  if (__cil_tmp21 == __cil_tmp20) {
1426    {
1427#line 144
1428    printk("<3>ks0108: ERROR: parport didn\'t register new device\n");
1429    }
1430#line 146
1431    goto none;
1432  } else {
1433
1434  }
1435  }
1436  {
1437#line 149
1438  result = parport_claim(ks0108_pardevice);
1439  }
1440#line 150
1441  if (result != 0) {
1442    {
1443#line 151
1444    __cil_tmp22 = & ks0108_port;
1445#line 151
1446    __cil_tmp23 = *__cil_tmp22;
1447#line 151
1448    printk("<3>ks0108: ERROR: can\'t claim %i parport, maybe in use\n", __cil_tmp23);
1449#line 153
1450    ret = result;
1451    }
1452#line 154
1453    goto registered;
1454  } else {
1455
1456  }
1457#line 157
1458  ks0108_inited = (unsigned char)1;
Show full sources