Showing error 766

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

Source: 

1489  unsigned char *__cil_tmp10 ;
1490  unsigned long __cil_tmp11 ;
1491  unsigned char **__cil_tmp12 ;
1492  unsigned char *__cil_tmp13 ;
1493  unsigned long __cil_tmp14 ;
1494  unsigned char *__cil_tmp15 ;
1495  unsigned long __cil_tmp16 ;
1496  unsigned long __cil_tmp17 ;
1497  struct workqueue_struct *__cil_tmp18 ;
1498  unsigned long __cil_tmp19 ;
1499  unsigned long __cil_tmp20 ;
1500  void const   *__cil_tmp21 ;
1501  unsigned char **__cil_tmp22 ;
1502  unsigned char *__cil_tmp23 ;
1503  unsigned long __cil_tmp24 ;
1504
1505  {
1506  {
1507#line 347
1508  ret = -22;
1509#line 350
1510  tmp = ks0108_isinited();
1511  }
1512  {
1513#line 350
1514  __cil_tmp8 = (unsigned int )tmp;
1515#line 350
1516  if (__cil_tmp8 == 0U) {
1517    {
1518#line 351
1519    printk("<3>cfag12864b: ERROR: ks0108 is not initialized\n");
1520    }
1521#line 353
1522    goto none;
1523  } else {
1524
1525  }
1526  }
1527  {
1528#line 357
1529  tmp___0 = get_zeroed_page(208U);
Show full sources
↑