Project

General

Profile

Actions

Bug #1069

open

BLAST goes to local label out instead of global one or vice versa

Added by Vadim Mutilin over 13 years ago. Updated about 10 years ago.

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

Actions #1

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.

Actions #2

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. :-)

Actions #3

Updated by Pavel Shved over 13 years ago

  • Priority changed from High to Normal
Actions #4

Updated by Pavel Shved about 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions #5

Updated by Vadim Mutilin about 10 years ago

  • Category set to CIL
  • Assignee deleted (Pavel Shved)

Looks like a CIL bug.
See #1334

Actions

Also available in: Atom PDF