Showing error 771

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/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1158
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

1128#line 152
1129    goto none;
1130  } else {
1131
1132  }
1133  }
1134  {
1135#line 155
1136  __cil_tmp11 = (int (*)(void * ))0;
1137#line 155
1138  __cil_tmp12 = (void (*)(void * ))0;
1139#line 155
1140  __cil_tmp13 = (void (*)(void * ))0;
1141#line 155
1142  __cil_tmp14 = (void *)0;
1143#line 155
1144  ks0108_pardevice = parport_register_device(ks0108_parport, "ks0108", __cil_tmp11,
1145                                             __cil_tmp12, __cil_tmp13, 2, __cil_tmp14);
1146  }
1147  {
1148#line 157
1149  __cil_tmp15 = (struct pardevice *)0;
1150#line 157
1151  __cil_tmp16 = (unsigned long )__cil_tmp15;
1152#line 157
1153  __cil_tmp17 = (unsigned long )ks0108_pardevice;
1154#line 157
1155  if (__cil_tmp17 == __cil_tmp16) {
1156    {
1157#line 158
1158    printk("<3>ks0108: ERROR: parport didn\'t register new device\n");
1159    }
1160#line 160
1161    goto none;
1162  } else {
1163
1164  }
1165  }
1166  {
1167#line 163
1168  result = parport_claim(ks0108_pardevice);
Show full sources
↑