Showing error 165

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--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4586
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

4556    (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0,
4557    {"cfag12864bfb", (struct bus_type *)0, (struct module *)0, (char const   *)0,
4558     (_Bool)0, (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0,
4559     (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, (int (*)(struct device *dev ,
4560                                                                                 pm_message_t state ))0,
4561     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
4562     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
4563#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/drivers/auxdisplay/cfag12864bfb.c.common.c"
4564static struct platform_device *cfag12864bfb_device  ;
4565#line 140
4566static int cfag12864bfb_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
4567#line 140 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16869/dscv_tempdir/dscv/ri/32_1/drivers/auxdisplay/cfag12864bfb.c.common.c"
4568static int cfag12864bfb_init(void) 
4569{ int ret ;
4570  unsigned char tmp___7 ;
4571  unsigned char tmp___8 ;
4572
4573  {
4574  {
4575#line 142
4576  ret = -22;
4577#line 145
4578  tmp___7 = cfag12864b_isinited();
4579  }
4580#line 145
4581  if (tmp___7) {
4582
4583  } else {
4584    {
4585#line 146
4586    printk("<3>cfag12864bfb: ERROR: cfag12864b is not initialized\n");
4587    }
4588#line 148
4589    goto none;
4590  }
4591  {
4592#line 151
4593  tmp___8 = cfag12864b_enable();
4594  }
4595#line 151
4596  if (tmp___8) {
Show full sources