Showing error 768

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

Source: 

1547  if (__cil_tmp14 == __cil_tmp11) {
1548    {
1549#line 359
1550    printk("<3>cfag12864b: ERROR: can\'t get a free page\n");
1551#line 361
1552    ret = -12;
1553    }
1554#line 362
1555    goto none;
1556  } else {
1557
1558  }
1559  }
1560  {
1561#line 365
1562  tmp___1 = kmalloc(1024UL, 208U);
1563#line 365
1564  cfag12864b_cache = (unsigned char *)tmp___1;
1565  }
1566  {
1567#line 367
1568  __cil_tmp15 = (unsigned char *)0;
1569#line 367
1570  __cil_tmp16 = (unsigned long )__cil_tmp15;
1571#line 367
1572  __cil_tmp17 = (unsigned long )cfag12864b_cache;
1573#line 367
1574  if (__cil_tmp17 == __cil_tmp16) {
1575    {
1576#line 368
1577    printk("<3>cfag12864b: ERROR: can\'t alloc cache buffer (%i bytes)\n", 1024);
1578#line 371
1579    ret = -12;
1580    }
1581#line 372
1582    goto bufferalloced;
1583  } else {
1584
1585  }
1586  }
1587  {
Show full sources
↑