Actions
Bug #1069
openBLAST goes to local label out instead of global one or vice versa
Status:
New
Priority:
Normal
Assignee:
-
Category:
CIL
Target version:
-
Start date:
04/12/2011
Due date:
% Done:
0%
Estimated time:
Detected in build:
41b2b9632f441a890ed26345cc44d3d8ce6fdd25
Platform:
Published in build:
Description
=== linux-2.6.37 39_7 drivers/bluetooth/hci_uart.ko ldv_main3_sequence_infinite_withcheck_stateful (false unsafe:label) BT_DBG("hu %p", hu); goto local label out (marked as __label__) misinterprets as leading to global label out === linux-2.6.37 39_7 drivers/input/serio/ps2mult.ko ldv_main0_sequence_infinite_withcheck_stateful (false unsafe:label) dev_dbg(&serio->dev, "Received %02x flags %02x\n", data, dfl); local label out === linux-2.6.37 39_7 drivers/net/8139too.ko ldv_main0_sequence_infinite_withcheck_stateful (false unsafe:label) netdev_dbg macro declares local label out goes to local label out instead of global one === linux-2.6.37 39_7 drivers/net/ethoc.ko ldv_main0_sequence_infinite_withcheck_stateful (false unsafe:label) dev_dbg(&dev->dev, "stopping queue\n"); goto global out instead of local one
Updated by Evgeny Novikov over 13 years ago
Our C backend may be adjusted to provide unique labels as workaround. Although it will be just a workaround.
Updated by Pavel Shved over 13 years ago
Eugene Novikov wrote:
Our C backend may be adjusted to provide unique labels as workaround. Although it will be just a workaround.
Actually, we might want to name these "workarounds" "simplifications of C code to support more Static Verifiers", and they will become mainstream. :-)
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
Updated by Vadim Mutilin about 10 years ago
- Category set to CIL
- Assignee deleted (
Pavel Shved)
Looks like a CIL bug.
See #1334
Actions