Actions
Bug #5323
closedIncorrect type for pointer in ___del_dma_pool
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
Updated by Evgeny Novikov about 10 years ago
- Assignee set to Evgeny Novikov
I suggest that the cause of this issue is the same as in #1258.
Updated by Vadim Mutilin over 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
Updated by Evgeny Novikov almost 9 years ago
- Priority changed from Low to High
This is definitely very bad.
Updated by Evgeny Novikov over 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.
Updated by Evgeny Novikov over 5 years ago
- Related to Bug #6629: Used CIL is outdated added
Updated by Evgeny Novikov over 5 years ago
- Status changed from Open to Closed
It seems that I fixed this very old bug at last in a492618.
Actions