Showing error 767

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

Source: 

1520    }
1521#line 353
1522    goto none;
1523  } else {
1524
1525  }
1526  }
1527  {
1528#line 357
1529  tmp___0 = get_zeroed_page(208U);
1530#line 357
1531  __cil_tmp9 = & cfag12864b_buffer;
1532#line 357
1533  *__cil_tmp9 = (unsigned char *)tmp___0;
1534  }
1535  {
1536#line 358
1537  __cil_tmp10 = (unsigned char *)0;
1538#line 358
1539  __cil_tmp11 = (unsigned long )__cil_tmp10;
1540#line 358
1541  __cil_tmp12 = & cfag12864b_buffer;
1542#line 358
1543  __cil_tmp13 = *__cil_tmp12;
1544#line 358
1545  __cil_tmp14 = (unsigned long )__cil_tmp13;
1546#line 358
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  {
Show full sources
↑