Showing error 168

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


Source:

1534  unsigned long __cil_tmp10 ;
1535  unsigned long __cil_tmp11 ;
1536  void *__cil_tmp12 ;
1537  unsigned long __cil_tmp13 ;
1538  unsigned long __cil_tmp14 ;
1539  void *__cil_tmp15 ;
1540  struct lock_class_key *__cil_tmp16 ;
1541  void *__cil_tmp17 ;
1542  char const   *__cil_tmp18 ;
1543  void *__cil_tmp19 ;
1544  unsigned long __cil_tmp20 ;
1545  unsigned long __cil_tmp21 ;
1546  void const   *__cil_tmp22 ;
1547  unsigned char **__cil_tmp23 ;
1548  unsigned char *__cil_tmp24 ;
1549  unsigned long __cil_tmp25 ;
1550
1551  {
1552  {
1553#line 333
1554  ret = -22;
1555#line 336
1556  tmp = ks0108_isinited();
1557  }
1558#line 336
1559  if (tmp) {
1560
1561  } else {
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
Show full sources