Showing error 170

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

Source: 

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  {
1603#line 351
1604  __cil_tmp11 = 1UL * 1024UL;
1605#line 351
1606  tmp___1 = kmalloc(__cil_tmp11, 208U);
1607#line 351
1608  cfag12864b_cache = (unsigned char *)tmp___1;
1609  }
1610  {
1611#line 353
1612  __cil_tmp12 = (void *)0;
1613#line 353
1614  __cil_tmp13 = (unsigned long )__cil_tmp12;
1615#line 353
1616  __cil_tmp14 = (unsigned long )cfag12864b_cache;
1617#line 353
1618  if (__cil_tmp14 == __cil_tmp13) {
1619    {
1620#line 354
1621    printk("<3>cfag12864b: ERROR: can\'t alloc cache buffer (%i bytes)\n", 1024);
1622#line 357
1623    ret = -12;
1624    }
1625#line 358
1626    goto bufferalloced;
1627  } else {
1628
1629  }
1630  }
1631  {
Show full sources
↑