Project

General

Profile

Actions

Bug #5323

closed

Incorrect type for pointer in ___del_dma_pool

Added by Vadim Mutilin over 9 years ago. Updated almost 5 years ago.

Status:
Closed
Priority:
Urgent
Category:
C back-end
Start date:
10/08/2014
Due date:
% Done:

0%

Estimated time:
Detected in build:
2c42610
Platform:
Published in build:

Description

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


Related issues 1 (0 open1 closed)

Related to Klever - Bug #6629: Used CIL is outdatedClosedEvgeny Novikov03/13/2019

Actions
Actions #1

Updated by Evgeny Novikov over 9 years ago

  • Assignee set to Evgeny Novikov

I suggest that the cause of this issue is the same as in #1258.

Actions #2

Updated by Evgeny Novikov over 9 years ago

  • Status changed from New to Open
Actions #3

Updated by Vadim Mutilin about 9 years ago

The same problem occurs in vt6655_init_info
http://lxr.free-electrons.com/source/drivers/staging/vt6655/device_main.c?v=3.17#L992

992 static void vt6655_init_info(struct pci_dev *pcid, PSDevice *ppDevice,
993                              PCHIP_INFO pChip_info) {

CIF prints
static void vt6655_init_info(struct pci_dev *pcid, PSDevice **ppDevice, PCHIP_INFO pChip_info)

GCC diagnostics
drivers/staging/vt6655/device_main.c: In function 'vt6655_init_info':
drivers/staging/vt6655/device_main.c:1005:22: error: request for member 'prev' in something not a structure or union

Actions #4

Updated by Evgeny Novikov about 8 years ago

  • Priority changed from Low to High

This is definitely very bad.

Actions #5

Updated by Evgeny Novikov about 8 years ago

  • Category set to C back-end
Actions #6

Updated by Evgeny Novikov almost 5 years ago

  • Priority changed from High to Urgent

After switching to new CIL from Frama-C (#6629) this issue became crucial since new CIL fails on parsing this bad code. Instead of workarounds in CIL I prefer to fix C back-end of course.

Actions #7

Updated by Evgeny Novikov almost 5 years ago

  • Related to Bug #6629: Used CIL is outdated added
Actions #8

Updated by Evgeny Novikov almost 5 years ago

  • Status changed from Open to Closed

It seems that I fixed this very old bug at last in a492618.

Actions

Also available in: Atom PDF