Bug #340
closed
Support of signed/unsigned integer types and integer constant
Added by Evgeny Novikov almost 14 years ago.
Updated over 11 years ago.
Detected in build:
old bug
Published in build:
e2a8d1f
Description
LLVM converts all standard integer types (either signed or unsigned) to 'int32' with no sign and supports both signed and unsigned integers constants. But when CBackend prints variables having integer types it must say what type they have. It assumes that all such variables have 'unsigned int'. So then it has to convert all constants to unsigned equivalents. But it seems that afterwards cil+blast doesn't accept this correctly (they don't understand that the '4 million' constant is simply '-4').
Pavel Shved 2009-12-08 16:42:38 MSK¶
For example, these drivers are reported as incorrect due to this bug. Funny, but they're all TIME LIMITs if checked without LLVM:
- drivers/media/dvb/dvb-usb/af9015.c unsafe
- drivers/media/dvb/dvb-usb/au6610.c unsafe
- drivers/media/dvb/dvb-usb/ce6230.c unsafe
- drivers/media/dvb/dvb-usb/cxusb.c unsafe
- drivers/media/dvb/dvb-usb/digitv.c unsafe
- drivers/media/dvb/dvb-usb/dtv5100.c unsafe
- drivers/media/dvb/dvb-usb/dw2102.c unsafe
- drivers/media/dvb/dvb-usb/gl861.c unsafe
- drivers/media/dvb/dvb-usb/gp8psk.c unsafe
- drivers/media/dvb/dvb-usb/m920x.c unsafe
- drivers/media/dvb/dvb-usb/ttusb2.c unsafe
- drivers/media/dvb/dvb-usb/vp702x.c unsafe
- drivers/media/dvb/dvb-usb/vp7045.c == unsafe
- Status changed from New to Open
- Priority changed from Normal to High
It seems that this bug prevent some aspect models like 08_1 from correct verification.
We've to think about usage of LLVM at all...
- Priority changed from High to Low
I assume that we won't depend on this bug if we'll finish use of llvm. So we don't need to spend our time to resolve this issue.
I think that we shouldn't hurry. This bug blocks #876 ("Issues related with LLVM usage should be removed") that in turn consists of a lot of "LLVM" bugs. So I suggest that we will close all of them immediately when we will say that the new aspectator works well enough (and doesn't contain non of those bugs indeed).
- Status changed from Open to Resolved
- Published in build set to e2a8d1f
There is no more the given issue since we have moved aspectator from LLVM to GCC.
- Status changed from Resolved to Closed
- Project changed from Linux Driver Verification to C Instrumentation Framework
- Category deleted (
15)
Also available in: Atom
PDF