Showing error 169

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

Source: 

1562    {
1563#line 337
1564    printk("<3>cfag12864b: ERROR: ks0108 is not initialized\n");
1565    }
1566#line 339
1567    goto none;
1568  }
1569  {
1570#line 343
1571  tmp___0 = get_zeroed_page(208U);
1572#line 343
1573  __cil_tmp5 = & cfag12864b_buffer;
1574#line 343
1575  *__cil_tmp5 = (unsigned char *)tmp___0;
1576  }
1577  {
1578#line 344
1579  __cil_tmp6 = (void *)0;
1580#line 344
1581  __cil_tmp7 = (unsigned long )__cil_tmp6;
1582#line 344
1583  __cil_tmp8 = & cfag12864b_buffer;
1584#line 344
1585  __cil_tmp9 = *__cil_tmp8;
1586#line 344
1587  __cil_tmp10 = (unsigned long )__cil_tmp9;
1588#line 344
1589  if (__cil_tmp10 == __cil_tmp7) {
1590    {
1591#line 345
1592    printk("<3>cfag12864b: ERROR: can\'t get a free page\n");
1593#line 347
1594    ret = -12;
1595    }
1596#line 348
1597    goto none;
1598  } else {
1599
1600  }
1601  }
1602  {
Show full sources
↑