C Instrumentation Framework

For the variable pp which originally has type m_pool_p *
CIF print type m_pool_p **

Original

 static void ___del_dma_pool(m_pool_p p)
 {
         m_pool_p *pp = &mp0.next;

         while (*pp && *pp != p)
                 pp = &(*pp)->next;

CIF output

static void ___del_dma_pool(m_pool_p p)
{
  m_pool_p **pp = ( m_pool_p **) & mp0 . next;
# 328 "drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared" 
  goto ldv_36182;
  ldv_36181:;
# 329 "drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared" 
  pp = ( m_pool_p **) & ( * * pp ) . next;
  ldv_36182:;

GCC output

drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared: In function ‘___del_dma_pool’:
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared:329:36: error: request for member ‘next’ in something not a structure or union
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared:331:23: error: request for member ‘next’ in something not a structure or union
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared: In function ‘___free_dma_mem_cluster’:
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared:284:40: error: request for member ‘next’ in something not a structure or union
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared:283:52: error: request for member ‘vaddr’ in something not a structure or union
drivers/scsi/sym53c8xx_2/sym_malloc.o.c.prepared:287:27: error: request for member ‘next’ in something not a structure or union

CPAchecker

Unrecognized C code (Field owner of a non-composite type): (*(*pp)).next (line was originally * pp = ( * * pp ) . next;)

linux-3.17-rc1.tar.xz, 32_7a, drivers/scsi/sym53c8xx_2/sym53c8xx.ko, ldv_main1_sequence_infinite_withcheck_stateful