Showing error 166

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

Source: 

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) {
4597    {
4598#line 152
4599    printk("<3>cfag12864bfb: ERROR: can\'t enable cfag12864b refreshing (being used)\n");
4600    }
4601#line 154
4602    return (-19);
4603  } else {
4604
4605  }
4606  {
4607#line 157
4608  ret = platform_driver_register(& cfag12864bfb_driver);
4609  }
Show full sources
↑