Bug #340
closedSupport of signed/unsigned integer types and integer constant
0%
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').
Updated by Evgeny Novikov almost 14 years ago
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
Updated by Evgeny Novikov over 13 years ago
- 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...
Updated by Evgeny Novikov over 13 years ago
- 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.
Updated by Evgeny Novikov about 13 years ago
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).
Updated by Evgeny Novikov almost 13 years ago
- 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.
Updated by Pavel Shved almost 13 years ago
- Status changed from Resolved to Closed
Updated by Evgeny Novikov over 11 years ago
- Project changed from Linux Driver Verification to C Instrumentation Framework
- Category deleted (
15)