Showing error 763

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


Source:

4386     (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t  ))0,
4387     (int (*)(struct device * ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
4388     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
4389#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864bfb.c.p"
4390static struct platform_device *cfag12864bfb_device  ;
4391#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864bfb.c.p"
4392static int cfag12864bfb_init(void) 
4393{ int ret ;
4394  unsigned char tmp ;
4395  unsigned char tmp___0 ;
4396  unsigned int __cil_tmp4 ;
4397  unsigned int __cil_tmp5 ;
4398  struct platform_device *__cil_tmp6 ;
4399  unsigned long __cil_tmp7 ;
4400  unsigned long __cil_tmp8 ;
4401
4402  {
4403  {
4404#line 156
4405  ret = -22;
4406#line 159
4407  tmp = cfag12864b_isinited();
4408  }
4409  {
4410#line 159
4411  __cil_tmp4 = (unsigned int )tmp;
4412#line 159
4413  if (__cil_tmp4 == 0U) {
4414    {
4415#line 160
4416    printk("<3>cfag12864bfb: ERROR: cfag12864b is not initialized\n");
4417    }
4418#line 162
4419    goto none;
4420  } else {
4421
4422  }
4423  }
4424  {
4425#line 165
4426  tmp___0 = cfag12864b_enable();
Show full sources