Showing error 764

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: 4435
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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();
4427  }
4428  {
4429#line 165
4430  __cil_tmp5 = (unsigned int )tmp___0;
4431#line 165
4432  if (__cil_tmp5 != 0U) {
4433    {
4434#line 166
4435    printk("<3>cfag12864bfb: ERROR: can\'t enable cfag12864b refreshing (being used)\n");
4436    }
4437#line 168
4438    return (-19);
4439  } else {
4440
4441  }
4442  }
4443  {
4444#line 171
4445  ret = platform_driver_register(& cfag12864bfb_driver);
Show full sources
↑